Algebraic approach to linking the semantics of web services

Web services have become more and more important in these years, and BPEL4WS (BPEL) is a de facto standard for the web service composition and orchestration. It contains several distinct features, including the scope-based compensation and fault handling mechanism. We have considered the operational semantics and denotational semantics for BPEL, where a set of algebraic laws can be achieved via these two models, respectively. In this paper, we consider the inverse work, deriving the operational semantics and denotational semantics from algebraic semantics for BPEL. In our model, we introduce four types of typical programs, by which every program can be expressed as the summation of these four types. Based on the algebraic semantics, the strategy for deriving the operational semantics is provided and a transition system is derived by strict proof. This can be considered as the soundness exploration for the operational semantics based on the algebraic semantics. Further, the equivalence between the derivation strategy and the derived transition system is explored, which can be considered as the completeness of the operational semantics. Finally, the derivation of the denotational semantics from algebraic semantics is explored, which can support to reason about more program properties easily.     

Specification-oriented semantics for Communicating Processes

Summary A process P satisfies a specification S if every observation we can make of the behaviour of P is allowed by S. We use this idea of process correctness as a starting point for developing a specific form of denotational semantics for processes, called here specification — oriented semantics. This approach serves as a uniform framework for generating and relating a series of increasingly sophisticated denotational models for Communicating Processes. These models differ in the underlying structure of their observations which influences both the number of representable language operators and the induced notion of process correctness. Safety properties are treated by all models; the more sophisticated models also permit proofs of certain liveness properties. An important feature of the models is a special hiding operator which abstracts from internal process activity. This allows large processes to be composed hierarchically from networks of smaller ones in such a way that proofs of the whole are constructed from proofs of its components. We also show the consistency of our denotational models w.r.t. a simple operational semantics based on transitions which make internal process activity explicit. A preliminary version of this paper appeared in [42]     

A comparative study of two formal semantics of the SIGNAL language

SIGNAL is a part of the synchronous languages family, which are broadly used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. There exist several semantics for SIGNAL, such as denotational semantics based on traces (called trace semantics), denotational semantics based on tags (called tagged model semantics), operational semantics presented by structural style through an inductive definition of the set of possible transitions, operational semantics defined by synchronous transition systems (STS), etc. However, there is little research about the equivalence between these semantics. In this work, we would like to prove the equivalence between the trace semantics and the tagged model semantics, to get a determined and precise semantics of the SIGNAL language. These two semantics have several different definitions respectively, we select appropriate ones and mechanize them in the Coq platform, the Coq expressions of the abstract syntax of SIGNAL and the two semantics domains, i.e., the trace model and the tagged model, are also given. The distance between these two semantics discourages a direct proof of equivalence. Instead, we transformthem to an intermediate model, which mixes the features of both the trace semantics and the tagged model semantics. Finally, we get a determined and precise semantics of SIGNAL.     

The semantics of the combination of atomized statements and parallel choice

In this paper we define a uniform language that is an extension of the language underlying the process algebraPA. One of the main extensions of this language overPA is given by so-called atomizing brackets. If we place these brackets around a statement then we treat this statement as an atomic action. Put differently, these brackets remove all interleaving points. We present a transition system for the language and derive its operational semantics. We show that there are several options for defining a transition system such that the resulting operational semantics is a conservative extension of the semantics forPA. We define a semantic domain and a denotational model for the language. Next we define a closure operator on the semantic domain and show how to use this closure operator to derive a fully abstract denotational semantics. Then the algebraic theory of the language is considered. We define a collection of axioms and a term rewrite system based on these axioms. Using this term rewrite system we are able to identify normal forms for the language. It is shown that these axioms capture the denotational equality. It follows that if two terms are provably equal then they have the same operational semantics. Finally, we show how to extend the axiomatization in order to axiomatize its operational equivalence.     

Operational and goal-independent denotational semantics for Prolog with cut

In this paper we propose an operational and a denotational semantics for Prolog. We deal with the control rules of Prolog and the cut operator. Our denotational semantics provides a goal-independent semantics. This means that the behaviour of a goal in a program is defined as the evaluation of the goal in the denotation (semantics) of the program. We show how our denotational semantics can be specialised into a computed answer semantics and into a call pattern semantics. Our work provides a basis for a precise abstract interpretation of Prolog programs.     

A mathematical semantics for a nondeterministic typed λ-calculus

This paper is concerned with the problems encountered in defining the semantics of nondeterministic algorithms. A nondeterministic control structure is added to a typed λ-calculus and the usual operational semantics for the deterministic language is generalized to take into account the more complex behaviour of nondeterministic algorithms. A mathematical model is then given for the language and the relationship between the denotational and operational semantics is explored.     

Executing continuation semantics: A comparison

Several authors have suggested translating denotational semantics into prototype interpreters written in high-level programming languages to provide evaluation tools for language designers. These implementations have generally been understandable when restricted to direct denotational semantics. This paper considers using two declarative programming languages, Prolog and Standard ML, to implement an interpreter that follows the continuation semantics of a small imperative programming language, called Gull. Each of the two declarative languages presents certain difficulties related to evaluation strategies and expressiveness. The implementations are compared in terms of their ease of use for prototyping, their resemblance to the denotational definitions, and their efficiency.     

From algebraic semantics to denotational semantics for Verilog

