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 concentrates on the derivation of an operational semantics from an algebraic. First, the transition relation is defined by an inequation, and then the individual clauses of the operational semantics are der...
详细信息
This paper concentrates on the derivation of an operational semantics from an algebraic. 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 two languages;one is a large subset of CSP, and the other a notational variant of Dijkstra's Language. A combination of these languages provides a basis for the treatment of the transputer language occam.
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.
An overview is given of D-I algebra, an algebra for the specification of the safety and progress properties of delay-insensitive circuits in terms of voltage-level transitions on wires. The algebraic laws make it poss...
详细信息
The authors describe a method for speeding up divide-and-conquer algorithms with a hardware coprocessor, using sorting as an example. The method employs a conventional processor for the 'divide' and 'merge...
详细信息
An occam program is usually translated into a machine program executed in parallel with a set of system processes such as communication protocol and scheduler, where the target program appears in a form which cannot b...
详细信息
This paper explores the limits to computer-aided medical diagnosis. A specific application area (the diagnosis of abdominal pain of suspected gynaecological origin) is chosen, and the factors limiting the accuracy of ...
详细信息
This paper explores the limits to computer-aided medical diagnosis. A specific application area (the diagnosis of abdominal pain of suspected gynaecological origin) is chosen, and the factors limiting the accuracy of computer programs are investigated by means of a simulation model which has been shown previously to generate realistic cases. The model is used to generate arbitrarily large training and test sets. The results suggest that, while statistical dependencies exist amongst symptoms and signs, there is little to be gained by taking interactions into account. However, failure to record all possible observations does limit diagnostic accuracy significantly. The results suggest that near-optimal diagnostic accuracy (75-80%) can be obtained with a training set size of 10(5) cases simply by applying Bayes' theorem with the usual assumption of conditional independence.
A prototype proof system for "W: A Logic for Z" has been produced using the 2OBJ metalogical theorem-prover. 2OBJ permits an encoding which is very similar in structure to that of W, and the details are pres...
详细信息
We present a methodology for the formal specification and development of software systems using Z and the refinement calculus. The methodology combines the data structuring capabilities and the codified discrete mathe...
详细信息
The purpose of this paper is to introduce a notation for expressing the requirements of time-critical systems and a calculus for reasoning about them. The Actions, Events and States of a system are represented by sets...
详细信息
暂无评论