Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings
Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings
复制标题
程序构建数学 - 第 13 届国际会议，MPC 2019，葡萄牙波尔图，2019 年 10 月 7-9 日，会议记录
DOI：
10.1007/978-3-030-33636-3_8
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Dongol B
中科院分区：
文献类型：
--
作者：
Dongol B
代数代数已经发展为等式一阶逻辑的代数化。我们适应圆柱Kleene晶格及其变种，并提出这些关系和关系故障模型。这使我们能够编码帧和局部变量块，并得出摩根的细化演算以及代数霍尔逻辑，而程序的分配法。因此，我们的方法打开了大门，代数计算程序和逻辑变量，而不是特定领域的推理程序存储的具体模型。最后给出了一个小程序的精化证明。
Cylindric algebras have been developed as an algebraisation of equational first order logic. We adapt them to cylindric Kleene lattices and their variants and present relational and relational fault models for these. This allows us to encode frames and local variable blocks, and to derive Morgan’s refinement calculus as well as an algebraic Hoare logic for while programs with assignment laws. Our approach thus opens the door for algebraic calculations with program and logical variables instead of domain-specific reasoning over concrete models of the program store. A refinement proof for a small program is presented as an example.