Monotone predicate transformers as Up-closed multirelations
Date
2006
Authors
Rewitzky I.
Brink C.
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
In the study of semantic models for computations two independent views predominate: relational models and predicate transformer semantics. Recently the traditional relational view of computations as binary relations between states has been generalised to multirelations between states and properties allowing the simultaneous treatment of angelic and demonic nondeterminism. In this paper the two-level nature of multirelations is exploited to provide a factorisation of up-closed multirelations which clarifies exactly how multirelations model nondeterminism. Moreover, monotone predicate transformers are, in the precise sense of duality, up-closed multirelations. As such they are shown to provide a notion of effectivity of a specification for achieving a given postcondition. © Springer-Verlag Berlin Heidelberg 2006.
Description
Keywords
Binary codes, Data structures, Mathematical models, Mathematical transformations, Semantics, Theorem proving, Binary relations, Multirelations, Nondeterminism, Computation theory
Citation
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
4136 LNCS
4136 LNCS