Non-Standard Semantics for Program Slicing

In this paper we generalize the notion of compositional semantics to cope with transfinite reductions of a transition system. Standard denotational and predicate transformer semantics, even though compositional, provide inadequate models for some known program manipulation techniques. We are interested in the systematic design of extended compositional semantics, observing possible transfinite computations, i.e. computations that may occur after a given number of infinite loops. This generalization is necessary to deal with program manipulation techniques modifying the termination status of programs, such as program slicing. We include the transfinite generalization of semantics in the hierarchy developed in 1997 by P. Cousot, where semantics at different levels of abstraction are related with each other by abstract interpretation. We prove that a specular hierarchy of non-standard semantics modeling transfinite computations of programs can be specifiedin such a way that the standard hierarchy can be derived by abstract interpretation. We prove that non-standard transfinite denotational and predicate transformer semantics can be both systematically derived as solutions of simple abstract domain equations involving the basic operation of reduced power of abstract domains. This allows us to prove the optimality of these semantics, i.e. they are the most abstract semantics in the hierarchy which are compositional and observe respectively the terminating and initial states of transfinite computations, providing an adequate mathematical model for program manipulation.     

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.     

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.     

补偿通信顺序进程的扩展及失败发散语义

补偿通信顺序进程(cCSP)是通信顺序进程用于长事务建模的扩展,可用来描述服务计算中的编制程序,比如WS-BPEL程序。目前,cCSP只有操作语义和基于迹的指称语义,对死锁和发散行为的推理支持不够。本文扩展了cCSP,引入新的组合操作子,给出扩展cCSP的失败发散语义;并根据该语义,给出新引入组合操作子的重要代数规则,用于语义的理解和佐证。最后,给出一个案例描述用于展示扩展cCSP。     

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.     

Defining the meaning of tabular mathematical expressions

Mathematical expressions in tabular form (also called “tabular expressions” or “tables”) have been shown to be useful for documenting and analysing software systems. They are usually easier to read than conventional mathematical expressions but are no less precise. They can be used wherever mathematical expressions are used. To avoid misunderstandings, and to support users with trustworthy tools, the meaning of these expressions must be fully defined.This paper presents a new method for defining the meaning of tabular expressions. Each definition of an expression type names the expression’s constituents, and provides a restriction schema and one or more evaluation schemas. The restriction schema defines the class of well-formed expressions of the type. An evaluation schema maps a well-formed tabular expression of the type to a mathematical expression of a previously defined type. Since the meaning of conventional mathematical expressions is well known, describing an equivalent expression fully defines the meaning of a tabular expression.In this approach, indexation is used to decouple the appearance of a tabular expression from its semantics. A tabular expression is an indexed set of grids; a grid is an indexed set of expressions. The expressions in a grid can be either conventional expressions or tabular expressions of a previously defined type.Defining the meaning of a tabular expression in this way facilitates the building of tools that faithfully implement the semantics. The decoupling of syntax and semantics by means of indices overcomes some limitations of older approaches.The method presented in the paper is illustrated by defining several previously known types of tabular expressions and some new ones. The use of the new model to build a suite of tools for the input, presentation, validation, evaluation, simplification, conversion and composition of tabular expressions is discussed.     

Failure-based equivalence of constraint automata

Constraint automata are the first-proposed operational semantics of Reo coordination language. They can be composed not only by all well-defined composition operators of labeled transition systems but also by two new operators. The new operators are joining of constraint automata with respect to their common port names and hiding a port name in all transition labels. The operations of these two extra operators depend on the internal structures of the transition labels, while in the others each transition label is considered as a simple entity. An equivalence relation between transition systems is a congruence relation if the replacement of the components of a model by the equivalent ones always yields a model that is equivalent with the original one. Obviously, this definition of the congruency depends on the operators which are used to compose the components of models. This paper introduces four congruency results: we prove that failure-based equivalence relation CFFD (chaos-free failures divergences relation) is a congruence relation with respect to joining of constraint automata and also with respect to hiding port names in a constraint automaton. We also show that these are cases for equivalence relation NDFD (non-divergent failures divergences).     

目标独立的Prolog程序路径依赖分析语义

