论文部分内容阅读
并发程序的不变式验证对理解程序和提高程序的正确性具有重要意义。以一种区间时序逻辑程序设计语言Framed Tempura为研究对象，给出了该语言的等价正则形，定义了该正则形在相邻两个状态上的良基关系，进而利用良基归纳法原理对该语言所描述的系统的不变式进行归纳验证。提出的基于良基归纳法的验证方法在时序逻辑程序中可以方便地验证系统的不变式，尤其是循环结构的不变量性质。