Structured Specifications for Better Verificationof Heap-Manipulating Programs
Cristian Gherghina1
1

Cristina David1

Shengchao Qin2

Wei-Ngan Chin1

Department of Computer Science, National University of Singapore
2School of Computing, University of Teesside

Abstract. Conventional specifications typically have a flat structure that is based
primarily on the underlying logic. Such specifications lack structures that could
have provided better guidance to the verification process. In this work, we propose to add three new structures to a specification framework for separation logic
to achieve a more precise and better guided verification for pointer-based programs. The newly introduced structures empower users with more control overthe verification process in the following ways: (i) case analysis can be invoked
to take advantage of disjointness conditions in the logic. (ii) early, as opposedto 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.

1

Introduction

Recent developments of the specification mechanisms have focused mostly on expressiveness [2, 1, 5] (to support verification for more properties), abstraction [16, 18] (tosupport information hiding in specification) and modularity [14, 7, 8] (to support morereadable and reusable specifications). To the best of our knowledge, there has been
hardly any attempt on the development of specification mechanisms that could support
better verifiability (in terms of both efficiency and effectiveness). Most efforts on better verifiability have been confined to the verification technology; an approach that may
lead to less portability (as we become more reliant on clever heuristics from the verification tools) and also more complex implementation for the verification tools themselves.
In this paper, we shall propose a novel approach towards better verifiability that focuseson new structures in the specification mechanism instead.
To illustrate the need for an enhanced specification mechanism, we will make useof separation logic, which allows for a precise description of heap-based data structures and their properties. As an example, consider a data node node2 and a predicate
describing an AVL tree that captures the size property via s and the height via h:data node2 { int val; int height; node2 right; node2 left; }avlhroot, h, si ≡ root=null ∧ h=0 ∧ s=0∨ root 7→ node2h , h, r, li ∗ avlhr, h1 , s1 i∗avlhl, h2 , s2 i∧h = max(h1 , h2 )+1∧ − 1≤h1 −h2 ≤1∧s=s1 +s2 +1

