Constraints: a uniform approach to aliasing and typing
Constraints: a uniform approach to aliasing and typing
复制标题
约束：统一的别名和类型方法
DOI：
--
复制
发表时间：
1985
期刊：
影响因子：
--
通讯作者：
F. Schneider
中科院分区：
文献类型：
--
作者：
L. Lamport;F. Schneider
约束是在整个执行过程中维持的程序变量之间的关系。类型声明和非常通用的别名形式可以表示为约束。给出了一个基于将霍尔三元组解释为时间逻辑公式的证明系统，用于推理带有约束的程序。证明系统是健全的、相对完整的，并给出了示例程序证明。
A constraint is a relation among program variables that is maintained throughout execution. Type declarations and a very general form of aliasing can be expressed as constraints. A proof system based upon the interpretation of Hoare triples as temporal logic formulas is given for reasoning about programs with constraints. The proof system is shown to be sound and relatively complete, and example program proofs are given.