A simple text processing tool which allows positioning of lines within a document is presented using the formal specification language Z. Implementation details such as the use of tab characters and newline sequences ...
详细信息
A simple text processing tool which allows positioning of lines within a document is presented using the formal specification language Z. Implementation details such as the use of tab characters and newline sequences are covered. The program has been implemented under the UNIX operating system. It is hoped that the use of similar techniques will become widespread in the field of software engineering.
Two regular processor arrays for multiplying unsigned numbers are described. The essence is a structure that allows designs with different degrees of pipelining to be synthesised. The impact of varying the degree of p...
详细信息
Two regular processor arrays for multiplying unsigned numbers are described. The essence is a structure that allows designs with different degrees of pipelining to be synthesised. The impact of varying the degree of pipelining on performance is assessed.
In this paper we deal with the problem of (nondeterministic and parallel) process refinement. The basic notion of refinement is defined via the improved failure semantics of CSP [BHR84, BrR85, Hoa85, Ros88]. The conce...
详细信息
Two systolic arrays for recursive digital filtering are presented. Both have a rectangular structure and produce output for a particular computation in consecutive cycles. Their performance is analyzed and the design ...
详细信息
Two systolic arrays for recursive digital filtering are presented. Both have a rectangular structure and produce output for a particular computation in consecutive cycles. Their performance is analyzed and the design tradeoffs are discussed.< >
作者:
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.
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.
Data refinement is the transformation in a computer program of one data type to another. Usually, we call the original data type ‘abstract’ and the final data type ‘concrete’. The concrete data type is said to rep...
详细信息
Data refinement is the transformation in a computer program of one data type to another. Usually, we call the original data type ‘abstract’ and the final data type ‘concrete’. The concrete data type is said to represent the abstract. In spite of recent advances, there remain obvious data refinements that are difficult to prove. We give such a refinement and present a new technique that avoids the difficulty. Our innovation is the use of program fragments that do not satisfy Dijkstra's Law of the excluded miracle . These of course can never be implemented, so they must be eliminated before the final program is reached. But, in the intermediate stages of development, they simplify the calculations.
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.
暂无评论