Two for the price of one: lifting separation logic assertions. (English) Zbl 1258.03032

Thamsborg, Jacob; Birkedal, Lars; Yang, Hongseok

Log. Methods Comput. Sci. 8, No. 3, Paper No. 22, 31 p. (2012).

Summary: Recently, data abstraction has been studied in the context of separation logic, with noticeable practical successes: the developed logics have enabled clean proofs of tricky challenging programs, such as subject-observer patterns, and they have become the basis of efficient verification tools for Java (jStar), C (VeriFast) and Hoare Type Theory (Ynot).
In this paper, we give a new semantic analysis of such logic-based approaches using Reynolds’s relational parametricity. The core of the analysis is our lifting theorems, which give a sound and complete condition for when a true implication between assertions in the standard interpretation entails that the same implication holds in a relational interpretation. Using these theorems, we provide an algorithm for identifying abstraction-respecting client-side proofs; the proofs ensure that clients cannot distinguish two appropriately related module implementations.

MSC:

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

Keywords:

separation logic; data abstraction; relational interpretation

Software:

Ynot; ESC/Java; jStar; SIMPLIFY; Boogie; VeriFast