Formula p 7→ chv∗ i denotes a points-to fact of the heap where c is a data nodewith v∗ as its arguments, while spatial conjunction Φ1 ∗Φ2 denotes a program state withtwo disjoint heap spaces described by sub-formulae Φ1 and Φ2 , respectively. These two
notations of separation logic allow heap states to be expressed in a succinct manner.
The aforementioned definition asserts that an AVL tree is either empty (the basecase root=null ∧ h=0 ∧ s=0), or it consists of a data node (root 7→ node2h , h, r, li) andtwo disjoint subtrees (avlhr, h1 , s1 i∗avlhl, h2 , s2 i). Each node is used to store the actual
data in the val field, and the maximum height of the current subtree in the height
field. The constraint −1≤h1 −h2 ≤1 states that the tree is balanced, while s=s1 +s2 +1
and h=max(h1 , h2 )+1 compute the size and height of the tree pointed by root from theproperties s1 , s2 and h1 , h2 , respectively, that are obtained from the two subtrees. The ∗connector ensures that the head node and the right and left subtrees reside in disjoint
heaps. Our system automatically generates existential quantifiers for local values andpointers, such as r, l, h1 , h2 , s1 , s2 .
Next, we specify a method that attempts to retrieve the height information fromthe root node of the data structure received as argument. In case the argument has thevalue null, the method returns 0, as captured by res=0. To provide a suitable link
between pre- and post-conditions, we use the logical variables v, h, lt, lr that have to
be instantiated for each call to the method. As a first try, we capture both the null andnon-null scenarios as a composite formula consisting of a disjunction of the two cases,
as shown below:
int get height(node2 x)
requires x=null ∨ x 7→ node2hv, h, lt, lriensures (x=null ∧ res=0) ∨ (x 7→ node2hv, h, lt, lri ∧ res=h);{if (x = null) then 0 else x.height}
This specification introduces disjunctions both in the pre and post-conditions, which
would make the verification process perform search over the disjuncts[17]. Basically,each disjunct corresponds to an acceptable scenario of which at least one needs to be
proven. However, there are situations when the program state does not contain enoughinformation to determine which of the scenarios applies. For illustration, let us consider
that we are interested in retrieving the height information for an AVL tree pointed byx and the program state before the call to the get height method is avlhx, h1 , s1 i. We
have to verify that the current program state obeys the method’s precondition. However,when verifying the null and non-null scenarios separately, both checks fail as the
program state avlhx, h1 , s1 i does not contain sufficient information to conclude neither
that x6=null, nor that x=null. We provide the two failing verification conditions in theform of the entailment procedure from [17]: Φa ` Φc ∗ Φr , where the antecedent Φa andconsequent Φc are given, while the residue Φr is to be computed. This entailment finds
a subheap in Φa that satisfies Φc and returns the unused subheap from Φa as residue
Φr . Getting back to the current get height example, the two failing entailments are
given below. As none of the following two entailments succeeds, the verification of themethod call fails.
avlhx, h1 , s1 i`(x=null)∗Φr1
avlhx, h1 , s1 i`(x 7→ node2hv, h, lt, lri)∗Φr2

As a second try, we write the specification in a modular fashion by separating thetwo scenarios as advocated by past works [14, 7]. In [14], Leavens and Baker proposed
for each specification to be decomposed into multiple specifications (where it is calledcase analysis) to capture different scenarios of usage. Their goal was improving thereadability of specifications, as smaller and simpler specifications are easier to understand than larger ones. In [7] multiple specifications were advocated to help achieve
more scalable program verification. By using multiple pre/post conditions, we obtainthe following specification:
int get height(node2 x)
requires x=null ensures res=0;
requires x 7→ node2hv, h, lt, rti ensures x 7→ node2hv, h, lt, rti ∧ res=h;During the verification process, each scenario (denoted by a pre/post-condition pair)is proven separately [7]. However, neither of the two entailments (for each of the two
scenarios) succeeds, causing the verification of the method call to fail.
A possible solution is to perform case analysis on variable x: first assume x=null,then assume x6=null, and try to prove both cases. For soundness, these cases must be
disjoint and exhaustively cover all scenarios. Accordingly, the following two provableentailments are obtained, and the verification succeeds:
avlhx, h1 , s1 i∧x=null`(x=null)∗Φr1
avlhx, h1 , s1 i∧x6=null`(x 7→ node2hv, h, lt, lri)∗Φr2
However, case analysis is not always available in provers, as it might be tricky to decide on the condition for a case split. 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 paper,
we attempt a novel approach, where the focus is on determining a good specification
mechanism to achieve better expressivity and verifiability.
Often, a user has an intuition about the proving process. In the current work, we
provide the necessary utensils for integrating this intuition in the specification in orderto guide the verification. 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:– Case analysis is conventionally captured as part of the proving process. The user
typically indicates the program location where case analysis is to be performed[23]. This corresponds to performing a case analysis on some program state (orantecedent) of the proving process. In our approach, we provide a case construct todistinguish the input states of pre/post specifications instead. This richer specification can be directly used to guide the verification process. For the aforementioned
get height method, the case structured specification will automatically force a casesplit on x:case{x=null → ensures res=0;x6=null → requires x 7→ node2hv, h, lt, lriensures x 7→ node2hv, h, lt, lri ∧ res=h};

– Early vs. late instantiations denote different types of bindings for the logical variables (of consequent) during the entailment proving process. Early instantiation
is an instantiation that occurs at the first occurrence of its logical variable, while
late instantiation occurs at the last occurrence of its logical variable. While late instantiation can be more accurate for variables that are constructed from inequality
constraints, early instantiation can typically be done with fewer existential quantifiers since instantiation converts these existential logical variables to quantifier-freeform at an earlier point. We propose to use early instantiation, by default, and only
to resort to late instantiation when explicitly requested by the programmer.
– Staged formulae allows the specification to be made more concise through sharingof common sub-formulae. Apart from better sharing, this also allows verification
to be carried out incrementally over multiple (smaller) stages, instead of a single(larger) stage. The need for early/late instantiations, as well as for staged formulae
will be motivated in more details later in Sec 2.
In the rest of the paper we shall focus on the apparatus for writing and verifying (orchecking) structured specifications. Sec 2 provides examples to motivate the need for
two other aspects of structured specifications. Sec 3 formalizes the notion of structured
specifications. Sec 4 formalizes the verification rules to generate Hoare triples and entailment proving for structured specifications, while Sec 5 presents our experimental
results before some concluding remarks in Sec 6.

2

Motivating Examples

In the current section we present two more examples that motivate our enhancements
to the specification mechanism.
2.1

Example 1

Consider a method that receives two AVL trees, t1 and t2, and merges them by recursively inserting all the elements of t2 into t1. By using the case construct introduced in
Sec 1 we may write a case structured specification, which captures information about
the resulting tree size when t1 is not null, and about the resulting size and height,
whenever t1 is null:case{t1 = null → requires avlht2, s2, h2iensures avlhres, s2, h2i;t16=null → requires avlht2, s2, h2i ∗ avlht1, s1, i
ensures avlhres, s1+s2, i};
However, let us note that there is a redundancy in this specification, namely the same
predicate avlht2, s2, h2i appears on both branches of the case construct. After the needfor a case construct which was already discussed in Sec 1, this is the second deficiency
we shall address in our specification mechanism, that is due to a lack of sharing in
the logic formula which in turn causes repeated proving of identical sub-formulae. To
provide for better sharing of the verification process, we propose to use staged formulaeof the form (Φ1 then Φ2 ), to allow sub-formula Φ1 to be proven prior to Φ2 .
Though (Φ1 then Φ2 ) is semantically equivalent to (Φ1 ∗ Φ2 ), we stress that themain purpose of adding this new structure is to support more effective verification withthe help of specifications with less redundancy. By itself, it is not meant to improve theexpressivity of our specification, but rather its effectiveness. Nevertheless, when it isused in combination with the case construct, it could support case analysis of logicalvariables to ensure successful verification. The same structuring mechanisms can beused by formulae in both predicate definitions and pre/post specifications.
Getting back to the AVL merging example, the redundancy in the specification canbe factored out by using a staged formulae, as follows:
requires avlht2, s2, h2i thencase{t1 = null → ensures avlhres, s2, h2i;t16=null → requires avlht1, s1, i ensures avlhres, s1+s2, i};During the verification process, when reaching a call to the AVL merging method,
the current program state must entail the method’s precondition. Since the entailment
process needs to explore both branches of the specification, the avlht2, s2, h2i node will
be proven twice for each method call. By using staged formulae, the second specification will force the common formula to be proved only once. Although the two specifications capture the same information, the second version requires much less proving
effort. For this example, there was a 40% reduction in verification time by our system,
due solely to the presence of staged formulae.
For the general case, if x denotes the number of heap nodes/predicates that areshared in the consequent formula, and y the number of possible matchings from theantecedent, then the number of redundant matchings that are eliminated is (x − 1) ∗ y.
An analogy can be made between the use of the staged formula and the use of thebinary decision diagram (BDD) as an intermediate representation for SAT formulae
to support better sharing of identical sub-formulae [4]. Where applicable, we expect
staged formulae to improve the effectiveness of verification.
2.2

Example 2

Parameter instantiation is needed primarily for connecting the logical variables between
precondition and postcondition of specifications. Traditionally, manual instantiation of
ghost variables has played this role. In this paper, we propose two new mechanisms,
early and late instantiations, to support automatic instantiations of logical variables. As
an example, consider a data node cell and a predicate cellPred defined as follows:data cell { int val}
cellPredhroot, ii ≡ root=null ∧ i≤3 ∨ root 7→ cellh i ∧ i>3
To highlight the difference between early and late instantiations, we shall consider
two separate proof obligations. The first one is given below.
p 7→ cellh i ` (cellPredhp, ji∧j>2)∗Φr
At this point, we first need to match a heap predicate cellPredhp, ji on the RHS
with a data node p 7→ cellh i on the LHS to obtain an instantiation for the variable j.
A fundamental question is whether the variable instantiation could occur for just thepredicate cellPredhp, ji (we refer to this as early instantiation), or it has to be forthe entire formula cellPredhp, ji ∧ j>2 (known as late instantiation). By default, oursystem uses early (or implicit) instantiation for variables that are not explicitly declared.
In this scenario, early instantiation j>3 is obtained when folding with the predicate
cellPredhp, ji. This instantiation is transferred to the LHS. Consequently, we obtain asuccessful proof below.
j>3 ` (j>2)∗Φr
Now, let us consider a second proof obligation that will require late instantiation:p=null ` (cellPredhp, ji∧j>2)∗Φr
Similar to the previous case, we will first use a default early instantiation mechanism.
After matching cellPredhp, ji, we obtain the instantiation j≤3. However, moving only
this binding to the LHS is not enough, causing the proof below to fail.
p=null ∧ j≤3 ` (j>2)∗Φr
To support late instantiation for variable j, we declare it explicitly using [j] below:
p=null ` ([j] cellPredhp, ji∧j>2)∗Φr
This time variable j is kept on the RHS until the end of the entailment. As its proof
below succeeds, the instantiation for j will be captured in the residue as Φr =j≤3∧j>2.
p=null ` (∃j.j≤3∧j>2)∗Φr
Though late instantiation is more general, it may require existential quantifications overa larger formula. Hence, by default, we prefer to use early instantiation where possible,
and leave it to the user to manually declare where late instantiation is mandated.

3

Structured Specifications
Pre/Post. Z ::= ∃v∗1 ·Y1 . . . ∃v∗n ·Yn
multiple specs
Y ::= case{π1 ⇒Z1 ; . . . ; πn ⇒Zn }case construct| requires [w∗ ] Φ [then] Zstaged spec
|Wensures Q
post
Formula Q ::= ∃v∗ ·R
multiple disjuncts
R ::= case{π1 ⇒Q1 ; . . . ; πn ⇒Qn }case construct| [w∗ ] Φ [then Q]
staged formulaWΦ ::= ∃v∗ · (κ ∧ π)
Heap formula κ ::= emp | v 7→ chv∗ i | phv∗ i | κ1 ∗ κ2
Pure formula π ::= . . .
Fig. 1. Syntax for Structured Specifications

We shall now focus on the structured specifications mechanism. Fig 1 provides asyntactic description where Z denotes structured (pre/post) specifications, while Q denotes structured formulae that may be used for pre/post specifications, as well as forpredicate definitions. Apart from multiple specifications, our new syntax includes caseconstructs and staged formulae.

For structured specification, the requires keyword introduces a part of precondition through a staged specification. The postcondition is captured after each ensures
keyword, which must appear as a terminating branch for the tree-like specification
format. We support late instantiation via variables w∗ , from requires [w∗ ] Φ Z and[w∗ ] Φ [then Q] at the end of proving Φ. To minimise user annotations, our system automatically determines the other unbound variables (different from those to be late instantiated) as either existential or to be early instantiated.
Our construct to support case analysis is case{π1 ⇒Z1 ; . . . ; πn ⇒Zn } for specification, and case{π1 ⇒Q1 ; . . . ; πn ⇒Qn } for formula. We impose the following three
conditions on π1 , . . . , πn :(i) are restricted to only pure constraints, without any heap formula.
(ii) are exclusive, meaning that ∀i, j · i6=j → πi ∧πj =false.
(iii) are exhaustive, meaning that π1 ∨ . . . ∨πn =true.
Condition (i) is imposed since pure formula can be freely duplicated. Condition (ii)
is imposed to avoid conjunction over the heap-based formula. If absent, each heap state
may have to satisfy multiple case branches. Condition (iii) is needed for soundness ofcase analysis which requires all scenarios to be considered. To illustrate, consider:[(w : t)∗ ] Φ case{x=null⇒Q1 ; x6=null⇒Q2 }The first condition holds as the two guards, x=null and x6=null, are pure. Furthermore, our system checks successfully that the guards are exclusive((x=null∧x6=null)=false) and exhaustive ((x=null ∨ x6=null) = true).
3.1

Semantic Model for Structured Formulae

The semantics of our structured formula is similar to those given for separation logic[21], with extensions for the new structured formulae.
To define the model we assume sets Loc of locations (positive integer values), Valof primitive values, with 0 ∈ Val denoting null, Var of variables (program and logical variables), and ObjVal of object values stored in the heap, with c[f1 7→ν1 , .., fn 7→νn ]denoting an object value of data type c where ν1 , .., νn are current values of the corresponding fields f1 , .., fn . Let s, h |= Q in Fig 2 denote the model relation, i.e. the stacks and heap h satisfy the constraint Q, with h, s from the following concrete domains:h ∈ Heaps =df Loc *fin ObjVals ∈ Stacks =df Var → Val ∪Loc
Note that each heap h is a finite partial mapping while each stack s is a total mapping, as
in the classical separation logic [21, 9]. Function dom(f ) returns the domain of function
f . The model relation for separation heap formulas is defined below. The model relation
for pure formula s |= π denotes that the formula π evaluates to true in s. Note thath1 ⊥h2 indicates h1 and h2 are domain-disjoint, h1 ·h2 denotes the union of disjoint heaps
h1 and h2 . For the case of a data node, v 7→ chv∗ i, h has to be a singleton heap. On theother hand, a shape predicate defined by phv1..n i≡Q may be inductively defined.
With the semantics of the structured formulae in place, we can provide a translationfrom a structured formula to its equivalent unstructured formula. This translation isformalised with Q ;T Φ, as shown below:

Wn
W
∗
∗
s, h |= Q
iff Q= ni=1 ∃v ·Ri
i=1 ∃v ·Ri and s, h |=Wns, h |= i=1 ∃vi1..im ·Ri iff ∃k∈{1, .., n}·∃αk1..km ·s[vk1 7→αk1 , .., vkm 7→αkm ], h |= Rks, h |= [wn
]Φ
then
Q
iff ∃h1 , h2 · h1 ⊥h2 and h = h1 ·h2i=1and ∃α1..n ·s[w1 7→α1 , .., wn 7→αn ], h1 |= Φ and s, h2 |= Qs, h |= case{(πi ⇒Qi )ni=1 } iff ∀k∈{1, .., n}·(s, h |= π k → s, h |= Qk )s, h |= Φ1 ∨Φ2
iff s, h |= Φ1 or s, h |= Φ2s, h |= ∃v1..n ·κ∧π
iff ∃α1..n ·s[v1 7→α1 , .., vn 7→αn ], h |= κand s[v1 7→α1 , .., vn 7→αn ] |= πs, h |= κ1 ∗κ2
iff ∃h1 , h2 · h1 ⊥h2 and h = h1 ·h2
and s, h1 |= κ1 and s, h2 |= κ2s, h |= emp
iff dom(h) = ∅s, h |= p 7→ chv∗ iiff exists a data type decl. data c {t1 f1 , .., tn fn }and h=[s(p)7→r] and r=c[f1 7→s(v1 ), .., fn 7→s(vn )]s, h |= phv1..n iiff exists a pred. def. phv1..n i≡Q and s, h |= Q
Fig. 2. Model for Structured Formulae∀i · Qi ;T ΦiW∗
case{πi ⇒Qi } ;T (Φi ∧πi )W∀i · Ri ;T ΦiW∃v∗ ·Ri ;T ∃v∗ ·Φi

Q ;T Φ
[w∗ ] Φ1 then Q ;T Φ1 ∗ Φ[w∗ ] Φ ;T Φ

We make use of the semantics for structured formulae Q and for unstructured formula Φ to prove the correctness of the given translation rules.
Theorem 3.1 (Correctness of Translation) Given Q and Φ such that Q ;T Φ: for alls, h, s, h |= Q if and only if s, h |= Φ.
Proof: By structural induction on Q.

4Modular Verification

The main goal of structured specification is to support a modular verification processthat could be carried out efficiently and precisely. In this section, we propose a set ofrules to help generate Hoare-style triples for code verification, together with entailment
checking to support proof obligations over the structured formulae domain.
4.1

Building Verification Rules

Program verification is typically formalised using Hoare triples of the form{pre}e{post}, where pre and post are the initial and final states of the program code(e) in some logic. Our verification system uses separation logic, where a Hoare-stylespecification {pre}e{post} is valid, denoted as |= {pre}e{post}, if and only if, for allstates (s, h) that s, h |= pre, if the execution of e starting from (s, h) does not lead tomemory errors and terminates in a state (s1 , h1 ), then s1 , h1 |= post.
To better support structured specifications and case analysis, we propose a new tripleof the form {|Φ|} e {|Z|}, with pre being an unstructured formula and Z being the structured specification. We use structured specifications in the poststate because our case

analysis is guided from the post-states. In contrast, unstructured formulae are used in
the prestate since the structured form is unnecessary here. The semantic meaning of thisnew triple is defined as follows:
Definition 4.1 The validity of {|Φ|} e {|Z|} is defined inductively over the structure of Z.
That is:– if Z ≡ ensures Q : |= {|Φ|} e {|Z|} ⇐⇒ |= {Φ}e{Q};– if Z ≡ requires Φ1 [then] Z1 : |= {|Φ|} e {|Z|} ⇐⇒ |= {|Φ∗Φ1 |} e {|Z1 |};– if Z ≡ case{π1 ⇒Z1 ; . . . ; πn ⇒Zn }: |={|Φ|} e {|Z|} ⇐⇒⇐⇒ ∀i∈{1, .., n}·|={|Φ∧πi |} e {|Zi |};– if Z ≡ (∃v∗1 ·Y1 . . . ∃v∗n ·Yn ) : |= {|Φ|} e {|Z|} ⇐⇒⇐⇒ ∀i∈{1, .., n}· |= {|Φ|} e {|∃v∗i ·Yi |})2
[FV−METH]
H=[(v:t)∗ , (u:t)∗ ]G+ [res:t0 ]V= prime(H)+HVG ` {| (v 0 =v)∗ ∧ (u0 =u)∗ |} code {|Z|}` t0 mn ((t v)∗ , (ref t u)∗ ) Z { code }[FV−MULTI−SPECS]
fresh nv∗
ρ=[(v→nv)∗ ]∀i · G`{|Φ|} code {|ρYi |}G`{|Φ|} code {|∃v∗1 ·Y1 ..∃v∗n ·Yn |}[FV−REQUIRES]{w∗} ∩ Vars(G) = {}G1 = G + [(w : t)∗ ]G1 ` {|Φ1 ∗Φ2 |} code {|Z|}G ` {|Φ1 |} code {|requires [(w : t)∗ ] Φ2 Z|}[FV−ENSURES]
V =PassByValue(G)` {Φ} code {Φ2 }∃prime(V ) · Φ2 `emp
S6={}{} Q∗SG ` {|Φ|} code {|ensures Q|}[FV−CASE]∀i∈{1, .., n} · G ` {|Φ ∧ πi |} code {|Zi |}G`{|Φ|} code {|case{π1 ⇒Z1 ; . . . ; πn ⇒Zn }|}Fig. 3. Building Verification Rules for Structured Specifications

