The weakest specifunction

Chen, Yifeng; Sanders, J.W.

Abstract

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.

Citation

Chen, Y., & Sanders, J. (2005). The weakest specifunction. Acta Informatica, 41(7-8), 383-414. https://doi.org/10.1007/s00236-005-0163-5

• Journal Article Type: Article
• Publication Date: 2005-06
• Deposit Date: Apr 23, 2008
• Journal: Acta Informatica
• Print ISSN: 0001-5903
• Electronic ISSN: 1432-0525
• Publisher: Springer
• Peer Reviewed: Peer Reviewed
• Volume: 41
• Issue: 7-8
• Pages: 383-414
• DOI: https://doi.org/10.1007/s00236-005-0163-5
• Keywords: Formal methods, Refinement, Parallel programming, Program design.
• Public URL: https://durham-repository.worktribe.com/output/1588183
• Publisher URL: http://www.springerlink.com/openurl.asp?genre=article&eissn=1432-0525&volume=41&issue=7&spage=383