Two Case Studies of Semantics Execution in Maude: CCS and LOTOS

We explore the features of rewriting logic and, in particular, of the rewriting logic language Maude as a logical and semantic framework for representing and executing inference systems. In order to illustrate the general ideas we consider two substantial case studies. In the first one, we represent both the semantics of Milner’s CCS and a modal logic for describing local capabilities of CCS processes. Although a rewriting logic representation of the CCS semantics is already known, it cannot be directly executed in the default interpreter of Maude. Moreover, it cannot be used to answer questions such as which are the successors of a process after performing an action, which is used to define the semantics of Hennessy-Milner modal logic. Basically, the problems are the existence of new variables in the righthand side of the rewrite rules and the nondeterministic application of the semantic rules, inherent to CCS. We show how these problems can be solved in a general, not CCS dependent way by controlling the rewriting process by means of reflection. This executable specification plus the reflective control of rewriting can be used to analyze CCS processes. The same techniques are also used to implement a symbolic semantics for LOTOS in our second case study. The good properties of Maude as a metalanguage allow us to implement a whole formal tool where LOTOS specifications without restrictions in their data types (given as ACT ONE specifications) can be executed. In summary, we present Maude as an executable semantic framework by providing easy-tool-building techniques for a language given its operational semantics.Research supported by CICYT projects Desarrollo Formal de Sistemas Distribuidos (TIC97-0669-C03-01) and Desarrollo Formal de Sistemas Basados en Agentes Móviles (TIC2000-0701-C02-01).     

A transformation system for concurrent processes

Program transformation techniques have been extensively studied in the framework of functional and logic languages, where they were applied mainly to obtain more efficient and readable programs. All these works are based on the Unfold/Fold program transformation method developed by Burstall and Darlington in the context of their recursive equational language. The use of Unfold/Fold based transformations for concurrent languages is a relevant issue that has not yet received an adequate attention. In this paper we define a transformation methodology for CCS. We give a set of general rules which are a specialization of classical program transformation rules, such as Fold and Unfold. Moreover, we define the general form of other rules, “oriented” to the goal of a transformation strategy, and we give conditions for the correctness of these rules. We prove that a strategy using the general rules and a set of goal oriented rules is sound, i.e. it transforms CCS programs into equivalent ones. We show an example of application of our method. We define a strategy to transform, if possible, a full CCS program into an equivalent program whose semantics is a finite transition system. We show that, by means of our methodology, we are able to a find finite representations for a class of CCS programs which is larger than the ones handled by the other existing methods. Our transformational approach can be seen as unifying in a common framework a set of different techniques of program analysis. A further advantage of our approach is that it is based only on syntactic transformations, thus it does not requires any semantic information. Received: 24 April 1997 / 19 November 1997     

An efficiency preorder for processes

A simple efficiency preorder for CCS processes is introduced in whichpq means thatq is at least as fast asp, or more generally,p uses at least as much resources asq. It is shown to be preserved by all CCS contexts except summation and it is used to analyse a non-trivial example: two different implementations of a bounded buffer. Finally we give a sound and complete proof system for finite processes.Most of this work was done while the first author was at the University of Sussex and supported by SERC grant GR/D 97368 of the Science and Engineering Research Council of Great Britain.The second author would like to acknowledge the support of the ESPRIT II Basic Research Action Concur.     

Constructive semantics for instantaneous reactions

This paper presents some results towards a game-theoretic account of the constructive semantics of step responses for synchronous languages, providing a coherent semantic framework encompassing both non-deterministic Statecharts (as per Pnueli & Shalev) and deterministic esterel. In particular, it is shown that esterel arises from a finiteness condition on strategies whereas Statecharts permits infinite games. Beyond giving a novel and unifying account of these concrete languages the paper sketches a general theory for obtaining different notions of constructive responses in terms of winning conditions for finite and infinite games and their characterisation as maximal post-fixed points of functions in directed complete lattices of intensional truth-values.     

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.     

基于源代码扩展信息的细粒度缺陷定位方法

