Predicate-transformer semantics of general recursion

Summary We develop the semantics of a language with arbitrary atomic statements, unbounded nondeterminacy, and mutual recursion. The semantics is expressed in weakest preconditions and weakest liberal preconditions. Individual states are not mentioned. The predicates on the state space are treated as elements of a distributive lattice. The semantics of recursion is constructed by means of the theorem of Knaster-Tarski. It is proved that the law of the excluded miracle can be preserved, if that is wanted. The universal conjunctivity of the weakest liberal precondition, and the connection between the weakest precondition and the weakest liberal precondition are proved to remain valid. Finally we treat Hoare-triple methods for proving correctness and conditional correctness of programs.     

Temporal predicate transformers and fair termination

Summary It is usually assumed that implementations of nondeterministic programs may resolve the nondeterminacy arbitrarily. In some circumstances, however, we may wish to assume that the implementation is in some sense fair, by which we mean that in its long-term behaviour it does not show undue bias in forever favouring some nondeterministic choices over others. Under the assumption of fairness many otherwise failing programs become terminating. We construct various predicate transformer semantics of such fairly-terminating programs. The approach is based on formulating the familiar temporal operators always, eventually, and infinitely often as predicate transformers. We use these operators to construct a framework that accommodates many kinds of fairness, including varieties of socalled weak and strong fairness in both their all-levels and top-level forms. Our formalization of the notion of fairness does not exploit the syntactic shape of programs, and allows the familiar nondeterminacy and fair nondeterminacy to be arbitrarily combined in the one program. Invariance theorems for reasoning about fairly terminating programs are proved. The semantics admits probabilistic implementations provided that unbounded fairness is excluded.     

Dual unbounded nondeterminacy,recursion, and fixpoints

In languages with unbounded demonic and angelic nondeterminacy, functions acquire a surprisingly rich set of fixpoints. We show how to construct these fixpoints, and describe which ones are suitable for giving a meaning to recursively defined functions. We present algebraic laws for reasoning about them at the language level, and construct a model to show that the laws are sound. The model employs a new kind of power domain-like construct for accommodating arbitrary nondeterminacy.     

Command algebras,recursion and program transformation

Dijkstra's language of guarded commands is extended with recursion and transformed into algebra. The semantics is expressed in terms of weakest preconditions and weakest liberal preconditions. Extreme fixed points are used to deal with recursion. Unbounded nondeterminacy is allowed. The algebraic setting enables us to develop efficient transformation rules for recursive procedures. The main result is an algebraic version of the rule of computational induction. In this version, certain parts of the programs are restricted to finite nondeterminacy. It is shown that without this restriction the rule would not be valid. Some applications of the rule are presented. In particular, we prove the correctness of an iterative stack implementation of a class of simple recursive procedures.     

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.     

Modelling higher-order dual nondeterminacy

We investigate models for programming and specifying in which higher-order functions and nondeterminacy (both demonic and angelic) coexist. The models are built using predicate transformers, binary multirelations, state transformers, and free lattices over a poset. We show there exist suitable models in each approach, and that they are isomorphic. The models support an algebra of nondeterminacy which we use to prove that the classical list fusion law holds even in the presence of nondeterminacy.     

The fixed point theory of unbounded non-determinism

This paper presents a fixed point theorem for the infinite traces model of CSP. Unlike any other model of CSP, there is no complete partial order over the infinite traces model whose fixed point theory agrees with the operational semantics (A. W. Roscoe, Oxford University Computing Laboratory Technical Monograph PRG-67, 1988). This arises from the introduction of unbounded non-determinism. However, the subset of pre-deterministic processes, that is those which describe the behaviour of a process on some run of its implementation, do form a subset for which the usual order is complete. By requiring that each CSP operator has a monotonic implementation which preserves pre-determinism, it is possible to show that all CSP operators have a least fixed point. In effect, it is the requirement that all operators have a methodical implementation.The author carried out the research for this paper on the Espirit Genesis project at the Programming Research Group, Oxford University.     

A treatment of unbounded dependencies in eurotra with an experimental coindexation tool

The purpose of this article is to present a treatment of unbounded dependencies which is currently being experimented with in Eurotra. The treatment is based on the coindexation tool designed by the authors as an extension to the E-Framework, Eurotra's NLP formalism. At present, the tool has been tested in a systematic way in the Danish, French, Italian, and Spanish modules of the Eurotra translation system. Testing work on other languages (especially German) is in progress. Our article is organized as follows: in section 1, we discuss the linguistic and translational motivations for the treatment presented here; in section 2, we give the syntax and semantics of the two main components of the coindexation tool, namely the recursion markers and the copy operator; section 3 shows how this machinery can be applied for the implementation of unbounded dependency constructions according to our approach.

---

     

Combining angels, demons and miracles in program specifications

The complete lattice of monotonic predicate transformers is interpreted as a command language with a weakest precondition semantics. This command lattice contains Dijkstra's guarded commands as well as miracles. It also permits unbounded nondeterminism and angelic nondeterminism. The language is divided into sublanguages using criteria of demonic and angelic nondeterminism, termination and absence of miracles. We investigate dualities between the sublanguages and how they can be generated from simple primitive commands. The notions of total correctness and refinement are generalized to the command lattice.     

Consistency in dataflow graphs

Analytical properties of programming languages with dataflow graph semantics are discussed. It is shown that one of the most serious problems with these languages is that subtle inconsistencies between parts of the dataflow graph can be inadvertently created. These inconsistencies can lead to deadlock, or in the case of nonterminating programs, to unbounded memory requirements. Consistency is defined to mean that the same number of tokens is consumed as produced on any arc, in the long run. A token-flow model is developed for testing for inconsistency. The method is a generalization of consistency checks for synchronous dataflow (SDF) graphs. The token-flow model is compared to similar tests applied to hybrid dynamical systems. It is argued that dataflow semantics make steady-state analysis possible, leading to a simpler method in most cases     