Our main verification rules are given in Fig. 3. Note that G records a list of variables (including res as result of the code) visible to the code verifier. Our specification
formulae use both primed and unprimed notations, where primed notations represent
the latest values of program variables, and unprimed notations denote either logicalvariables or initial values of program variables.
The verification of method declarations is described by the [FV−METH] rule. It verifies the method body code against the specification Z, as indicated by the rule. The
0function prime({v1 , .., vm }) returns the primed version {v10 , .., vm}. The third line of the
V 0
V 0
∗
premise deals with the verification task G ` {| (v =v) ∧ (u =u)∗ |} code {|Z|}, where
the precondition indicates that the latest values of program variables are the same astheir initial values. The other rules are syntax-directed and rely on the structure of thespecification Z.
The rule [FV−MULTI−SPECS] deals with the case where the post-state is a multispecification. It verifies the code against each of the specifications. Note that the substitution ρ replaces variables v∗ with fresh variables nv∗ . The rule [FV−REQUIRES] deals
with the case where the post-state starts with a requires clause. In this case, the formula in the requires clause is added to the pre-state (by separation conjunction) before

verifying the code against the remaining part of the specification in the post-state. The
variables for late instantiation (w∗ ) are also attached to the end of the list G. The rule
[FV−ENSURES] deals with the case where the post-state starts with an ensures clause.
It invokes our forward verification rules to derive the strongest postcondition Φ2 for thenormal Hoare triple {Φ}code{Φ2 } and invokes the entailment prover (described in thenext section) to check that the derived post-state Φ2 subsumes the given post-condition
Q (The test S 6= {} signifies the success of this entailment proof). Note that V denotes
the set of pass-by-value parameters that are not modified by the procedure. Hence, theirvalues (denoted by primed variables) are ignored in the postcondition, even if the program code may have updated these parameters. The last rule [FV−CASE] deals with thecase where the post-state is a case specification. It verifies in each case the specification
Zi is met when the guard πi is assumed in the pre-state.
To illustrate the generation of the verification tasks, consider the AVL merging given
in Section 2.1. By applying the rules from Figure 3, two Hoare triples are produced.
` {avlht2, s2, h2i ∧ t1=null} code {avlhres, s2, h2i}
` {avlht1, s1, i∗avlht2, s2, h2i∧t16=null} code {avlhres, s1+s2, i}
Theorem 4.1 (Soundness of Verification) Our verification rules are sound. That is,given a program code, an unstructured formula Φ, and a structured specification Z, if
our system derives a proof, ` {|Φ|} code {|Z|}, then we have |= {|Φ|} code {|Z|}.
Proof: It follows from the soundness of our underlying verification system (i.e. theone without structured specifications) [17], the definition 4.1, and the soundness of theentailment prover enriched with structured formulae (described in the next section).
4.2

