Categorical Assertion Semantics in Toposes

Categorical Assertion Semantics in Toposes
复制标题

拓扑中的分类断言语义

DOI：
10.1016/b978-0-12-037104-4.50013-x
复制
发表时间：
1993
期刊：
--
影响因子：
--
通讯作者：
Yoshihiro Mizoguchi
Yoshihiro Mizoguchi
中科院分区：
--
文献类型：
--
作者：
Yasuo Kawahara;Yoshihiro Mizoguchi

文献摘要

被引文献

相似文献

提出了一种程序设计语言断言（公理化）语义的范畴化解释。利用关系演算将所有的前置条件、后置条件和程序解释为命题中的（二元）关系，并证明了Dijkstra最弱前置条件的几个基本性质。语义中的断言依赖于直觉逻辑，因此这是由于EG Manes和MA Arbib的断言语义的扩展。
A categorical interpretation of assertion (axiomatic) semantics of programming languages is proposed. All of the preconditions, postconditions and programs are interpreted as (binary) relations in toposes by making use of relational calculus, and several fundamental properties of Dijkstra's weakest preconditions are proved. Assertions in the semantics depend on the intuitionistic logic, so this is an extension of the assertion semantics due to EG Manes and MA Arbib.