在Prolog程序分析中,考虑程序的执行路径和非逻辑的cut操作可提高程序分析的精度.当前用于Prolog程序路径依赖分析的语义因依赖于程序执行的目标而不适合目标独立的程序分析.为此,本文采用了一种携带路径信息并允许cut操作的Prolog抽象语法,在此基础上给出了Prolog的操作语义和一种目标独立的标号树(LT)语文,并证明了LT语义相对于操作语义的正确性.LT语义可作为目标独立的Prolog程序路径依赖分析的基础.     

Equivalence of formal semantics definition methods

There are numerous methods of formally defining the semantics of computer languages. Each method has been designed to fulfil a different purpose. For example, some have been designed to make reasoning about languages as easy as possible; others have been designed to be accessible to a large audience and some have been designed to ease implementation of languages. Given two semantics definitions of a language written using two separate semantics definition methods, we must be able to show that the two are in fact equivalent. If we cannot do this then we either have an error in one of the semantics definitions, or more seriously we have a problem with the semantics definition methods themselves.Three methods of defining the semantics of computer languages have been considered, i.e. Denotational Semantics, Structural Operational Semantics and Action Semantics. An equivalence between these three is shown for a specific example language by first defining its semantics using each of the three definition methods. The proof of the equivalence is then constructed by selecting pairs of the semantics definitions and showing that they define the same language.A full version of this paper can be accessed via our web page http://www.cs.man.ac.uk/fmethods/ facj.html     

一种基于模块单子语义的动态程序切片方法

提出一种基于程序模块单子语义的新动态切片方法--模块单子动态切片.首先通过单子转换器,将切片这一类计算抽象成独立于具体语言的实体：切片单子转换器.然后,将该切片转换器作为模块加载到实际程序中,并给出相应的模块单子动态切片算法.据此,可直接在抽象语法结构上计算动态切片,不必记录程序执行历史;相应单子切片器也无需显式地构造诸如依赖图的中间结构.这种模块化抽象机制使得文中的动态切片算法具有很强的可扩展性和重用性.     

A non-standard semantics for program slicing and dependence analysis

We introduce a new non-strict semantics for a simple while language. We demonstrate that this semantics allows us to give a denotational definition of variable dependence and neededness, which is consistent with program slicing. Unlike other semantics used in variable dependence, our semantics is substitutive. We prove that our semantics is preserved by traditional slicing algorithms.     

Enabling metrology-oriented specification of geometrical variability – A categorical approach

In this paper a metrology-oriented specification schema is proposed to enrich the specification semantics with sufficient metrological information. It is designed particularly for applications where non-traditional measurement methods are applied; and it can also identify any redundancies, inconsistencies or incompletenesses of a specification. The proposed schema is based on category theoretical semantics which uses category theory as the foundation to model the semantics. A set of verification operations that derived from the measurement process was firstly formalised using the categorical semantics. Then a set of full faithful functors were constructed to map the set of verification operations to a set of specification operations. A set of simplification rules was then developed to deduce all of the necessary specification objects which are independent to each other. Then the residual specification objects provide a compact structure of the specification. Three test cases were conducted to validate the proposed schema. An industrial computed tomography (CT) measurement process for an impeller manufacturing using selective laser sintering (SLS) technique, was modelled and a set of independent specification elements was then deduced. The other two test cases for checking redundancy and incompleteness on general ISO specifications were carried out. The results show that the proposed schema works for proposing semantic enriched specification that are characterised by non-traditional measurement methods and for testing redundancy and incompleteness of specifications based on geometrical product specifications and verification (GPS) standards system.     

Partial ordering models for concurrency can be defined operationally

Labelled rewriting systems are shown to be powerful enough for defining the semantics of concurrent systems in terms of partial orderings of events, even in the presence of non standard operators like N that is not expressible by means of concurrency and sequentialization. This contrasts with Pratt's claim.⁽¹⁾ The main operators proposed by Pratt are used here to construct terms denoting concurrent systems, the behavior of which consists of partially ordered multisets defined operationally.⁽²⁾ Fully abstractness of the denotational semantics as defined in Ref. 1 with respect to the operational one is finally proved.     

Enhancing ebXML Registries to Make them OWL Aware

