The mathematical concepts and notational conventions we know of as Z were first proposed around 1981. Its origins were in line with the objectives of the PRG - to establish a mathematical basis for program ming ...
详细信息
ISBN:
(数字)9781447138778
ISBN:
(纸本)9783540196273
The mathematical concepts and notational conventions we know of as Z were first proposed around 1981. Its origins were in line with the objectives of the PRG - to establish a mathematical basis for program ming concepts and to verify the work by case studies with industry. Hence among early Z users some were from academic circles, with interests in the mathematical basis of programming; others came from industry and were involved with pilot projects and case studies linked with the programming research group. Four years ago we had the first Z User Meeting, a fairly modest affair with representatives more or less equally divided between academia and industry. At the first meeting there were, as in this meeting, a variety of technical papers, reports of work in progress and discussions. A number of people from industry came along, either because they had begun to use Z or were curious about the new direction. In the discussion sessions at the end of the meeting, there were calls from attendees for the establishment of a more stable base for the notation, including work on its documentation and standards. Many of these requests have now been satisfied and the notation is now being proposed for standards development.
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...
详细信息
The use of global time can simplify the design and description of distributed algorithms. It is, however, an expensive mechanism to implement. In this paper we show that in some cases global time can be assumed while ...
详细信息
The use of global time can simplify the design and description of distributed algorithms. It is, however, an expensive mechanism to implement. In this paper we show that in some cases global time can be assumed while designing an algorithm, but need not be implemented—in these cases it can be replaced with Lamport's logical time in a routine manner, which clearly preserves the correctness of the algorithm. The technique is illustrated by three examples. Two existing algorithms are described as if they had been designed while assuming global time; they are Chandy and Lamport's distributed snapshot algorithm, and Banatre and Lapalme's fair agreement algorithm for the distributed auction system Enchere. The third example is a new distributed algorithm for restarting from a saved checkpoint state. It was designed while assuming global time, but can be implemented without it.
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.
This paper concentrates on the derivation of an operational semantics from an algebraic. First, the transition relation is defined by an inequation, and then the individual clauses of the operational semantics are der...
详细信息
This paper concentrates on the derivation of an operational semantics from an algebraic. First, the transition relation is defined by an inequation, and then the individual clauses of the operational semantics are derived one by one by algebraic reasoning. Consistency is thereby guaranteed, although the question of completeness is left open. The method is illustrated on two languages;one is a large subset of CSP, and the other a notational variant of Dijkstra's Language. A combination of these languages provides a basis for the treatment of the transputer language occam.
In this paper, we develop a compositional denotational semantics for prioritized real-time distributed programming languages. One of the interesting features is that it extends the existing compositional theory propos...
详细信息
In this paper, we develop a compositional denotational semantics for prioritized real-time distributed programming languages. One of the interesting features is that it extends the existing compositional theory proposed by Koymans et al (1988) for prioritized real-time languages preserving the compositionality of the semantics. The language permits users to define situations in which an action has priority over another action without the requirement of preassigning priorities to actions for partially ordering the alphabet of actions. These features are part of the languages such as Ada designed specifically keeping in view the needs of real-time embedded systems. Further, the approach does not have the restriction of other approaches such as prioritized internal moves can preempt unprioritized actions etc. Our notion of priority in the environment is based on the intuition that a low priority action can proceed only if the high priority action cannot proceed due to lack of the handshaking partner at that point of execution. In other words, if some action is possible corresponding to that environment at some point of execution then the action takes place without unnecessary waiting. The proposed semantic theory provides a clear distinction between the semantic model and the execution model - this has enabled us to fully ensure that there is no unnecessary waiting.
作者：
HOARE, CAROxford University
Computing Laboratory Programming Research Group 8-11 Keble Road Oxford OX1 3QD UK
This paper shows how propositional logic may be used to reason about synchronous combinational switching circuits implemented in C-mos. It develops a simple formalism and theory for describing and predicting their beh...
详细信息
This paper shows how propositional logic may be used to reason about synchronous combinational switching circuits implemented in C-mos. It develops a simple formalism and theory for describing and predicting their behaviour. On this it builds a calculus of design which is driven by proof obligations. The design philosophy for software introduced in [1] is thereby extended to a certain kind of hardware design. No prior knowledge of hardware is assumed of the reader;but useful background, motivation, examples and pictures may be found in [2]. Many of the problems described in that paper have been solved in this one.
作者：
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 auxiliary if its members occur only in assignments to members of the same set. Data refinement transforms a program, replacing one set of local variables by another set, in ord...
详细信息
A set of local variables in a program is auxiliary if its members occur only in assignments to members of the same set. Data refinement transforms a program, replacing one set of local variables by another set, in order to move towards a more efficient representation of data. Most techniques of data refinement give a direct transformation. But there is an indirect technique, using auxiliary variables, that proceeds in several stages. Usually, the two techniques are considered separately. It is shown 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 formalised incidentally.
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.
Current processor architectures are diverse and heterogeneous. Examples include multicore chips, GPUs and the Cell Broadband Engine (CBE). The recent Open Compute Language (OpenCL) standard aims at efficiency and port...
详细信息
暂无评论