Completeness for recursive procedures in separation logic

详细信息    查看全文

• 作者：Mahmudul Faisal Al Ameen^a ; ^{alameen@nii.ac.jp" class="auth_mail" title="E-mail the corresponding author} ; Makoto Tatsuta^b ; ^{tatsuta@nii.ac.jp" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Separation logic ; Hoare's logic ; Completeness ; Recursive procedures
• 刊名：Theoretical Computer Science
• 出版年：2016
• 出版时间：6 June 2016
• 年：2016
• 卷：631
• 期：Complete
• 页码：73-96
• 全文大小：692 K

文摘

This paper proves the completeness of an extension of Hoare's logic and separation logic for pointer programs with mutual recursive procedures. This paper shows the expressiveness of the assertion language as well. This paper achieves a new system by introducing two new inference rules, and removes an axiom that is unsound in separation logic and other redundant inference rules for showing completeness. It introduces a novel expression that is used to describe complete information of a given state in a precondition. This work also uses the necessary and sufficient precondition of a program for the abort-free execution, which enables us to utilize strongest postconditions.