Entailment for Structured Formula

Given formulae Φ1 and Q2 , our entailment prover checks if Φ1 entails Q2 , that is if in
all heaps satisfying Φ1 , we can find a subheap satisfying Q2 .
The main features of our entailment prover are that, besides determining if theentailment relation holds, it also infers the residual heap of the entailment, that is aformula ΦR such that Φ1 ` Q2 ∗ ΦR and derives the predicate parameters. The relation is formalized using a judgment of the form Φ1 `κV Q2 ∗ ΦR , which is a shorthandfor Φ1 ∗κ ` ∃V · (Q2 ∗κ)∗ΦR . Note that κ denotes the consumed heap, while V is a set,{v ∗ , E:w∗ }, containing the existential variables encountered, v ∗ , together with the variables w∗ for late instantiation, .
To support proof search, we have also generalised the entailment checking procedure to return a set of residues SR : Φ1 `κV Q2 ∗ SR .This entailment succeeds when SR is
non-empty, otherwise it is deemed to have failed. The multiple residual states captured
in SR signify different search outcomes during proving. Our entailment procedure relies on unfolding and folding of the predicate definitions. Unfolding refers to a single
inlining of a predicate in the antecedent, while folding is a recursive entailment with the
body of a predicate in the consequent. In the current paper, we enhance the entailment
proving procedure to handle structured formulae in the consequent. The main rules are
given in Figure 4. Take note that we make use of a method mark(V, w∗ ) , which marks

