Chen, Y. and Sanders, J. W. (2005) 'The weakest specifunction.', Acta informatica., 41 (7-8). pp. 383-414.
The weakest specifunction has been introduced to generalise the notions of weakest prespecification and weakest parallel environment. It calculates the weakest specification function whose value refines the target specification when applied to a given component; thus it forms the basis for compositional refinement, an essential ingredient in program derivation. But unlike those previous calculi it is able to deal with several unknown components simultaneously and hence has wider applicability. In this paper we extend the general theory of the weakest specifunction, identifying those spaces in which it behaves miraculously. The par-seq specifunction places an established component in parallel with a required component and the result in sequence with another required component to meet a given specification. We extend the study of the par-seq specifunction in the context of LOGS, an intermediate-level language for reactive computing in an abstraction of the PRAM and BSP models of computation, and provide a single complete law for its use in program derivation. The resulting calculus is applied to the derivation of a distributed algorithm for dynamic load balancing.
|Keywords:||Formal methods, Refinement, Parallel programming, Program design.|
|Full text:||Full text not available from this repository.|
|Publisher Web site:||http://dx.doi.org/10.1007/s00236-005-0163-5|
|Record Created:||23 Apr 2008|
|Last Modified:||08 Apr 2009 16:22|
|Social bookmarking:||Export: EndNote, Zotero | BibTex|
|Look up in GoogleScholar | Find in a UK Library|