ebXML is a standard from OASIS and UN/CEFACT which specifies an infrastructure to facilitate electronic business. In this paper, we address how ebXML registry semantics support can be further enhanced to make it OWL aware. OWL constructs are represented through ebXML registry information model constructs, and stored procedures are defined in the ebXML registry for processing the OWL semantics. These predefined stored queries provide the necessary means to exploit the enhanced semantics stored in the registry. In this way, an application program does not have to be aware of the details of how this semantics support is achieved in ebXML registry, and does not have to contain additional code to process this semantics.We believe that this approach is quite powerful to associate semantics with registry objects: it becomes possible to retrieve knowledge through queries, the enhancements to the registry are generic and also the registry specification is kept intact. The capabilities provided move the semantics support beyond what is currently available in ebXML registries and it does so by using a standard ontology language.To be able to demonstrate the benefits of the enhancements, we also show how the resulting semantics can be made use of in Web service discovery and composition.Recommended by: Athman Bouguettaya and Boualem BenatallahThis work is supported in part by the European Commission, Project No: IST-1-002104-STP SATINE and the Scientific and Technical Research Council of Turkey (TÜBÍTAK), Project No: EEEAG 104E013 and is realized as a proposal to OASIS ebXML Semantic Content Management subcommittee which is working on possible semantic extensions to the registry.     

SLT-Resolution for the Well-Founded Semantics

Global SLS-resolution and SLG-resolution are two representative mechanisms for top-down evaluation of the well-founded semantics of general logic programs. Global SLS-resolution is linear for query evaluation but suffers from infinite loops and redundant computations. In contrast, SLG-resolution resolves infinite loops and redundant computations by means of tabling, but it is not linear. The principal disadvantage of a nonlinear approach is that it cannot be implemented by using a simple, efficient stack-based memory structure nor can it be easily extended to handle some strictly sequential operators such as cuts in Prolog. In this paper, we present a linear tabling method, called SLT-resolution, for top-down evaluation of the well-founded semantics. SLT-resolution is a substantial extension of SLDNF-resolution with tabling. Its main features are the following. First, it resolves infinite loops and redundant computations while preserving the linearity. Second, it is terminating and is sound and complete w.r.t. the well-founded semantics for programs with the bounded-term-size property with nonfloundering queries. Its time complexity is comparable with SLG-resolution and polynomial for function-free logic programs. Third, because of its linearity for query evaluation, SLT-resolution bridges the gap between the well-founded semantics and standard Prolog implementation techniques. It can be implemented by an extension to any existing Prolog abstract machines such as WAM or ATOAM.     

Functional semantics of programs with exceptions

Linguistic mechanisms for exception handling facilitate the production of reliable software and play an important role in fault tolerant computing. This paper describes the functional semantics of a Pascal-like language which supports exception handling and data abstraction. A program with exceptions is considered as having a standard semantics, as well as an exceptional semantics for each exception that may be signaled during its execution. Standard functional semantics methods provide rules to obtain the function representing the standard semantics. In this paper, we provide rules to determine the functions representing the exceptional semantics. We also describe a method for specifying and verifying the correctness of implementation of data types with exceptions.     

汉语逻辑补足义标注框架研究

逻辑补足义是指附加在以谓词为中心的基本命题成分之上的否定、程度、时体、模态和语气等, 具体表现为逻辑语义算子对谓词的语义约束关系,是基本命题成分所表达语义关系的有效补充。在句子中,逻辑补足义所表达的语义是句子深度语义理解的重要层面。该文以深层语义理解为目标,在逻辑补足义已有的研究基础上,建立了否定、程度、时体和语气分类体系,构建了相应的算子词典;制定标注规范,对已经标注了基本命题义语义角色的句子进行各类逻辑补足义的标注;最后,对标注的结果进行统计并对标注过程中出现的问题进行了分析。     

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.     

Infinitary rewriting: closure operators, equivalences and models

Infinitary Term Rewriting allows to express infinite terms and transfinite reductions that converge to those terms. Underpinning the machinery of infinitary rewriting are closure operators on relations that facilitate the formation of transfinite reductions and transfinite equivalence proofs. The literature on infinitary rewriting has largely neglected to single out such closure operators, leaving them implicit in definitions of (transfinite) rewrite reductions, or equivalence relations. This paper unpicks some of those definitions, extracting the underlying closure principles used, as well as constructing alternative operators that lead to alternative notions of reduction and equivalence. A consequence of this unpicking is an insight into the abstraction level at which these operators can be defined. Some of the material in this paper already appeared in Kahrs (2010). The paper also generalises the notion of equational model for infinitary rewriting. This leads to semantics-based notions of equivalence that tie in with the equivalences constructed from the closure operators.