基于时态逻辑演算的程序验证
刘清
江西大学计算机科学系;
Liu Qing Department of Computer Science
摘要 本文建立了时态逻辑演算。在该演算系统下,若能证明一程序抽象成的时态逻辑公式是定理,则该程序是完全正确的。
关键词 :
良结构 ,
时态逻辑 ,
不变式 ,
演绎
Abstract :Temporal logic calculu is established. The program is total correctenessif it can prove that the temporal logic formula from a program abstractingis a theorem in the system of the calculu.
Key words :
well-structure
inveriant
temporal logic;
deduction
出版日期: 1990-09-28
[1]
张学立; 王东浩; . 具有不确定性的溯因推理 [J]. 南昌大学学报(人文社会科学版), 2014, 45(05): 38-.
[2]
孙玉芸. 从演绎作品的原创性看演绎权的侵犯 [J]. 南昌大学学报(人文社会科学版), 2013, 44(01): 86-.
[3]
孙玉芸. 论非法演绎作品的法律保护 [J]. 南昌大学学报(人文社会科学版), 2012, 43(05): 79-.
[4]
刘清. 基于Rough集理论的模态逻辑与Rough逻辑 [J]. 南昌大学学报(理科版), 1998, 22(04): 1-.
[5]
谢先仁. 形式逻辑演绎推理就是从一般到个别的推理吗? [J]. 南昌大学学报(人文社会科学版), 1994, 25(01): 1-6.
[6]
谢先仁; 樊明亚. 普通逻辑几个理论问题辨要 [J]. 南昌大学学报(人文社会科学版), 1993, 24(01): 1-6.
[7]
谢先仁. 关于传统逻辑推理分类的反思 [J]. 南昌大学学报(人文社会科学版), 1991, 22(03): 1-6.
[8]
谢先仁. 对演绎推理两个定义的质疑 [J]. 南昌大学学报(人文社会科学版), 1989, 20(01): 1-6.