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.     

A Framework for Operational Equational Specifications with Pre-defined Structures

We present a general framework for studying equational specifications with pre-defined structures. The axioms of the specifications are to define new structures in addition to the given ones. In particular, they may define a new operator only partially over some given domain. Our approach allows one to assign easily semantics to such specifications in a denotational and operational fashion. In order to enable functional-style computations, we introduce a semantically enriched notion of term rewriting. This rewrite relation also allows us to infer the consistency of the specification. For the latter purpose one has to show confluence modulo the given structures. We outline how to obtain criteria easily for confluence and termination of the rewrite relation of discourse by generalizing results of the classical syntactic rewrite theory.     

The Rewriting Logic Semantics Project

Rewriting logic is a flexible and expressive logical framework that unifies denotational semantics and SOS in a novel way, avoiding their respective limitations and allowing very succinct semantic definitions. The fact that a rewrite theory's axioms include both equations and rewrite rules provides a very useful “abstraction knob” to find the right balance between abstraction and 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.     

Tableaux for logic programming

We present a logic programming language, which we call Proflog, with an operational semantics based on tableaux and a denotational semantics based on supervaluations. We show the two agree. Negation is well behaved, and semantic noncomputability issues do not arise. This is accomplished essentially by dropping a domain closure requirement. The cost is that intuitions developed through the use of classical logic may need modification, though the system is still classical at a level once removed. Implementation problems are discussed very briefly; the thrust of the paper is primarily theoretical.Research partly supported by NSF Grant CCR-9104015.     

Combinator-based compilation of recursive functions with different parameter passing modes

Summary Wand's technique of deriving compilers from denotational semantics is applied to a block structured language with recursive functions. The emphasis is on compilation of different parameter passing modes and a simple storage management. The technique starts by eliminating -variables from semantic equations through the introduction of special-purpose combinators. The final code consists of combinators equivalent to target-machine instructions (running-system procedures). The method enables us to derive a compiler and a running system directly from the denotational semantics of a language.     

基于轨迹的程序语义之一：轨迹与语义对象

本文提出一种基于轨迹的指称语义框架,该框架结合了操作语义和代数语义的特征,避免使用专门的数学理论,将静态语义和动态语义结合在一起统一处理.本文及其续篇将通过一个中等规模的过程式模型语言来说明上述语义框架更适合描述真正的程序设计语言.本文首先引入轨迹概念和模型语言,然后讨论该语言的各句法成分所对应的语义论域,其中没有使用含有函数空间构造运算的递归论域方程.     

A layered semantics for a parallel object-oriented language

We develop a denotational semantics for POOL, a parallel object-oriented programming language. The main contribution of this semantics is an accurate mathematical model of the most important concept in object-oriented programming: the object. This is achieved by structuring the semantics in layers working at three different levels: for statements, objects and programs. For each of these levels we define a specialized mathematical domain of processes, which we use to assign a meaning to each language construct. This is done in the mathematical framework of complete metric spaces. We also define operators that translate between these domains. At the program level we give a precise definition of the observable input/output behaviour of a particular program, which could be used at a later stage to decide the issue of full abstractness. We illustrate our semantic techniques by first applying them to a toy language similar to CSP.This paper describes work done in ESPRIT Basic Research Action 3020,Integration.     

Dynamic composition of parameterised logic modules

We present a logic-based programming language that features meta-level composition operations over programs. Object programs are parameterised named collections of definite clauses which may contain formulae of the form A in Pexp, where A is a standard atomic formula and Pexp is a program expression obtained by applying composition operations over named object programs. The semantics of the language is presented in two different equivalent styles. An operational, top-down semantics is given by means of inference rules, while a denotational, bottom-up semantics is given via an immediate consequence operator associated with program expressions. A meta-programming implementation of the language is also presented by transforming the operational inference rules into meta-level axioms. Several programming examples are discussed to illustrate the expressive power of the language.     

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.     

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.     

一个类Java语言的指称语义

文章提出了一个简化的Java语言SimpleJ并给出了此语言的指称语义。SimpleJ是一个简单的面向对象语言,具有Java语言的基本语义特点,该文通过对SimpleJ语言的语义域和语义方程的刻画和描述,讨论了以对象类型和异常语句为主的Java语言的语义特征。     

The formal definition of a real-time language

Summary This paper presents the formal definition of TOMAL (Task-Oriented Microprocessor Applications Language), a programming language intended for real-time systems running on small processors. The formal definition addresses all aspects of the language. Because some modes of semantic definition seem particularly well-suited to certain aspects of a language, and not as suitable for others, the formal definition employs several complementary modes of definition.The primary definition is axiomatic and is employed to define most statements of the language. Simple, denotational (but not lattice-theoretic) semantics complement the axiomatic semantics to define type-related features, such as binding of names to types, data type coercions, and evaluation of expressions. Together, the axiomatic and denotational semantics define all features of the sequential language. An operational definition is used to define real-time execution, and to extend the axiomatic definition to account for all aspects of concurrent execution. Semantic constraints, sufficient to guarantee conformity of a program with the axiomatic definition, can be checked by analysis of a TOMAL program at compilation.     

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.     

