Frame rule for mutually recursive procedures manipulating pointers |
| |
Authors: | Viorel Preoteasa |
| |
Affiliation: | Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5 B, 20520 Turku, Finland |
| |
Abstract: | 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. |
| |
Keywords: | Predicate transformer semantics Mechanical verification of programs Mutually recursive procedures Pointers Separation logic Frame rule |
本文献已被 ScienceDirect 等数据库收录! |
|