基于信息检索的缺陷定位技术,利用跨语言的语义相似性构造检索模型,通过缺陷报告定位源代码错误,具有方法直观、通用性强的特点.但是由于传统基于信息检索的缺陷定位方法将代码作为纯文本进行处理,只利用了源代码的词汇语义信息,导致在细粒度缺陷定位中面临候选代码语义匮乏产生的准确性低的问题,其结果有用性还有待改进.通过分析程序演化场景下代码改动与缺陷产生间的关系,提出一种基于源代码扩展信息的细粒度缺陷定位方法,以代码词汇语义显性信息及代码执行隐性信息共同丰富源代码语义实现细粒度缺陷定位.利用定位候选点的语义相关上下文丰富代码量,以代码执行中间形式的结构语义实现细粒度代码的可区分,同时以自然语言语义指导基于注意力机制的代码语言表征生成,实现细粒度代码与自然语言间的语义映射,从而实现细粒度缺陷定位方法FlowLocator.实验分析结果表明：与经典的IR缺陷定位方法相比,该方法定位准确性在Top-N排名、平均准确率及平均倒数排名上都有显著提高.     

A set expression based inheritance system

This paper describes a new formalism for inheritance systems, based on the formal semantics of set expressions. Using the formalism, it is possible to define new semantic classes by arbitrary set expressions operating on previously defined classes. Thus generalizing bothIS-A links andIS-NOT-A links and adding the set intersection operation. We present an efficient algorithm which follows these definitions to deduce the properties implied by the inheritance network, i.e., the properties of the classes containing a given element. The application which motivated the development of the formalism, namely semantic disambiguation of natural language, is also described.     

A compact fixpoint semantics for term rewriting systems

This work is motivated by the fact that a “compact” semantics for term rewriting systems, which is essential for the development of effective semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many “semantically useless” elements that can be retrieved from a smaller set of terms. Therefore, in this article, we present a compressed, goal-independent collecting fixpoint semantics that contains the smallest set of terms that are sufficient to describe, by semantic closure, all possible rewritings. We prove soundness and completeness under ascertained conditions. The compactness of the semantics makes it suitable for applications. Actually, our semantics can be finite whereas the big-step semantics is generally not, and even when both semantics are infinite, the fixpoint computation of our semantics produces fewer elements at each step. To support this claim we report several experiments performed with a prototypical implementation.     

Static semantics for normal and disjunctive logic programs

In this paper, we propose a newsemantic framework for disjunctive logic programming by introducingstatic expansions of disjunctive programs. The class of static expansions extends both the classes of stable, well-founded and stationary models of normal programs and the class of minimal models of positive disjunctive programs. Any static expansion of a programP provides the corresponding semantics forP consisting of the set of all sentences logically implied by the expansion. We show that among all static expansions of a disjunctive programP there is always theleast static expansion, which we call thestatic completion ¯P ofP. The static completion¯P can be defined as the least fixed point of a naturalminimal model operator and can be constructed by means of a simpleiterative procedure. The semantics defined by the static completion¯P is called thestatic semantics ofP. It coincides with the set of sentences that are true inall static expansions ofP. For normal programs, it coincides with the well-founded semantics. The class of static expansions represents a semantic framework which differs significantly from the other semantics proposed recently for disjunctive programs and databases. It is also defined for a much broader class of programs.Dedicated to Jack MinkerPartially supported by the National Science Foundation grant # IRI-9313061.     

包含协议和语义的构件一致性验证方法

在基于构件的系统设计中,需要对构件的一致性进行验证。构件的一致性包括语义一致性和协议一致性,已有的一致性验证方法仅支持构件的协议一致性验证。而在实际应用中除了要进行构件的协议一致性验证外,还需要进行其语义一致性验证。为此提出了一种包含协议和语义的构件一致性验证方法。所提方法将方法语义与基于场景的需求规约相结合,使用语义扩展接口自动机模型(SIA)来建模构件的语义和协议信息,使用带有语义约束的UML交互概观图来表示基于场景的需求规约。通过对SIA和带语义约束的UML交互概观图的行为的理论分析,进一步形成了一种一致性验证算法,并用实例来说明其过程。该算法不仅能够检验系统中构件的协议一致性,而且能够检验其语义一致性。该算法中的方法语义包括了该方法参数的类型和详细语义信息,更符合实际应用情形。     

Metric semantics from partial order semantics

In dealing with denotational semantics of programming languages partial orders resp. metric spaces have been used with great benefit in order to provide a meaning to recursive and repetitive constructs. This paper presents two methods to define a metric on a subset of a complete partial order such that is a complete metric spaces and the metric semantics on coincides with the partial order semantics on when the same semantic operators are used. The first method is to add a ‘length’ on a complete partial order which means a function of increasing power. The second is based on the ideas of [11] and uses pseudo rank orderings, i.e. monotone sequences of monotone functions . We show that SFP domains can be characterized as special kinds of rank orderded cpo's. We also discuss the connection between the Lawson topology and the topology induced by the metric. Received 11 July 1995 / 1 August 1996     