Semantics of plan revision in intelligent agents

In this paper, we give an operational and denotational semantics for a meta-language of the 3APL agent programming language. With this meta-language, various 3APL interpreters can be programmed. We prove equivalence of the operational and denotational semantics. Furthermore, we give an operational semantics for object-level 3APL. Using this semantics, we relate the 3APL meta-language to object-level 3APL by providing a specific interpreter, the semantics of which will prove to be equivalent to object-level 3APL.     

A UTP semantics for Circus

Circus specifications define both data and behavioural aspects of systems using a combination of Z and CSP constructs. Previously, a denotational semantics has been given to Circus; however, a shallow embedding of Circus in Z, in which the mapping from Circus constructs to their semantic representation as a Z specification, with yet another language being used as a meta-language, was not useful for proving properties like the refinement laws that justify the distinguishing development technique associated with Circus. This work presents a final reference for the Circus denotational semantics based on Hoare and He’s Unifying Theories of Programming (UTP); as such, it allows the proof of meta-theorems about Circus including the refinement laws in which we are interested. Its correspondence with the CSP semantics is illustrated with some examples. We also discuss the library of lemmas and theorems used in the proofs of the refinement laws. Finally, we give an account of the mechanisation of the Circus semantics and of the mechanical proofs of the refinement laws.     

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.     

Modalities in linear logic weaker than the exponential “of course”: Algebraic and relational semantics

We present a semantic study of a family of modal intuitionistic linear systems, providing various logics with both an algebraic semantics and a relational semantics, to obtain completeness results. We call modality a unary operator on formulas which satisfies only one rale (regularity), and we consider any subsetW of a list of axioms which defines the exponential of course of linear logic. We define an algebraic semantics by interpreting the modality as a unary operation on an IL-algebra. Then we introduce a relational semantics based on pretopologies with an additional binary relationr between information states. The interpretation of is defined in a suitable way, which differs from the traditional one in classical modal logic. We prove that such models provide a complete semantics for our minimal modal system, as well as, by requiring the suitable conditions onr (in the spirit of correspondence theory), for any of its extensions axiomatized by any subsetW as above. We also prove an embedding theorem for modal IL-algebras into complete ones and, after introducing the notion of general frame, we apply it to obtain a duality between general frames and modal IL-algebras.     

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]     

Step semantics for “true” concurrency with recursion

We present a variety of denotational linear time semantics for a language with recursion and true concurrency in a form of synchronous co-operation, which in the literature is known as step semantics. We show that this can be done by a generalization of known results for interleaving semantics. A general method is presented to define semantical operators and denotational semantics in the Smyth powerdomain of streams. With this method, first a naive and then more sophisticated semantics for synchronous co-operation are developed, which include such features as interleaving and synchronization. Then we refine the semantics to deal with a bounded number of processors, subatomic actions, maximal parallelism and a real-time operator. Finally, it is indicated how to apply these ideas to branching-time models, where it becomes possible to analyze deadlock behaviour as well as a form of true concurrency. John-Jules Meyer received his Master's degree in Mathematics in 1979 from the University of Leiden, and his Ph.D. degree in 1985 from the Free University Amsterdam. He is currently a Professor of Theoretical Computer Science, both at the Free University Amsterdam and at the University of Nijmegen. His current research interests include semantics of programming languages and logics for computer science, in particular artifical intelligence. Erik de Vink received the M.S. degree in Mathematics from the University of Amsterdam. He is currently a Junior Researcher at the Department of Mathematics and Computer Science of the Free University Amsterdam. At the moment his main research concerns the semantics of concurrent and logic programming languages.     

A timed semantics of Orc

Orc is a kernel language for structured concurrent programming. Orc provides three powerful combinators that define the structure of a concurrent computation. These combinators support sequential and concurrent execution, and concurrent execution with blocking and termination.Orc is particularly well-suited for task orchestration, a form of concurrent programming with applications in workflow, business process management, and web service orchestration. Orc provides constructs to orchestrate the concurrent invocation of services while managing time-outs, priorities, and failures of services or communication.Our previous work on the semantics of Orc focused on its asynchronous behavior. The inclusion of time or the effect of delay on a computation had not been modeled. In this paper, we define an operational semantics of Orc that allows reasoning about delays, which are introduced explicitly by time-based constructs or implicitly by network delays. We develop a number of identities among Orc expressions and define an equality relation that is a congruence. We also present a denotational semantics in which the meaning of an Orc program is a set of traces, and show that the two semantics are equivalent.