Paper Info
Title
UTP Designs for Binary Multirelations.
Abstract
The total correctness of sequential computations can be established through different isomorphic models, such as monotonic predicate transformers and binary multirelations, where both angelic and demonic nondeterminism are captured. Assertional models can also be used to characterise process algebras: in Hoare and He's Unifying Theories of Programming, CSP processes can be specified as the range of a healthiness condition over designs, which are pre and postcondition pairs. In this context, we have previously developed a theory of angelic designs that is a stepping stone for the natural extension of the concept of angelic nondeterminism to the theory of CSP. In this paper we present an extended model of upward-closed binary multirelations that is isomorphic to angelic designs. This is a richer model than that of standard binary multirelations, in that we admit preconditions that rely on later or final observations as required for a treatment of processes.
Year
DOI
Venue
2014
10.1007/978-3-319-10882-7_23
Lecture Notes in Computer Science
Keywords
Field
DocType
semantics,refinement,binary multirelations,UTP
Monotonic function,Algebra,Computer science,Correctness,Theoretical computer science,Isomorphism,Predicate (grammar),Postcondition,Semantics,Computation,Binary number
Conference
Volume
ISSN
Citations 
8687
0302-9743
1
PageRank 
References 
Authors
0.35
12
2
Name
Order
Citations
PageRank
Pedro Ribeiro1184.74
Ana Cavalcanti211.03