作者：
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.
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.”)
The study of computing is split at an early stage between the separate branches that deal with hardware and software;there is also a corresponding split in later professional specialisation. This paper explores the es...
详细信息
The study of computing is split at an early stage between the separate branches that deal with hardware and software;there is also a corresponding split in later professional specialisation. This paper explores the essential unity of the two branches and attempts to point to a common framework within which hardware-software codesigns can be expressed as a single executable specification, reasoned about, and transformed into implementations. We also describe a hardware/software co-design environment which has been built, and we show how designs can be realised within this environment. A rapid development cycle is achieved by using FPGAs to host the hardware components of the system. The architecture of a hardware platform for supporting experimental hardware/software co-designs is presented. A. particular example of a real-time video processing application built using this design environment is also described.
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 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.
We explore the suitability of two semantic spaces as a basis for a probabilistic variant of the language of Communicating Sequential Processes (CSP), so as to provide a formalism for the specification and proof of cor...
详细信息
We explore the suitability of two semantic spaces as a basis for a probabilistic variant of the language of Communicating Sequential Processes (CSP), so as to provide a formalism for the specification and proof of correctness of probabilistic algorithms. The two spaces give rise to two sublanguages, each of which is characterised by an algebraic axiomatisation which is shown to be sound and complete for finite processes. In the first semantics, processes are defined as probability measures on the space of infinite traces and operators are defined as functions (mostly transformations) of probability measures, The advantage of this semantics is that it is simple and good for reasoning about probabilistic properties such as self-stabilisation or fairness of random algorithms. The disadvantage is that neither external choice nor parallel composition other than fully synchronised parallel composition can be defined in this semantics. This problem is solved in the second model which is based on the space of conditional probability measures of infinite traces. This model leads to a set of proof rules for the deterministic properties of probabilistic algorithms, but it is more difficult to use in the analysis of probabilistic properties. The last part of the paper shows how the two models are related and how this can be exploited to combine their advantages and get around their disadvantages, This is illustrated by the example of a self-stabilising tokenring.
We describe and analyse a new parallel algorithm for event-driven simulation of hard-particle systems that is based on the ideas of the bulk-synchronous parallel (BSP) model. This model provides a unifying approach fo...
详细信息
We describe and analyse a new parallel algorithm for event-driven simulation of hard-particle systems that is based on the ideas of the bulk-synchronous parallel (BSP) model. This model provides a unifying approach for general purpose parallel computing which in addition to efficient computation ensures portability across different parallel architectures. The hard-particle system is divided into regions that are owned by a unique processor. Events involving particles located in the region boundaries are called border zone events and are used to synchronize the parallel operation of the processors. On a P-processor BSP computer the algorithm works doing iterations composed of two phases: the parallel phase where each processor is simultaneously allowed to simulate serially and asynchronously its own region, and the synchronization phase where the occurrence of at most P border zone events is scheduled for the next iteration considering the state of neighboring regions. We show that this algorithm is efficient in practice provided that a sufficiently large hard-particle system is to be simulated.
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.
暂无评论