Predicate Transformers for Recursive Procedures with Local Variables

The weakest precondition semantics of recursive procedures with local variables are developed for an imperative language with demonic and angelic operators for unbounded nondeterminate choice. This does not require stacking of local variables. The formalism serves as a foundation for a proof rule for total correctness of (mutually) recursive procedures with local variables. This rule is illustrated by a simple example. Its soundness is proved for arbitrary well-founded variant functions. Received March 1999 / Accepted in revised form January 2000     

A theory of bunches

A bunch is a simple data structure, similar in many respects to a set. However, bunches differ from sets in that the data is not packaged up or encapsulated, and in particular in that a bunch consisting of one element is the same as that element. Bunches are attractive for handling nondeterminacy and underspecification, by which is meant that for any particular input to the program or specification, the associated output is not fully determined. The acceptable outputs for any given input can be described by a bunch. This approach nicely generalises traditional single-output programs and specifications. We present a formal theory of bunches. It includes an axiomatisations of boolean and function types whose behaviour is well-known to be complicated by the presence of nondeterminacy. The axiomatisation of the booleans preserves most of the laws of classical predicate calculus. The axiomatisation of functions accommodates higher-order functions in all their generality, while avoiding the dangers of inconsistency when functions and nondeterminacy intermix. Our theory is presented as a Hilbert-style system of axioms and inference rules for a small specification language. We prove consistency. Received: 23 December 1998 / 2 November 1999     

Wait-free linearization with an assertional proof

Summary Given a sequential implementation of an arbitrary data object, a wait-free, linearizable concurrent implementation is constructed with space complexity quadratic in the number of processes. If processes do not concurrently invoke, the amortized time complexity of the invocations is independent of the number of processes. The worst case time complexity is linear in the number of processes. The construction is based on a compare&swap register. The correctness is proved by means of invariants and stability properties. Since it concerns memory reallocation by concurrent processes in a fault-tolerant setting, this proof is highly nontrivial. Wim H. Hesselink received his Ph.D. in mathematics from the University of Utrecht in 1975. After ten years of research in algebraic groups he turned to computer science. Since 1985 he has been an associate profesoor with the Department of Computing Science at the University of Groningen. In 1986/1987 he was on sabbatical leave with the Department of Computer Sciences of the University of Texas at Austin. His research interests include aspects and modalities of nondeterminacy, predicate transformation semantics, distributed programming, design and correctness of algorithms, and mechanical theorem proving.     

基于函数式语义的循环和递归程序结构通用证明技术

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.     

Goto and Concurrency Introducing Safe Jumps in Esterel

Esterel is a design language for the specification of real time embedded systems. Based on the synchronous concurrency paradigm, its semantics describes execution as a succession of instants of computation. In this work, we consider the introduction of a new gotopause instruction in the language, which acts as a non-instantaneous jump instruction compatible with concurrency. It allows the programmer to activate state control points anywhere in the program, from where the execution is resumed in the next instant. In order to provide the formal semantics of the extended language, we first define a state semantics of Esterel, which we prove observationally equivalent to the original logical behavioral semantics. Including gotopause in the state semantics is then straightforward. We sketch two key applications of our new primitive: a direct encoding of automata and a quasi-linear rewriting of programs eliminating schizophrenic behaviors.     

Meaning representation in Montague grammar and situation semantics1

This paper compares certain aspects of situation semantics and Montague grammar and points out some issues related to natural language programming. It provides and introduction to certain basic concepts of situation semantics and makes some tentative claims about possible advantages of situation semantics.     

Virtual Tree: A robust architecture for interval valid queries in dynamic distributed systems

This paper studies the problem of answering aggregation queries, satisfying the interval validity semantics, in a distributed system prone to continuous arrival and departure of participants. The interval validity semantics states that the query answer must be calculated considering contributions of at least all processes that remained in the distributed system for the whole query duration. Satisfying this semantics in systems experiencing unbounded churn is impossible due to the lack of connectivity and path stability between processes. This paper presents a novel architecture, namely Virtual Tree, for building and maintaining a structured overlay network with guaranteed connectivity and path stability in settings characterized by bounded churn rate. The architecture includes a simple query answering algorithm that provides interval valid answers. The overlay network generated by the Virtual Tree architecture is a tree-shaped topology with virtual nodes constituted by clusters of processes and virtual links constituted by multiple communication links connecting processes located in adjacent virtual nodes. We formally prove a bound on the churn rate for interval valid queries in a distributed system where communication latencies are bounded by a constant unknown by processes. Finally, we carry out an extensive experimental evaluation that shows the degree of robustness of the overlay network generated by the virtual tree architecture under different churn rates.     

Algebraic and operational semantics of specifications allowing exceptions and errors

The specification of abstract data types requires the possibility to treat exceptions and errors. We present an approach allowing all forms of error handling: error introduction, error propagation and error recovery. The algebraic semantics of our method and a new correctness criterion are given. We also introduce an operational semantics of a subclass of our specifications which coincides with the algebraic semantics.     

产品语义学在包装设计中的应用

本文把产品领域的产品语义学理论引入到包装设计中来,寻求其在包装设计中应用的可能性和前景。通过相关的分析和讨论,发现产品语义学在包装设计领域也是完全适用和可行的。产品语义学的引入为包装设计提供了新的观念和方法,开拓了包装设计新的领域,为包装设计的创新和实践提供了新的理论依据。