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.
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...
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) 1997 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.
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.
作者：
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.
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 programming 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 programming language developments which are now being pursued.
There is a general agreement among theoretical computing scientists that a programming 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 programming 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.”)
暂无评论