作者：
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.
In his extension of VDM, Jones added a rely and a guarantee-condition to the usual pre and post-condition pair. This extension to the technique permits the specification and development of concurrent, shared-variable ...
详细信息
Two classes of systolic array for the implementation of recursive digital filters are presented, which overcome some of the limitations of earlier designs. The trade-off resulting from varying the degree of pipelining...
详细信息
Two classes of systolic array for the implementation of recursive digital filters are presented, which overcome some of the limitations of earlier designs. The trade-off resulting from varying the degree of pipelining is discussed.
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.
In data refinement, a concrete data type replaces an abstract data type used in the design of an algorithm or system (Gries and Prins, 1985; Hoare, 1972; Jones, 1980). We present two methods for calculating the weakes...
详细信息
In data refinement, a concrete data type replaces an abstract data type used in the design of an algorithm or system (Gries and Prins, 1985; Hoare, 1972; Jones, 1980). We present two methods for calculating the weakest specification of each operation on a concrete data type from the specification of the corresponding abstract operation, together with a single simulation relation (Milner, 1980; Park, 1981), which specifies the correspondence between the two types. The methods are proved sound and (jointly) complete for a nondeterministic procedural programming language slightly more powerful than Dijkstra's (1976). Operations (in general, nondeterministic) are represented by relations, and significant use is made of prespecification and postspecification (Hoare and He, Jifeng, 1987).
Dijkstra's (1975) weakest precondition is generalized in 4 ways, including: 1. The parameter Q may be a program, or it may be just the specification of a program that is not yet written. 2. The programming lang...
详细信息
Dijkstra's (1975) weakest precondition is generalized in 4 ways, including: 1. The parameter Q may be a program, or it may be just the specification of a program that is not yet written. 2. The programming language is extended to include general recursion. The increase in generality is obtained at the expense of some increase in complexity, and it can be justified only when it is needed. It is suggested that, in the design and development of correct programs, a calculus should be adopted in which: 1. programs and specifications are freely mixed, and 2. P is a program or design that correctly implements a design or specification Q, represented by the relational inclusion of P as a subset of Q. These suggestions generate some paradoxes, but they can be solved by recognizing that the set of programs is a proper subset of the set of specifications. Specifically, they are confined to relations that can be described using the primitives and operators of some programming language only.
Program transformation is used to develop the alpha-beta pruning algorithm from a specification of minimaxing. The pruning algorithm is nontrivial, and yet the transformation turns out to be relatively straightforward...
详细信息
Program transformation is used to develop the alpha-beta pruning algorithm from a specification of minimaxing. The pruning algorithm is nontrivial, and yet the transformation turns out to be relatively straightforward. The exercise is regarded as providing yet more evidence of the importance of transformational techniques, both for producing efficient programs and explaining them.
The Distributed computing Software project at Oxford University is using formal spécification techniques to explore the design of services in a distributed operating system. Our goal is to construct and publish t...
详细信息
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.”)
暂无评论