Enhanced specification expressivity for verification with separation logic

Abstract

Traditionally, the focus of specification mechanism has been on improving its ability to cover a wider range of problems more accurately, while the effectiveness of verification is left to the underlying provers. In this thesis, we attempt a novel approach, where the focus is on determining a good specification mechanism to achieve better expressivity (the specification should capture more accurately and concisely the functionality and applicability of the corresponding code) and verifiability (the verification process should succeed in more scenarios than the corresponding verification without the specification enhancements, with better or at least similar performance). In particular, we develop three new specification mechanisms, which, besides improving the specification, are meant to assist during the verification process itself.

We begin by investigating the benefits of immutability annotations in the specification for allowing more flexible handling of aliasing, as well as more precise and concise specifications. Our approach supports finer levels of control that can localize and mark parts of a data structure as being immutable through the use of annotations on predicate and data declarations. By using such annotations to encode immutability guarantees, we expect to obtain better specifications that can more accurately describe the intentions, as well as prohibitions, of the method. Ultimately, our goal is improving the precision of the verification process. We have designed and implemented a new entailment procedure to formally and automatically reason about immutability enhanced specifications. We have also formalised the soundness for our new procedure through an operational semantics with mutability assertions on the heap. Additionally, we have carried out a set of experiments to both validate and affirm the utility of our current proposal on immutability enhanced specification mechanism.

Secondly, we notice that, often, a user has an intuition about the proving process. This thesis provides the necessary utensils for integrating this intuition in the specification. Instead of writing a flat (unstructured) specification, the user can use insights about the proof for writing a structured specification that will trigger different techniques during the proving process: (i) case analysis can be invoked to take advantage of disjointness conditions in the logic. (ii) early, as opposed to late, instantiation can minimise on the use of existential quantification. (iii) formulae that are staged provide better reuse of the verification process. Initial experiments have shown that structured specifications can lead to more precise verification without incurring any performance overhead.

Lastly, we observe that one major issue about writing specifications for object-oriented (OO) programs is the fact that such specifications must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the specifications of overridden methods in superclasses, leading to imprecision in program reasoning. To address this, we advocate for two types of specifications, one type that caters to calls with static dispatching, and one for calls with dynamic dispatching. We formulate a novel specification subsumption that can avoid code re-verification, where possible. Using a predicate mechanism, we propose a flexible scheme for supporting class invariant and lossless casting.