zbMATH — the first resource for mathematics

A semantic basis for local reasoning. (English) Zbl 1077.68705
Nielsen, Mogens (ed.) et al., Foundations of software science and computation structures. 5th international conference, FOSSACS 2002, held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43366-X). Lect. Notes Comput. Sci. 2303, 402-416 (2002).
Summary: We present a semantic analysis of a recently proposed formalism for local reasoning, where a specification (and hence proof) can concentrate on only those cells that a program accesses. Our main results are the soundness and, in a sense, completeness of a rule that allows frame axioms, which describe invariant properties of portions of heap memory, to be inferred automatically; thus, these axioms can be avoided when writing specifications.
For the entire collection see [Zbl 0989.00051].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q55 Semantics in the theory of computing
Full Text: Link