the variables to be late instantiated, w∗ , by removing them from the existential variables
stored in V and adding them as E : w∗ :mark(V, w∗ ) = (V −{w∗ })∪{(E : w)∗ }The rule [ENT−FORMULA] makes use of the aforementioned marking method in orderto mark the fact that variables w∗ are to be late instantiated, whereas rule [ENT−EXIST]
adds the existentially quantified variables v ∗ to the set V .
[ENT−FORMULA]Φ `κmark(V,w∗ ) (Φ1 ) ∗ SΦ `κV [w∗ ] Φ1 ∗ S[ENT−ENSURES]
Q ;T Φ1Φ `κV (ensures Q) ∗ (Φ ∗ Φ1 )[ENT−RHS−OR]∀i · Φ `κV Ri ∗ Si
W
S
Φ `κV
Ri ∗ ( S i )[ENT−CASE]∀i · Φ ∧ πi `κV Qi ∗ SiW
Φ `κV case{πi ⇒Qi }∗ ∗ ( Si )[ENT−STAGED−FORMULA]Φ `κmark(V,w∗ ) (Φ1 ) ∗ S S `κV −{w∗ } (Q) ∗ S2
Φ `κV ([w∗ ] Φ1 then Q) ∗ S2
[ENT−EXIST]Φ `κV ∪{v∗ } R ∗ SΦ `κV ∃v ∗ · R ∗ S

