Several primitives for transaction processing systems are developed using the notations of Communicating Sequential Processes. The approach taken is to capture each requirement separately, in the simplest possible con...
详细信息
Several primitives for transaction processing systems are developed using the notations of Communicating Sequential Processes. The approach taken is to capture each requirement separately, in the simplest possible context: The specification is then the conjunction of all these requirements. As each is developed as a predicate over traces of the observable events in the system, it is also implemented as a simple communicating process; the implementation of the entire system is then merely the parallel composition of these processes. The laws of CSP are then used to transform the system to achieve the required degree of concurrency, to make it suitable for execution in a multiple-tasking system, for example. Finally, there is a discussion of how state-based systems may be developed using this approach together with some appropriate notation for specifying and refining data structures and operations upon them and of how the system may be implemented. This work is intended as a case study in the use of CSP.
This is a continuation of the description of OS6, and it covers the facilities for input/output, and the handling of files on the disc. The input/output system uses a very general form of stream;the filing system is d...
This paper is a description of a simple operating system, which runs in a virtual machine (implemented on a real machine by an interpreter). OS6 copes with only one user at a time, and is not a multi-programming syste...
A process communicates with its environment and with other processes by syncronized output and input on named channels. The current state of a process is defined by the sequences of messages which have passed along ea...
A process communicates with its environment and with other processes by syncronized output and input on named channels. The current state of a process is defined by the sequences of messages which have passed along each of the channels, and by the sets of messages that may next be passed on each channel. A process satisfies an assertion if the assertion is at all times true of all possible states of the process. We present a calculus for proving that a process satisfies the assertion describing its intended behaviour. The following constructs are axiomatised: output; input; simple recursion; disjoint parallelism; channel renaming, connection and hiding; process chaining; nondeterminism; conditional; alternation; and mutual recursion. The calculus is illustrated by proof of a number of simple buffering protocols.
作者：
MORGAN, CComputing Laboratory
Programming Research Group Oxford University 8-11 Keble Road Oxford United Kingdom OXI 3QD
A set of local variables in a program is considered auxiliary if its members occur only in assignments to members of the same set. Data refinement changes a program, replacing one set of local variables by another se...
详细信息
A set of local variables in a program is considered auxiliary if its members occur only in assignments to members of the same set. Data refinement changes a program, replacing one set of local variables by another set, in order to move toward a more efficient representation of data. Most techniques of data refinement give a direct transformation, but there exists an indirect technique, using auxiliary variables, that proceeds in several stages. Generally, the 2 techniques are considered separately. It is demonstrated that the several stages of the indirect technique are themselves special cases of the direct one, thus unifying the separate approaches. Removal of auxiliary variables is formalized incidentally.
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 (1.91.. 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.
We present a basis for the formal specification and stepwise development of distributed systems, i.e. programs which are intended (at least conceptually) to run on distributed-memory parallel machines which communicat...
详细信息
This paper argues that our recent progress in the development of a sound programming methodology should not lead us to ignore the more difficult aspects of engineering;and that in future we should pay more attention t...
详细信息
In ordinary mathematics, an equation can be written down which is syntactically correct, but for which no solution exists. For example, consider the equation x = x + 1.defined over the real numbers; there is no value ...
详细信息
ISBN:
(数字)9781447132035
ISBN:
(纸本)9783540197805
In ordinary mathematics, an equation can be written down which is syntactically correct, but for which no solution exists. For example, consider the equation x = x + 1.defined over the real numbers; there is no value of x which satisfies it. Similarly it is possible to specify objects using the formal specification language Z [3,4], which can not possibly exist. Such specifications are called inconsistent and can arise in a number of ways. Example 1.The following Z specification of a functionf, from integers to integers "f x : ~ 1.x ~ O· fx = x + 1.(i) "f x : ~ 1.x ~ O· fx = x + 2 (ii) is inconsistent, because axiom (i) gives f 0 = 1. while axiom (ii) gives f 0 = 2. This contradicts the fact that f was declared as a function, that is, f must have a unique result when applied to an argument. Hence no suchfexists. Furthermore, iff 0 = 1.andfO = 2 then 1.= 2 can be deduced! From 1.= 2 anything can be deduced, thus showing the danger of an inconsistent specification. Note that all examples and proofs start with the word Example or Proof and end with the symbol.1.
暂无评论