计算机科学 ›› 2009, Vol. 36 ›› Issue (6): 150-152.
• • 上一篇 下一篇
杨潇潇 段振华
出版日期:
发布日期:
基金资助:
YANG Xiao-xiao DUAN Zhen-hua （ Institute of Computing Theory and Technology, Xidian University, Xi＇an 710071,China）
Online:
Published:
摘要： 并发程序的不变式验证对理解程序和提高程序的正确性具有重要意义。以一种区间时序逻辑程序设计语言Framed Tempura为研究对象，给出了该语言的等价正则形，定义了该正则形在相邻两个状态上的良基关系，进而利用良基归纳法原理对该语言所描述的系统的不变式进行归纳验证。提出的基于良基归纳法的验证方法在时序逻辑程序中可以方便地验证系统的不变式，尤其是循环结构的不变量性质。
关键词: 时序逻辑程序 正则形 良基关系 良基归纳法 不变式证明
Abstract: Invariance properties are very central in concurrent software systems. Thinking by virtue of establishing an invariant and preserving it has immediate implications for reasoning about programs and their design. In this paper, we emploied an interval tempo
Key words: Temporal logic programs, Normal forms,Well-founded relation, Well-founded induction, Invariants proofs
杨潇潇 段振华. 良基归纳法在时序逻辑程序不变式验证中的应用[J]. 计算机科学, 2009, 36(6): 150-152. https://doi.org/
YANG Xiao-xiao DUAN Zhen-hua （ Institute of Computing Theory and Technology, Xidian University, Xi＇an 710071,China）. [J]. Computer Science, 2009, 36(6): 150-152. https://doi.org/
0 / / 推荐
导出引用管理器 EndNote|Reference Manager|ProCite|BibTeX|RefWorks
链接本文: https://www.jsjkx.com/CN/
https://www.jsjkx.com/CN/Y2009/V36/I6/150
Cited
首页