Paper Info
Title
Algebras for correctness of sequential computations.
Abstract
Previous work gives algebras for uniformly describing correctness statements and calculi in various relational and matrix-based computation models. These models support a single kind of non-determinism, which is either angelic, demonic or erratic with respect to the infinite executions of a computation. Other models, notably isotone predicate transformers or up-closed multirelations, offer both angelic and demonic choice with respect to finite executions. We propose algebras for a theory of correctness which covers these multirelational models in addition to relational and matrix-based models. Existing algebraic descriptions, in particular general refinement algebras and monotonic Boolean transformers, are instances of our theory. Our new description includes a precondition operation that instantiates to both modal diamond and modal box operators. We verify all results in Isabelle, heavily using its automated theorem provers. We integrate our theories with the Isabelle theory of monotonic Boolean transformers making our results applicable to that setting.
Year
DOI
Venue
2014
10.1016/j.scico.2013.08.008
Science of Computer Programming
Keywords
Field
DocType
Axiomatic program semantics,Conway semirings,Hoare calculus,Multirelations,Preconditions
Monotonic function,Algebraic number,Programming language,Computer science,Matrix (mathematics),Correctness,Precondition,Operator (computer programming),Isotone,Computation
Journal
Volume
ISSN
Citations 
85
0167-6423
5
PageRank 
References 
Authors
0.46
35
1
Name
Order
Citations
PageRank
Walter Guttmann119616.53