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.
In data refinement, a concrete data type replaces an abstract data type used in the design of an algorithm or system (Gries and Prins, 1.85; Hoare, 1.72; Jones, 1.80). 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, 1.85; Hoare, 1.72; Jones, 1.80). 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, 1.80; Park, 1.81., 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 (1.76). Operations (in general, nondeterministic) are represented by relations, and significant use is made of prespecification and postspecification (Hoare and He, Jifeng, 1.87).
With two examples we show the suitability of the bulk-synchronous parallel (BSP) model for discrete-event simulation of homogeneous large-scale systems. This model provides a unifying approach for general purpose para...
详细信息
ISBN:
(纸本)0818679654
With two examples we show the suitability of the bulk-synchronous parallel (BSP) model for discrete-event simulation of homogeneous large-scale systems. This model provides a unifying approach for general purpose parallel computing which in addition to efficient and scalable computation, ensures portability across different parallel architectures. A valuable feature of this approach is a simple cost model that enables precise performance prediction of BSP algorithms. We show both theoretically and empirically that systems with uniform event occurrence among their components, such as colliding hard-spheres and ising-spin models, can be efficiently simulated in practice on current parallel computers supporting the BSP model.
Dijkstra's (1.75) 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 (1.75) 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.
A mathematical model of reconfigurability. We restrict is presented. The study is restricted to reconfigurations that can be implemented by connecting and disconnecting the wires that link nodes;these wires could be p...
详细信息
A mathematical model of reconfigurability. We restrict is presented. The study is restricted to reconfigurations that can be implemented by connecting and disconnecting the wires that link nodes;these wires could be physical or logical.
Two collaborative projects, the European ESPRIT BRA ProCoS project and the UK IED safemos project, are currently investigating methods to prove software and hardware systems correct at a number of different levels of ...
详细信息
Two collaborative projects, the European ESPRIT BRA ProCoS project and the UK IED safemos project, are currently investigating methods to prove software and hardware systems correct at a number of different levels of abstraction. Both projects intend to concentrate on subsets of Occam, and the transputer instruction set. The projects will aim to use the same machine language so that results obtained on both projects will be compatible. The initial selection of the projects (a simple subset of the transputer) is presented using the specification language Z. The role of the specification in the two projects is explained and the benefits and drawbacks of such a specification are discussed.
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.
Data refinement is the systematic substitution of one data type for another in a program. Usually, the new data type is more efficient than the old, but possibly more complex; the purpose of the data refinement in tha...
详细信息
Data refinement is the systematic substitution of one data type for another in a program. Usually, the new data type is more efficient than the old, but possibly more complex; the purpose of the data refinement in that case is to make progress in program construction from more abstract to more concrete formulations. A recent trend in program construction is tocalculateprograms from their specifications; that contrasts with proving that agivenprogram satisfies some specification. We investigate to what extent the trend can be applied to data refinement.
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.
暂无评论