This paper extends Reynolds' separation logical system for pointer-based while program verification by adding inductive definitions. Inductive definitions give us a great advantage for verification, since they enable us for example, to formalize linked lists and to support the lemma reasoning mechanism. This paper proves its completeness theorem that states that every true asserted program is provable in the logical system. In order to prove its completeness, this paper shows an expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed by some assertion.
展开▼
