Footprints in Local Reasoning

DOI10.1007/978-3-540-78499-9_15MaRDI QIDQ5458360zbMATHOpenAlexFDO

Authors Mohammad Raza, Philippa Gardner

Publication date 11 April 2008

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

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

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)

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.

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 DE number 4152550

Cites work

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

Cited in

(6)

• Separation Logic Semantics for Communicating Processes
• scientific article; zbMATH DE number 2087445 (Why is no real title available?)
• Mechanizing Mathematical Reasoning
• Footprints in Local Reasoning
• Spatial-behavioral types for concurrency and resource control in distributed systems
• Being and change: reasoning about invariance

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)