Fig. 4. Entailment for Structured Formula

In the rule for staged formula, [ENT−STAGED−FORMULA], the instantiation for thevariables w∗ takes place in the first stage, Φ1 . As instantiation moves the corresponding bindings to the LHS (or antecedent of entailment), the variables w∗ must be removed from the set of existentially quantified variables when entailing the rest of theformula, Q. At the end of the entailment proving, the variables that were marked aslate-instantiated are existentially quantified in the residue state. The generalised entailment with a set of n formulae in the antecedent is an abbreviation of the n entailments,
as illustrated below:∀i∈{1, .., n} · Φi `κV (Q) ∗ SiSn{Φ1 , .., Φn } `κV (Q) ∗ i=1 Si
The rule [ENT−CASE] adds the pure term πi to the antecedent. This rule requires alifted disjunction operation defined as S1 ∨S2 ≡{Φ1 ∨Φ2 |Φ1 ∈S1 , Φ2 ∈S2 } when applied
to two sets of states, S1 , S2 .
While a successful entailment of one disjunct suffices for the entailment of a disjunctive formula, our entailment rule [ENT−RHS−OR] facilitates a proof search by trying
to entail each of the RHS disjuncts separately. Therefore, the residue state must containthe union of all residues corresponding to the proof search from a set of entailments,∀i · Φ `κV Ri ∗ Si .
Take note that, at each call site, the forward verification procedure ensures thatthe method’s precondition is satisfied and assumes the method’s postcondition. This isachieved by entailing a formula denoting a specification of the Z form. As the corresponding entailment rules are similar to those for the entailment of a structured formula
given in Figure 4, we omit them for brevity. The only unusual rule is [ENT−ENSURES]

that is needed when entailing the actual postcondition ensures Q. In this case, the postcondition is added to the residual state in unstructured form, immediately after the translation Q ;T Φ1 to unstructured form.
Theorem 4.2 (Soundness of Entailment) Given Φ, Q such that s, h |= Φ,
if Φ `κV Q∗Φr for some Φr , then s, h |= Q∗Φr . That is, for all program states in which Φholds if Φ `κV Q∗Φr then Q∗Φr holds.
Proof: By structural induction on Q.

5

Experiments

We have built a prototype system using Objective Caml. The proof obligations generated by our verification are discharged using some off-the-shelf constraint solvers(like Omega Calculator [20]) or theorem provers (like MONA [13]). The specification
mechanism works with any constraint domain, as long as a corresponding prover forthe domain is available. The specific domains that our verifier currently supports, includes linear (Omega Calculator, Z3, CVC-lite) and non-linear arithmetic (Redlog), set(MONA, Isabelle bag tactic) and list properties (a Coq tactic). Though the current paper
highlighted mostly simpler specifications, our benchmark included the verification offunctional correctness properties, such as sortedness and permutation.
We have conducted preliminary experiments by testing our system on a suite ofexamples summarized in Figure 5. These examples are small but can handle data structures with sophisticated shape and size properties such as sorted lists, balanced trees,etc., in a uniform way. Methods “insert” and “delete” refer to the insertion and deletionof a value into/from the corresponding data structure, respectively. Method “del first”
deletes the node at the head in a circular list. Moreover, we verify a suite of sorting
algorithms, which receive as input an unsorted singly-linked list and return a sorted list.
Verification time for each function includes the time to verify all functions that it calls.
We compare the timings obtained with and without case analysis.
Take note that for each of the verified methods, in order to compare the results
obtained with and without case analysis, we provided specifications with the same levelof modularity through specifications with multiple pre/post. FAIL for the ”without case”
means it did not verify functional correctness (including memory safety). This is due
the absence of case analysis that would have been provided by the missing case spec.
Preliminary results indicate that case analysis improves both the completeness andthe performance of our system. From the completeness point of view, case analysis isimportant for verifying a number of examples that would fail otherwise. For instance,
the method implementing the selection sort algorithm over a linked list fails when it
is written with multiple specification instead of the case construct. The same scenario
is encountered for the method inserting/deleting a node of red black tree, and for the
method appending two list segments. The case construct thus helps our system to verify
more examples successfully. Regarding the performance, the timings obtained whenusing case analysis are smaller, taking on average 21% less computation time than thoseobtained without case analysis. The improvements are due to earlier pruning of falsecontexts with the help of case constructs and optimizations of the case entailment rule.

Program
Timings (in seconds)
speed
Codes
LOC with casewithout casegain (%)
Linked List
verifies length
delete
20
0.65
0.89
26
append
14
0.30
0.39
23
List Segmentverifies length
append11
0.95
failedCircular Linked List
verifies length + circularity
del first
15
0.35
0.41
15
insert
10
0.28
0.35
20
Doubly Linked List
verifies length + double links
insert
18
0.35
0.52
33
delete
29
0.94
1.27
26
Sorted List
verifies bounds + sortedness
insert
17
0.71
0.96
26
delete
21
0.60
0.68
22
insertion sort
45
0.92
1.35
32
selection sort52
1.24
failedbubble sort
42
1.95
2.92
43
merge sort
105
2.01
2.53
31
quick sort
85
1.82
2.47
26
AVL Treeverifies size + height + balanced
insert
169
32.27
39.48
19
delete
287
85.1
97.30
13
Perfect Treeverifies height + perfectness
insert
89
0.73
0.99
26
Red-Black Treeverifies size + black-height
insert167
5.44
faileddelete430
22.43
failedFig. 5. Verification Times for Case Construct vs Multiple Pre/Post

We also investigated the performance gain that can be attributed to the use of staged
formulae. We observed that the timings improved on average by 20%. Noteworthy examples include the AVL insertion (from 32.27s to 22.93s) and AVL deletion (from 85.1s
to 81.6s).
We may conclude from our experiments that structured specifications together withcase analysis give better precision to our verification system while also improving its
performance, when compared to corresponding unstructured specifications.

6

Related Work and Conclusion

Previous works on enhancing pre/post specifications [14, 12] were mainly concernedwith improving modularity to allow easier understanding of specifications. With thisobjective, multiple specifications and redundant representations were advocated as theprimary machinery. In the context of shape analysis, Chang and Rival [6] make useof if notation for defining inductive checkers. However, the conditional gets approximated to disjunction during the actual analysis. Verification wise, the three structured
specification mechanisms that we have proposed are not available in existing tools,
such as JML [5], Spec# [1], Dafny [15], JStar [8] and VeriFast [10]. The closest relationships may be summarized, as follows. JML supports specification cases, in theform of multiple pre/post conditions, for better modularity and clarity of specifications.
Our case constructs also intend to provide better guidance to the verification process.
Spec#/Dafny supports ghost variables for manual instantiation (by user) of logical variables. In contrast, our early/late instantiation mechanisms provided two solutions toautomatic instantiation of logical variables. Overall, little attempt has been made to add
specification structures that can help produce a better verification outcome.
On timings, we did not compare with Spec# and Dafny, since our benchmark onheap-manipulating programs is not properly covered by their specification logic. Regarding JStar, it currently uses logics involving only shapes and equalities, it does
not support more expressive properties, like set and numeric properties, needed by ourbenchmark. Lastly, VeriFast requires more user intervention in the form of explicit unfolding and folding of the abstract predicates through ghost statements.
In a distributed systems setting, Seino et al [22] present a case analysis meant toimprove the efficiency of protocol verification, which involves finding appropriate predicates and splitting a case into multiple sub-cases based on the predicates. In order tocover all the possible case splits, they use a special type of matrix. Pientka [19] argues
for the need of case analysis in inductive proofs. The potential case splits are selectedheuristically, based on the pattern of the theorem. A case split mechanism has been usedby Brock et al [3] to guide case analysis during proving. Jhala and McMillan [11] used
a temporal case splitting in order to specialize the properties to be proven, so that they
depend on only a finite part of the overall state. As opposed to the previous works, ourcurrent proposal is to incorporate structured mechanisms within the specification mechanism itself for guiding the case analysis, existential instantiation or staged proving.
Some existing theorem provers use tactics as a way to automate or semi-automate
proofs, and our system can take advantage of them through lower-level pure proofs.
However, for Hoare-style specification and verification, we have chosen to design astructured specification (rather than another tactic language) for the following reasons:– It can be provided at a higher-level that users can understand more easily, since it
is closer to specification mechanism rather than the (harder) verification process.
– It is more portable, as specification are tied to program codes, while tactic language
tend to be prover-specific requiring the invoked prover to understand the relevant
commands. Our approach basically breaks down larger (hard) proofs into smaller(simpler) proofs that any prover could more easily and more effectively handle, asconfirmed by our experiments.
– Specification can be transformed (or restructured) which allows us to heuristicallyinfer structured specifications from unstructured counterparts. A version of thistranslation from unstructured formula to structured formula has been implemented
in our system. Though this can never be as good as that provided by expert users,
it can nevertheless be used to handle most of the straightforward cases for legacy
specifications, leaving the harder unverified examples to be handled by users.
The current paper has pioneered a novel approach towards resolving two key problemsof verification, namely better modularity and better completeness through a new formof structured specification. Our proposal has been formalized and implemented with apromising set of experimental results.

Acknowledgement We thank the anonymous reviewers for their insightful feedbackon this work. The work was supported by NUS Grant R-252-000-366-112, MoE Grant
R-252-000-444-112 and EPSRC Grant EP/G042322.

References
1. M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview.
In CASSIS, volume 3362, pages 49–69. Springer-Verlag, LNCS, 2004.
2. J. Berdine, C. Calcagno, and P. W. O’Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO, Springer LNCS 4111, pages 115–137, 2006.
3. B. Brock, M. Kaufmann, and J. Strother Moore. ACL2 Theorems About Commercial Microprocessors. In FMCAD, pages 275–293, 1996.
4. R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions
on Computers, 35:677–691, 1986.
5. L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, andE. Poll. An overview of JML tools and applications. Software Tools for Technology Transfer,
2005.
6. B.-Y. E. Chang and X. Rival. Relational inductive shape analysis. In POPL, pages 247–260,
2008.
7. W.-N. Chin, C. David, H. H. Nguyen, and S. Qin. Multiple pre/post specifications for heapmanipulating methods. In HASE, pages 357–364, 2007.
8. D. Distefano and M. J. Parkinson. jStar: Towards Practical Verification for Java. In OOPSLA,
2008.
9. S. Ishtiaq and P.W. O’Hearn. BI as an assertion language for mutable data structures. In
ACM POPL, pages 14–26, London, January 2001.
10. B. Jacobs, J. Smans, and F. Piessens. A Quick Tour of the VeriFast Program Verifier. In
APLAS, pages 304–311, 2010.
11. R. Jhala and K. L. McMillan. Microarchitecture verification by compositional model checking. In CAV, pages 396–410, 2001.
12. H. B. M. Jonkers. Upgrading the pre- and postcondition technique. In VDM, pages 428–456,
London, UK, 1991. Springer-Verlag.
13. N. Klarlund and A. Moller. MONA Version 1.4 - User Manual. BRICS Notes Series, January
2001.
14. G. T. Leavens and A. L. Baker. Enhancing the Pre- and Postcondition Technique for More
Expressive Specifications. In FM, September 1999.
15. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In
LPAR (Dakar), pages 348–370, 2010.
16. M.J.Parkinson and G.M.Bierman. Separation logic and abstraction. In ACM POPL, pages
247–258, 2005.
17. H.H. Nguyen, C. David, S.C. Qin, and W.N. Chin. Automated Verification of Shape And
Size Properties via Separation Logic. In VMCAI, Nice, France, January 2007.
18. P.W. O’Hearn, H. Yang, and J.C. Reynolds. Separation and Information Hiding. In ACM
POPL, Venice, Italy, January 2004.
19. B. Pientka. A heuristic for case analysis. Technical report, 1995.
20. W. Pugh. The Omega Test: A fast practical integer programming algorithm for dependence
analysis. Communications of the ACM, 8:102–114, 1992.
21. J. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In IEEE LICS,
pages 55–74, Copenhagen, Denmark, July 2002.
22. T. Seino, K. Ogato, and K. Futatsugi. Mechanically supporting case analysis for verificationof distributed systems. IJPCC, 2005.
23. K. Zee, V. Kuncak, and M. C. Rinard. An integrated proof language for imperative programs.
In PLDI, pages 338–351, New York, NY, USA, 2009. ACM.