Frame rule of mutually recursive procedures manipulating pointers
Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove a powerful Hoare total correctness rule for mutually recursive procedures manipulating pointers. The rule combines earlier proof rules for (mutually) recursive procedures with the frame rule for pointer programs. The theory, including the proofs, is implemented in the theorem prover PVS. in this implementation program variables and addresses can store values of almost any type of the theorem prover. (C) 2009 Elsevier B.V. All rights reserved.
frame rule mutually recursive procedures pointers predicate transformer semantics separation logic mechanical verification of programs