Resolving contradictions: A plausible semantics for inconsistent systems

The purpose of a knowledge systemS is to represent the worldW faithfully. IfS turns out to be inconsistent containing contradictory data, its present state can be viewed as a result of information pollution with some wrong data. However, we may reasonably assume that most of the system content still reflects the world truthfully, and therefore it would be a great loss to allow a small contradiction to depreciate or even destroy a large amount of correct knowledge. So, despite the pollution,S must contain a meaningful subset, and so it is reasonable to assume (as adopted by many researchers) that the semantics of a logic system is determined by that of its maximally consistent subsets,mc-subsets. The information contained inS allows deriving certain conclusions regarding the truth of a formulaF inW. In this sense we say thatS contains a certain amount ofsemantic information and provides anevidence of F. A close relationship is revealed between the evidence, the quantity of semantic information of the system, and the set of models of its mc-subsets. Based on these notions, we introduce thesemantics of weighted mc-subsets as a way of reasoning in inconsistent systems. To show that this semantics indeed enables reconciling contradictions and deriving plausible beliefs about any statement including ambiguous ones, we apply it successfully to a series of justifying examples, such as chain proofs, rules with exceptions, and paradoxes.     

Multimedia Data Modeling Through a Semantic View Mechanism

The semantics of multimedia data, which features context-dependency and media-independency, is of vital importance to multimedia applications but inadequately supported by the state-of-the-art database technology. In this paper, we address this problem by proposing MediaView as an extended object-oriented view mechanism to bridge the “semantic gap” between conventional databases and semantics-intensive multimedia applications. This mechanism captures the dynamic semantics of multimedia using a modelling construct named media view, which formulates a customized context where heterogeneous media objects with similar/related semantics are characterized by additional properties and user-defined semantic relationships. Due to the complex ingredients and dynamic application requirements of multimedia databases, it is however difficult for users to define by themselves individual media views in a top–down fashion. To this end, a unique approach of constructing media views logically is devised. In addition, a set of user level operators is defined and implemented to accommodate the specialization and generalization relationships among the views. The usefulness and elegancy of MediaView are demonstrated by its application in a multi-modal information retrieval system. Main part of the work by this Qing Li was done when he was on leave from City University of Hong Kong, HKSAR, China.     

Domain independence and the relational calculus

Several alternative semantics (or interpretations) of the relational (domain) calculus are studied here. It is shown that they all have the same expressive power, i.e., the selection of any of the semantics neither gains nor loses expressive power.Since the domain is potentially infinite, the answer to a relational calculus query is sometimes infinite (and hence not a relation). The following approaches which guarantee the finiteness of answers to queries are studied here:output-restricted unlimited interpretation, domain independent queries, output-restricted finite andcountable invention, andlimited interpretation. Of particular interest is the output-restricted unlimited interpretation—although the output is restricted to the active domain of the input and query, the quantified variables range over the infinite underlying domain. While this is close to the intuitive interpretation given to calculus formulas, the naive approach to evaluating queries under this semantics calls for the impossible task of examining infinitely many values. We describe here a constructiion which, given a queryQ under the output-restricted unlimited interpretation, yields a domain independent queryQ, with length no more than exponential in the length ofQ, such thatQ andQ (under their respective semantics) express the same function.This work supported in part by NSF grants IST-85-11541 and IRI-87-19875Work by this author was also supported in part by NSF grant IRI-9109520     

Code generation for a family of executable modelling notations

We are investigating semantically configurable model-driven engineering (MDE). The goal of this work is a modelling environment that supports flexible, configurable modelling notations, in which specifiers can configure the semantics of notations to suit their needs and yet still have access to the types of analysis tools and code generators normally associated with MDE. In this paper, we describe semantically configurable code generation for a family of behavioural modelling notations. The family includes variants of statecharts, process algebras, Petri Nets, and SDL88. The semantics of this family is defined using template semantics, which is a parameterized structured operational semantics in which parameters represent semantic variation points. A specific notation is derived by instantiating the family’s template semantics with parameter values that specify semantic choices. We have developed a code-generator generator (CGG) that creates a suitable Java code generator for a subset of derivable modelling notations. Our prototype CGG supports 26 semantics parameters, 89 parameter values, and 7 composition operators. As a result, we are able to produce code generators for a sizable family of modelling notations, though at present the performance of our generated code is about an order of magnitude slower than that produced by commercial-grade generators.     

