Completeness of Verification System with Separation Logic for Recursive Procedures

Abstract

The contributions of this dissertation are two results; the first result gives a new complete Hoare’s logic system for recursive procedures, and the second result proves the completeness of the verification system based on Hoare’s logic and separation logic for recursive procedures. The first result is a complete verification system for reasoning about WHILE programs with recursive procedures that can be extended to separation logic. To obtain it, this work introduces two new inference rules, shows derivability of an inference rule and removes other redundant inference rules and an unsound axiom for showing completeness. The second result is a complete verification system, which is an extension of Hoare’s logic and separation logic for mutual recursive procedures. To obtain the second result, the language of WHILE programs with recursive procedures is extended with commands to allocate, access, mutate and deallocate shared resources, and the logical system from the first result is extended with the backward reasoning rules of Hoare’s logic and separation logic. Moreover, it is shown that the assertion language of separation logic is expressive relative to the programs. It also introduces a novel expression that is used to describe the complete information of a given state in a precondition. In addition, this work uses the necessary and sufficient precondition of a program for the abort-free execution, which enables to utilize the strongest postconditions. iii I would like to dedicate this thesis to my parents for their love, sacrifice and support all through my life.