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.
One of the attractive features of occam is the large number of memorable algebraic laws which exist relating programs. We investigate these laws and, by discovering a normal form for WHILE-free programs, show that the...
详细信息
One of the attractive features of occam is the large number of memorable algebraic laws which exist relating programs. We investigate these laws and, by discovering a normal form for WHILE-free programs, show that they completely characterise the language's semantics.
The two models presented in this paper provide two different semantics for an extension of Dijkstra's language of guarded commands. The extended language has an additional operator, namely probabilistic choice, wh...
详细信息
The two models presented in this paper provide two different semantics for an extension of Dijkstra's language of guarded commands. The extended language has an additional operator, namely probabilistic choice, which makes it possible to express randomized algorithms. An earlier model by Claire Jones included probabilistic choice but not non-determinism, which meant that it could not be used for the development of algorithms from specifications. Our second model is built on top of Claire Jones' model, using a general method of extending a probabilistic cpo to one which also contains non-determinism. The first model was constructed from scratch, as it were, guided only by the desire for certain algebraic properties of the language constructs, which we found lacking in the second model. We compare and contrast the properties of the two models both by giving examples and by constructing mappings between them and the non-probabilistic model. On the basis of this comparison we argue that, in general, the first model is preferable to the second. (C) 1.97 Elsevier Science B.V.
In this paper we present two languages that are refinements of timed CSP (Davies and Schneider, this volume): a probabilistic language, and a fully deterministic language with a notion of priority. In the first part o...
详细信息
In this paper we present two languages that are refinements of timed CSP (Davies and Schneider, this volume): a probabilistic language, and a fully deterministic language with a notion of priority. In the first part of the paper we describe the deterministic language and its semantic model. The syntax is based upon that of timed CSP except some of the operators are refined so as to remove all nondeterminism;this produces prioritized operators. The semantics for our language represents a process as the set of possible behaviours for the process, where a behaviour models the priorities for different actions. A number of algebraic laws for our language are given and the model is illustrated with two examples. In the second part of the paper, we extend the language by adding a probabilistic choice operator. We produce a semantic model for our language which gives the probabilities of different behaviours occurring, as well as modelling the relative priorities for events within a behaviour. The model is illustrated with an example of a communications protocol transmitting messages over an unreliable medium.
General purpose parallel computing systems come in a variety of forms. We have various kinds of distributed memory architectures, shared memory multiprocessors, and clusters of workstations. New technologies may incre...
详细信息
General purpose parallel computing systems come in a variety of forms. We have various kinds of distributed memory architectures, shared memory multiprocessors, and clusters of workstations. New technologies may increase this range still further. Can one hope to design portable and scalable parallel software in the face of such architectural diversity? In this paper we show that it is indeed possible to produce fully portable parallel software which will run with highly efficient, scalable and predictable performance on any general purpose parallel architecture. The approach we describe is based on the bulk synchronous parallel (BSP) model of computation. The BSP model provides a simple, unified framework for the design and {1. of all kinds of general purpose parallel systems. Over the last few years, a number of important research activities in algorithms and architectures have been pursued as part of this new approach to scalable parallel computing. In this paper we give some simple BSP algorithms and show how they can be expressed as programs. We also briefly describe some of the BSP {1. language developments which are now being pursued.
作者：
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.
There is a general agreement among theoretical computing scientists that a {1. language, or its underlying computational paradigm, may be clarified by a mathematical investigation of its formal semantics. The...
详细信息
There is a general agreement among theoretical computing scientists that a {1. language, or its underlying computational paradigm, may be clarified by a mathematical investigation of its formal semantics. There are at least 3 approaches to the definition of the required semantics. The algebraic approach is presented as a group of algebraic equations, like the axioms of group theory. The derivation of operational semantics from algebraic laws is examined. 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 2 languages. One is a large subset of CSP, while the other is a notational variant of Dijkstra's Language. A combination of these languages provides a basis for the treatment of the transputer language OCCAM.
We study 2- and 3-dimensional digital geometry in the context of almost arbitrary adjacency relations. (Previous authors have based their work on particular adjacency relations). We define a binary digital picture to ...
详细信息
We study 2- and 3-dimensional digital geometry in the context of almost arbitrary adjacency relations. (Previous authors have based their work on particular adjacency relations). We define a binary digital picture to be a pair whose components are a set of lattice-points and an adjacency relation on the whole lattice. We show how a wide class of digital pictures have natural “continuous analogs.” This enables us to use methods of continuous topology in studying digital pictures. We are able to prove general results on the connectivity of digital borders, which generalize results that have appeared in the literature. In the 3-dimensional case we consider the possibility of using a uniform relation on the whole lattice. (In the past authors have used different types of adjacency for “object” and “background.”)
This paper describes the use of Ruby, a language of functions and relations, to develop serialised implementations of array-based architectures. Our Ruby expressions contain parameters which can be varied to produce a...
详细信息
This paper describes the use of Ruby, a language of functions and relations, to develop serialised implementations of array-based architectures. Our Ruby expressions contain parameters which can be varied to produce a wide range of designs with different space-time trade-offs. Such expressions can be obtained by applying correctness-preserving transformations to an initial simple description. This approach provides a unified treatment of serialisation schemes similar to LPGS (Locally Parallel Globally Sequential) and LSGP (Locally Sequential Globally Parallel) partitioning methods, and will be illustrated by the development of a variety of circuits for convolution.
We give a model-theoretic semantics for the logic of higher-order Horn clauses, the basis of a form of the lambdaProlog higher-order logic programming language. We define certain intensional general models and show th...
详细信息
We give a model-theoretic semantics for the logic of higher-order Horn clauses, the basis of a form of the lambdaProlog higher-order logic programming language. We define certain intensional general models and show that higher-order Horn clause logic is sound and complete with respect to them.
暂无评论