Finite-tree analysis for constraint logic-based languages

Logic languages based on the theory of rational, possibly infinite, trees have much appeal in that rational trees allow for faster unification (due to the safe omission of the occurs-check) and increased expressivity (cyclic terms can provide very efficient representations of grammars and other useful objects). Unfortunately, the use of infinite rational trees has problems. For instance, many of the built-in and library predicates are ill-defined for such trees and need to be supplemented by run-time checks whose cost may be significant. Moreover, some widely used program analysis and manipulation techniques are correct only for those parts of programs working over finite trees. It is thus important to obtain, automatically, a knowledge of the program variables (the finite variables) that, at the program points of interest, will always be bound to finite terms. For these reasons, we propose here a new data-flow analysis, based on abstract interpretation, that captures such information. We present a parametric domain where a simple component for recording finite variables is coupled, in the style of the open product construction of Cortesi et al., with a generic domain (the parameter of the construction) providing sharing information. The sharing domain is abstractly specified so as to guarantee the correctness of the combined domain and the generality of the approach. This finite-tree analysis domain is further enhanced by coupling it with a domain of Boolean functions, called finite-tree dependencies, that precisely captures how the finiteness of some variables influences the finiteness of other variables. We also summarize our experimental results showing how finite-tree analysis, enhanced with finite-tree dependencies, is a practical means of obtaining precise finiteness information.     

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

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

From P2P to reliable semantic P2P systems

Current research to harness the power of P2P networks involves building reliable Semantic Peer-to-Peer (SP2P) systems. SP2P systems combine two complementary technologies: P2P networking and ontologies. There are several types of SP2P systems with applications to knowledge management systems, databases, the Semantic Web, emergent semantics, web services, and information systems. Correct semantic mapping is fundamental for success of SP2P systems where semantic mapping refers to semantic relationship between concepts from different ontologies. Current research on SP2P systems has emphasized semantics at the cost of dealing with the traditional issues of P2P networks of reliability and scalability. As a result of their lack of resilience to temporary mapping faults, SP2P systems can suffer from disconnection failures. Disconnection failures arise when SP2P systems that use adaptive query routing methods treat temporary mapping faults as permanent mapping faults. This paper identifies the disconnection failure problem due to temporary semantic mapping faults and proposes an algorithm to resolve it. To identify the problem, we will use a simulation model of SP2P systems. The Fault-Tolerant Adaptive Query Routing (FTAQR) algorithm proposed to resolve the problem is an adaptation of the generous tit-for-tat method originally developed in evolutionary game theory. The paper demonstrates that the reliability of an SP2P system increases by using the algorithm.     

Broadcast Calculus Interpreted in CCS upto Bisimulation

A function M is given that takes any process p in the calculus of broadcasting systems CBS and returns a CCS process M(p) with special actions {hear?, heard!, say?, said!} such that a broadcast of ω by p is matched by the sequence say? τ^* said(ω) by M(p) and a reception of υ by hear(v) τ^*heard!. It is shown that p M(p), where is a bisimulation equivalence using the above matches, and that M(p) has no CCS behaviour not covered by . Thus the abstraction of a globally synchronising broadcast can be implemented by sequences of local synchronisations. The criteria of correctness are unusual, and arguably stronger than requiring equivalences to be preserved — the latter does not guarantee that meaning is preserved. Since is not a native CCS equivalence, it is a matter of dicussion what the result says about Holmer's (CONCUR'93) conjecture, partially proved by Ene and Muntean (FCT'99), that CCS cannot interpret CBS upto preservation of equivalence.     

Rule Formats for Timed Processes

Building on previous work (15,8), this paper describes two syntactic ways of defining ‘well-behaved’ operational semantics for timed processes. In both cases, the semantic rules are derived from abstract operational rules for behaviour comonads and thus ensure congruence results. The first of them, a light-weight attempt using schematic rules, is shown to be sound, i.e., to indeed induce abstract rules as introduced in [8]. Then a second format, based on a new and very general kind of abstract rules, comonadic SOS (CSOS), is presented which uses meta rules and is also complete, i.e., it characterises all possible CSOS rules for timed processes.