Semantics of EqL

The formal semantics of a novel language, called EqL, are presented for first-order functional and Horn logic programming. An EqL program is a set of conditional pattern-directed rules, where the conditions are expressed as a conjunction of equations. The programming paradigm provided by this language may be called equational programming. The declarative semantics of equations is given in terms of their complete set of solutions, and the operational semantics for solving equations is an extension of reduction, called object refinement. The correctness of the operational semantics is established through the soundness and completeness theorems. Examples are given to illustrate the language and its semantics.<>     

A rewriting logic approach to operational semantics

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.     

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.     

Executable structural operational semantics in Maude

This paper describes in detail how to bridge the gap between theory and practice when implementing in Maude structural operational semantics described in rewriting logic, where transitions become rewrites and inference rules become conditional rewrite rules with rewrites in the conditions, as made possible by the new features in Maude 2. We validate this technique using it in several case studies: a functional language Fpl (evaluation and computation semantics), an imperative language WhileL (evaluation and computation semantics), Kahn’s functional language Mini-ML (evaluation or natural semantics), Milner’s CCS (with strong and weak transitions), and Full LOTOS (including ACT ONE data type specifications). In addition, on top of CCS we develop an implementation of the Hennessy–Milner modal logic for describing local capabilities of processes, and for LOTOS we build an entire tool where Full LOTOS specifications can be entered and executed (without user knowledge of the underlying implementation of the semantics). We also compare this method based on transitions as rewrites with another one based on transitions as judgements.     

Two-level grammar as an implementable metalanguage for axiomatic semantics

Two-level grammars can define the syntax and the operational semantics of programming languages and these definitions are directly executable by interpretation. In this paper it is shown that axiomatic semantics can also be defined using a two-level grammar with the result being a partially automatic program verification system accomplished within the framework of a language definition. These results imply that a programming language can be defined operationally and axiomatically together in complementary definitions as advocated by Hoare and Lauer. Because two-level grammars are executable, these complementary definitions accomplish a system for interpreting and verifying programs.     

A residualizing semantics for the partial evaluation of functional logic programs

Recent proposals for multi-paradigm declarative programming combine the most important features of functional, logic and concurrent programming into a single framework. The operational semantics of these languages is usually based on a combination of narrowing and residuation. In this paper, we introduce a non-standard, residualizing semantics for multi-paradigm declarative programs and prove its equivalence with a standard operational semantics. Our residualizing semantics is particularly relevant within the area of program transformation where it is useful, e.g., to perform computations during partial evaluation. Thus, the proof of equivalence is a crucial result to demonstrate the correctness of (existing) partial evaluation schemes.     

Logical approximation for program analysis

The abstract interpretation of programs relates the exact semantics of a programming language to a finite approximation of those semantics. In this article, we describe an approach to abstract interpretation that is based in logic and logic programming. Our approach consists of faithfully representing a transition system within logic and then manipulating this initial specification to create a logical approximation of the original specification. The objective is to derive a logical approximation that can be interpreted as a terminating forward-chaining logic program; this ensures that the approximation is finite and that, furthermore, an appropriate logic programming interpreter can implement the derived approximation. We are particularly interested in the specification of the operational semantics of programming languages in ordered logic, a technique we call substructural operational semantics (SSOS). We show that manifestly sound control flow and alias analyses can be derived as logical approximations of the substructural operational semantics of relevant languages.     

进程创建的语义及等价性

针对一个基于共享变量的带有进程创建的命令式语言,用变迁系统描述了它的结构操作语义,并用扩展的状态变迁迹模型定义了它的指称语义,在该模型下,状态变迁被区分为两种不同形式,分别表示发生在原进程和被创建进程中的状态变迁,这样便可以定义适当的语义复合运算,在对命令的指称进行复合时根据变迁类型的不同对变迁迹进行串行或交错连接,恰当地反映了进程的并发运行受创建命令在程序中的相对位置的限制,最后证明了这两个语义     

A Rewriting Logic Approach to Operational Semantics (Extended Abstract)

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, and continuation-based semantics. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.     

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

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

An operational semantics for object-oriented concepts based on the class hierarchy

The formalisation of object-oriented languages is essential for describing the implementation details of specific programming languages or for developing program verification techniques. However there has been relatively little formalisation work aimed at abstractly describing the fundamental concepts of object-oriented programming, separate from specific language considerations or suitability for a particular verification style. In this paper we address this issue by formalising a language that includes the core object-oriented programming language concepts of field tests and updates, methods, constructors, subclassing, multithreading, and synchronisation, built on top of standard sequential programming constructs. The abstract syntax is relatively close to the core of typical object-oriented programming languages such as Java. A novel aspect of the syntax is that objects and classes are encapsulated within a single syntactic term, including their fields and methods. Furthermore, class terms are structured according to the class hierarchy, and objects appear as subterms of their class (and method instances as subterms of the relevant object). This helps to narrow the gap between how a programmer thinks about their code and the underlying mathematical objects in the semantics. The semantics is defined operationally, so that all actions a program may take, such as testing or setting local variables and fields, or invoking methods on other objects, appear on the labels of the transitions. A process-algebraic style of interprocess communication is used for object and class interactions. A benefit of this label-based approach to the semantics is that a separation of concerns can be made when defining the rules of the different constructs, and the rules tend to be more concise. The basic rules for individual commands may be composed into more powerful rules that operate at the level of classes and objects. The traces generated by the operational semantics are used as the basis for establishing equivalence between classes.     

Operational semantics of Framed Tempura

This paper investigates the operational semantics of temporal logic programs. To this end, a temporal logic programming language called Framed Tempura is employed. The evaluation rules for both the arithmetic and boolean expressions are defined. The semantic equivalence rules for the reduction of a program within a state is formalized. Furthermore, the transition rules within a state and transition rules over an interval between configurations are also specified. Moreover, some examples are given to illustrate how these rules work. Thus, the executable behavior of framed programs can be captured in an operational way. In addition, the consistency between the operational semantics and the minimal model semantics based on model theory is proved in detail.     

Agents with emotions

This paper discusses the role of emotions in artificial agent design and implementation. The syntax and semantics of a simplified version of a logic‐based agent‐oriented programming language is presented. This programming language facilitates the implementation of artificial agents with emotions. Four types of emotions are distinguished: happiness, sadness, anger, and fear. These emotions are defined relative to agent's goals and plans. The emotions result from the agent's deliberation process and influence the deliberation process. The semantics of each emotion type is incorporated in the transition semantics of the presented agent‐oriented programming language. © 2010 Wiley Periodicals, Inc.     

Typical examples of using the atoment language

Atoment is a domain-specific language of executable specifications applied to describe methods and techniques of program verification. In this paper, a series of typical examples of using the Atoment language covering program models; the operational, transformational, and axiomatic semantics; and the formal specification of programming languages is presented.     

Asynchronous communication model based on linear logic

We propose a new framework called ACL for concurrent computation based on linear logic. ACL is a kind oflinear logic programming framework, where its operational semantics is described in terms ofproof construction in linear logic. We also give a model-theoretic semantics based onphase semantics, a model of linear logic. Our framework well captures concurrent computation based on asynchronous communication. It will, therefore, provide us with a new insight into other models of asynchronous concurrent computation from alogical point of view. We also expect ACL to become a formal framework for analysis, synthesis and transformation of concurrent programs by the use of techniques for traditional logic programming. ACL's attractive features for concurrent programming paradigms are also discussed.