This paper demonstrates how reduction to normal form can help in the design of a correct compiler for Dijkstra's guarded command language. The compilation strategy is to transform a source program, by a series of ...
This paper demonstrates how reduction to normal form can help in the design of a correct compiler for Dijkstra's guarded command language. The compilation strategy is to transform a source program, by a series of algebraic manipulations, into a normal form that describes the behaviour of a stored-program computer. Each transformation eliminates high-level language constructs in favour of lower-level constructs. The correctness of the compiler follows from the correctness of each of the algebraic transformations.
Modern functional programming languages and specification formalisms are built around the notion of inductive data types and homomorphisms on these data types. Such homomorphisms, which correspond to the familiar fol...
详细信息
Modern functional programming languages and specification formalisms are built around the notion of inductive data types and homomorphisms on these data types. Such homomorphisms, which correspond to the familiar fold or reduce operators in functional programming, are called catamorphisms. It is shown how catamorphisms can be generalized from functions to relations and from relations to predicate transformers. The first step of this generalization, from functions to relations, was achieved in a slightly different setting by Backhouse, de Bruin, Malcolm, Voermans, and van der Woulde (1991). In practical terms, the main result of this analysis is that a calculus based on predicate transformers can be enriched with program constructors for iterating over inductive data types. The refinement calculus did already allow a notion of inductive data types, but until now it lacked the program constructors that are associated with such data types, namely catamorphisms.
The sliding-window protocol is specified using the notation of Communicating Sequential Processes and its partial correctness is proved using the trace semantics. First the stop-and-wait protocol is defined;its correc...
详细信息
The sliding-window protocol is specified using the notation of Communicating Sequential Processes and its partial correctness is proved using the trace semantics. First the stop-and-wait protocol is defined;its correctness, that it forms a 1-place buffer, is almost evident. Next the alternating-bit protocol is defined and described in terms of the stop-and-wait protocol, and its correctness deduced from that of the stop-and-wait protocol. Finally the sliding-window protocol is described in terms of the alternating-bit protocol and its correctness deduced accordingly. The paper has two thrusts: that modularity of a specification helps to structure proofs about it (in this case, proofs that the protocols implement buffers);and that refinement in CSP leads to structured, correct implementation in occam. In support of the latter point the appendix contains a refinement and implementation of the protocols in occam 2.
An overview is given of D-I algebra, an algebra for the specification of the safety and progress properties of delay-insensitive circuits in terms of voltage-level transitions on wires. The algebraic laws make it poss...
详细信息
The carrier-null message approach to conservative distributed discrete-event simulation can significantly reduce the number of synchronization messages required to avoid deadlock. In thts paper we show that the origin...
详细信息
ISBN:
(纸本)1565550277
The carrier-null message approach to conservative distributed discrete-event simulation can significantly reduce the number of synchronization messages required to avoid deadlock. In thts paper we show that the original approach does not apply to simulations with arbitrary communication graphs and we propose a modified carrier-null approach whtch does. We present and discuss some preliminary results obtained using our approach to simulate digital logic circuits.
作者：
Bowen, JonathanOxford University
Computing Laboratory Programming Research Group Oxford OX1 3QD 11 Keble Road United Kingdom
A compiler may be specified by a description of how each construct of the source language is translated into a sequence of object code instructions. It is possible to produce a compiler prototype almost directly from ...
详细信息
Dynamic programming is a strategy for solving optimisation problems. In this paper, we show how many problems that may be solved by dynamic programming are instances of the same abstract specification. This specificat...
Dynamic programming is a strategy for solving optimisation problems. In this paper, we show how many problems that may be solved by dynamic programming are instances of the same abstract specification. This specification is phrased using the calculus of relations offered by topos theory. The main theorem underlying dynamic programming can then be proved by straightforward equational reasoning.
This volume contains papers from the Eighth Z User Meeting, to be held at the University of Cambridge from 29 - 30 June 1994. The papers cover a wide range of issues associated with Z and formal methods, with particul...
详细信息
ISBN:
(数字)9781447134527
ISBN:
(纸本)9783540198840
This volume contains papers from the Eighth Z User Meeting, to be held at the University of Cambridge from 29 - 30 June 1994. The papers cover a wide range of issues associated with Z and formal methods, with particular reference to practical application. These issues include education, standards, tool support, and interaction with other design paradigms such as consideration of real-time and object-oriented approaches to development. Among the actual topics covered are: the formal specification in Z of Defence Standard 00-56; formal specification of telephone features; specifying and interpreting class hierarchies in Z; and software quality assurance using the SAZ method.;provides an important overview of current research into industrial applications of Z, and will provide invaluable reading for researchers, postgraduate students and also potential industrial users of Z.
Operations on action systems may be defined corresponding to CSP hiding and renaming. These are of particular use in describing the refinement between action systems in which the granularity of actions is altered. We ...
详细信息
暂无评论