This paper considers how the algebraic semantics for Verilog relates with its denotational semantics. Our approach is to derive the denotational semantics from the algebraic semantics. We first present the algebraic laws for Verilog. Every program can be expressed as a guarded choice that can model the execution of a program. In order to investigate the parallel expansion laws, a sequence is introduced, indicating which instantaneous action is due to which exact parallel component. A head normal form is defined for each program by using a locality sequence. We provide a strategy for deriving the denotational semantics based on head normal form. Using this strategy, the denotational semantics for every program can be calculated. Program equivalence can also be explored by using the derived denotational semantics. A short version of this paper appeared in Proc. ICECCS 2006: 11th IEEE International Conference on Engineering of Complex Computer Systems [48]. This work is partially supported by the National Basic Research Program of China (No. 2005CB321904), the National High Technology Research and Development Program of China (No. 2007AA010302) and the National Natural Science Foundation of China (No. 90718004). Jonathan Bowen is a visiting professor at King’s College London and an emeritus professor at London South Bank University.     

A continuous semantics for unbounded nondeterminism

Nondeterminism is introduced into an ordinary iterative programming language by treating procedure calls as nondeterministic assignment statements. The effect of such assignment statements is assumed to be determined solely by the entry-exit specifications of the corresponding procedures. The nondeterminism which this approach yields is not necessarily bounded. The paper discusses the problem of defining a denotational semantic for programming languages with this kind of, possibly unbounded, nondeterminism. As an additional constraint, the semantics is required to be continuous, in the sense that the underlying semantic algebra is continuous. It is shown how such a continuous semantics for unbounded nondeterminism can be derived from a simple operational semantics based on program execution trees.     

A set-theoretic semantics for Clear

Summary A semantics for the Clear specification language is given. The language of set theory is employed to present constructions corresponding to Clear's specification-combining operations, which are then used as the basis for a denotational semantics. This is in contrast to Burstall and Goguen's 1980 semantics which described the meanings of these operations more abstractly via concepts from category theory.     

prialt in Handel-C: an operational semantics

We describe an operational semantics for the hardware compilation language Handel-C [7], which is a C-like language with channel communication and parallel constructs which compiles down to mainly synchronously clocked hardware. The work in this paper builds on previous work describing the semantics of the “prialt” construct within Handel-C [5] and a denotational semantics for part of the language [6]. We describe a key subset of the language and show how a design decision for the real language, namely that default guards in a prialt statement executed in “zero-time”, has consequences for the complexity of the operational semantics. We present the operational semantics, along with a revised and completed prialt semantics, indicating clearly the interface between them. We then describe a notion of observational equivalence and present an example illustrating how we handle the complexity of nested prialts in default guards.     

Event-based operational semantics and a consistency result for real-time concurrent processes with action refinement

In this paper an event-based operational interleaving semantics is proposed for real-time processes,for which action refinement and a denotational true concurrency semantics are developed and defined in terms of timed event structures. The authors characterize the timed event traces that are generated by the operational semantics in a denotational way, and show that this operational semantics is consistent with the denotational semantics in the sense that they generate the same set of timed event traces, thereby eliminating the gap between the true concurrency and interleaving semantics.     

Stack method in program semantics

In this paper,we describe firstly a formal concept of stack and introduce some operational rules on it.Then we extend the denotational semantics to“the denotational semantics with stacks”,by which we makea formal semantics for a real PASCAL(subset)which can run on a computer.By an example of programwith procedures it will be seen that our method can be used to describe the basic principles of compiling.Finally,we have succeeded in building a formal semantics model of a PROLOG(subset).     

Semantic theories of programs with nested interrupts

In the design of dependable software for embedded and real-time operating systems, time analysis is a crucial but extremely difficult issue, the challenge of which is exacerbated due to the randomness and nondeterminism of interrupt handling behaviors. Thus research into a theory that integrates interrupt behaviors and time analysis seems to be important and challenging. In this paper, we present a programming language to describe programs with interrupts that is comprised of two essential parts: main program and interrupt handling programs. We also explore a timed operational semantics and a denotational semantics to specify the meanings of our language. Furthermore, a strategy of deriving denotational semantics from the timed operational semantics is provided to demonstrate the soundness of our operational semantics by showing the consistency between the derived denotational semantics and the original denotational semantics.     

The rewriting logic semantics project

Rewriting logic is a flexible and expressive logical framework that unifies algebraic denotational semantics and structural operational semantics (SOS) in a novel way, avoiding their respective limitations and allowing succinct semantic definitions. The fact that a rewrite logic theory’s axioms include both equations and rewrite rules provides a useful “abstraction dial” to find the right balance between abstraction and computational observability in semantic definitions. Such semantic definitions are directly executable as interpreters in a rewriting logic language such as Maude, whose generic formal tools can be used to endow those interpreters with powerful program analysis capabilities.     

Denotational semantics of a synchronous VHDL subset

A denotational definition for a single clock synchronous subset of VHDL is proposed. The different domains for variables and signals, the elaboration of static environments, and the formulation of a simulation algorithm for the sub-language characterize this definition, and distinguish it from more traditional denotational semantics of programming languages.     

A denotational semantics for Handel-C

We present a denotational semantics for a fully functional subset of the Handel-C hardware compilation language (Celoxica Ltd., Handel-C Language Reference Manual, v3.0, 2002, ), based on the concept of typed assertion traces. We motivate the choice of semantic domains by illustrating the complexities of the behaviour of the language, paying particular attention to the prialt (priority-alternation) construct of Handel-C. We then define the typed assertion traces over an abstract notion of actions, and demonstrate key properties of the key semantic operations on these. The denotational semantics is then given using traces with actions instantiated as state-transformers.