We describe the rudiments of algorithm refinement: the business of taking a specification and producing code that correctly implements it. The paper starts with a general discussion of the concepts, and then turns to ...
详细信息
We describe the rudiments of algorithm refinement: the business of taking a specification and producing code that correctly implements it. The paper starts with a general discussion of the concepts, and then turns to a particular calculus for algorithm refinement.
We present a basis for the formal specification and stepwise development of distributed systems, i.e. programs which are intended (at least conceptually) to run on distributed-memory parallel machines which communicat...
详细信息
This paper argues that our recent progress in the development of a sound programming methodology should not lead us to ignore the more difficult aspects of engineering;and that in future we should pay more attention t...
详细信息
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.
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 ordinary mathematics, an equation can be written down which is syntactically correct, but for which no solution exists. For example, consider the equation x = x + 1 defined over the real numbers; there is no value ...
详细信息
ISBN:
(数字)9781447132035
ISBN:
(纸本)9783540197805
In ordinary mathematics, an equation can be written down which is syntactically correct, but for which no solution exists. For example, consider the equation x = x + 1 defined over the real numbers; there is no value of x which satisfies it. Similarly it is possible to specify objects using the formal specification language Z [3,4], which can not possibly exist. Such specifications are called inconsistent and can arise in a number of ways. Example 1 The following Z specification of a functionf, from integers to integers "f x : ~ 1 x ~ O· fx = x + 1 (i) "f x : ~ 1 x ~ O· fx = x + 2 (ii) is inconsistent, because axiom (i) gives f 0 = 1, while axiom (ii) gives f 0 = 2. This contradicts the fact that f was declared as a function, that is, f must have a unique result when applied to an argument. Hence no suchfexists. Furthermore, iff 0 = 1 andfO = 2 then 1 = 2 can be deduced! From 1 = 2 anything can be deduced, thus showing the danger of an inconsistent specification. Note that all examples and proofs start with the word Example or Proof and end with the symbol.1.
A framework for model-checking timed CSP processes within a new model of standard CSP was discussed. The timing of events was provided by the consistent and regular communication of a special tock event, analogous to ...
详细信息
A framework for model-checking timed CSP processes within a new model of standard CSP was discussed. The timing of events was provided by the consistent and regular communication of a special tock event, analogous to the tick of a clock. A translation function TCSP&rarrCSP was done inductively over syntax of TCSP processes to equate every elapsed time unit with the communication of k tocks. It was observed that event occurance and timeout did not lead to an accumulation of timing errors.
Separation of concerns in existing code can be achieved by specific refactoring techniques. Modern refactoring tools support a number of well-known refactoring transformations, including method extraction. In this pap...
详细信息
ISBN:
(纸本)1581138423
Separation of concerns in existing code can be achieved by specific refactoring techniques. Modern refactoring tools support a number of well-known refactoring transformations, including method extraction. In this paper, we examine how method extraction can be improved through program slicing. Furthermore, we show how a generalization of such slice extraction can be applied to untangle existing code by extracting aspects. Copyright 2004 ACM.
This paper demonstrates how reduction to normal form can help in the design of a correct compiler for Dijkstra's guarded command language. The compilation strategy is to transform a source program, by a series of ...
This paper demonstrates how reduction to normal form can help in the design of a correct compiler for Dijkstra's guarded command language. The compilation strategy is to transform a source program, by a series of algebraic manipulations, into a normal form that describes the behaviour of a stored-program computer. Each transformation eliminates high-level language constructs in favour of lower-level constructs. The correctness of the compiler follows from the correctness of each of the algebraic transformations.
暂无评论