The Z notation has been developed at the programmingresearchgroup at the Oxford University computinglaboratory and elsewhere for over a decade. It is now used by industry as part of the software (and hardware) deve...
详细信息
ISBN:
(数字)9781447135562
ISBN:
(纸本)9783540198185
The Z notation has been developed at the programmingresearchgroup at the Oxford University computinglaboratory and elsewhere for over a decade. It is now used by industry as part of the software (and hardware) development process in both Europe and the USA. It is currently undergoing BSI standardisation in the UK, and has been proposed for ISO standardisation internationally. In recent years researchers have begun to focus increasingly on the development of techniques and tools to encourage the wider application of Z and other formal methods and notations. This volume contains papers from the Seventh Annual Z User Meeting, held in London in December 1992. In contrast to previous years the meeting concentrated specifically on industrial applications of Z, and a high proportion of the participants came from an industrial background. The theme is well represented by the four invited papers. Three of these discuss ways in which formal methods are being introduced, and the fourth presents an international survey of industrial applications. It also provides a reminder of the improvements which are needed to make these methods an accepted part of software development. In addition the volume contains several submitted papers on the industrial use of Z, two of which discuss the key area of safety-critical applications. There are also a number of papers related to the recently-completed ZIP project. The papers cover all the main areas of the project including methods, tools, and the development of a Z Standard, the first publicly-available version of which was made available at the meeting. Finally the volume contains a select Z bibliography, and section on how to access information on Z through ***.z, the international, computer-based USENET newsgroup.;provides an important overview of current research into industrial applications of Z, and will provide invaluable reading for researchers, postgraduate students andalso potential industrial users of Z.
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.
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 *** generic specification of dynamic programming makes use of higher-order operators on relations, akin to the fold operators found in functional programming languages. In the present context, a data type is modelled as an initial F-algebra, where F is an endofunctor on the topos under consideration. The mediating arrows from this initial F-algebra to other F-algebras are instances of fold – but only for total functions. For a regular category ε, it is possible to construct a category of relations Rel(ε). When a functor between regular categories is a so-called relator, it can be extended (in some canonical way) to a functor between the corresponding categories of relations. Applied to an endofunctor on a topos, this process of extending functors preserves initial algebras, and hence fold can be generalised from functions to *** is well-known that the use of dynamic programming is governed by the principle of optimality. Roughly, the principle of optimality says that an optimal solution is composed of optimal solutions to subproblems. In a first attempt, we formalise the principle of optimality as a distributivity condition. This distributivity condition is elegant, but difficult to check in practice. The difficulty arises because we consider minimum elements with respect to a preorder, and therefore minimum elements are not unique. Assuming that we are working in a Boolean topos, it can be proved that monotonicity implies distributivity, and this monotonicity condition is easy to verify in practice.
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 ...
详细信息
暂无评论