Monotone Predicate Transformers as Up-Closed Multirelations
Monotone Predicate Transformers as Up-Closed Multirelations
复制标题
作为闭环多重关系的单调谓词变换器
DOI：
10.1007/11828563_21
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
C. Brink
中科院分区：
文献类型：
--
作者：
Ingrid Rewitzky;C. Brink
在计算语义模型的研究中，两个独立的观点占主导地位：关系模型和谓词Transformer语义。最近，传统的关系计算的观点，作为国家之间的二元关系，已被推广到multirelations之间的状态和属性，允许同时治疗天使和恶魔的非决定论。本文利用多重关系的两级性质来提供上闭多重关系的因式分解，从而准确地阐明多重关系如何建模非确定性。此外，单调谓词转换器，在对偶的精确意义上，上闭的多重关系。因此，它们被证明是提供一个概念的有效性规范实现一个给定的后置条件。
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.