Frame rule for 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 combine...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2009-09, Vol.410 (42), p.4216-4233
Main Author: Preoteasa, Viorel
Format: Article
Language:English
Subjects:
Applied sciences
Computer science
control theory
systems
Exact sciences and technology
Frame rule
Language theory and syntactical analysis
Mathematical analysis
Mathematics
Mechanical verification of programs
Miscellaneous
Mutually recursive procedures
Operator theory
Pointers
Predicate transformer semantics
Sciences and techniques of general use
Separation logic
Software
Software engineering
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0304-3975
1879-2294
DOI:10.1016/j.tcs.2009.05.016