Footprints in Local Reasoning

DOI10.1007/978-3-540-78499-9_15zbMATH Open1139.68020arXiv0903.1032OpenAlexW2171375973MaRDI QIDQ5458360FDOQ5458360

Authors: Mohammad Raza, Philippa Gardner 

Publication date: 11 April 2008

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Abstract: Local reasoning about programs exploits the natural local behaviour common in programs by focussing on the footprint - that part of the resource accessed by the program. We address the problem of formally characterising and analysing the footprint notion for abstract local functions introduced by Calcagno, O Hearn and Yang. With our definition, we prove that the footprints are the only essential elements required for a complete specification of a local function. We formalise the notion of small specifications in local reasoning and show that for well-founded resource models, a smallest specification always exists that only includes the footprints, and also present results for the non-well-founded case. Finally, we use this theory of footprints to investigate the conditions under which the footprints correspond to the smallest safe states. We present a new model of RAM in which, unlike the standard model, the footprints of every program correspond to the smallest safe states, and we also identify a general condition on the primitive commands of a programming language which guarantees this property for arbitrary models.

Full work available at URL: https://arxiv.org/abs/0903.1032

Recommendations

• Footprints in Local Reasoning
• On Local Reasoning in Verification
• A logical theory of localization
• scientific article; zbMATH DE number 2087445
• scientific article; zbMATH DE number 1916675
• scientific article; zbMATH DE number 1341465
• Mechanizing Mathematical Reasoning
• Local possibilistic logic
• scientific article

zbMATH Keywords

Hoare LogicSeparation LogicFootprintsLocal Reasoning

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cites Work

• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• The semantics and proof theory of the logic of bunched implications
• The Logic of Bunched Implications
• BI as an assertion language for mutable data structures
• Variables as resource in separation logic
• Permission accounting in separation logic
• Context logic and tree update
• Title not available (Why is that?)
• The specification statement
• Shape Analysis for Composite Data Structures
• Relational Parametricity and Separation Logic
• Local reasoning about data update

Cited In (5)

• Footprints in Local Reasoning
• Mechanizing Mathematical Reasoning
• Separation Logic Semantics for Communicating Processes
• Spatial-behavioral types for concurrency and resource control in distributed systems
• Title not available (Why is that?)

This page was built for publication: Footprints in Local Reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458360)