Loop Invariant Synthesis in a Combined Abstract Domain
Shengchao Qin∗a,b,c , Guanhua Hea , Chenguang Luoa , Wei-Ngan Chind , Xin Chenc
a School of Computing, Teesside University, Middlesbrough, TS1 3BA, UK
b College of Computer Science, Beijing University of Technologyc State Key Lab. for Novel Software Technology, Nanjing Universityd School of Computing, National University of Singapore

Abstract
Automated verification of memory safety and functional correctness for heap-manipulating programs has been a challenging task, especially when dealing with complex data structures with strong invariants involving both shape andnumerical properties. Existing verification systems usually rely on users to supply annotations to guide the verification, which can be cumbersome and error-prone by hand and can significantly restrict the usability of the verification
system. In this paper, we reduce the need for some user annotations by automatically inferring loop invariants overan abstract domain with both shape and numerical information. Our loop invariant synthesis is conducted automatically by a fixed-point iteration process, equipped with newly designed abstraction mechanism, together with join andwidening operators over the combined domain. We have also proven the soundness and termination of our approach.
Initial experiments confirm that we can synthesise loop invariants with non-trivial constraints.
Keywords: loop invariant, fixpoint analysis, abstraction, combining analysis, shape analysis, numerical analysis,
separation logic
PACS: 07.05.Bx, 89.20.Ff

1. Introduction
Although research on software verification has a long and distinguished history dating back to the 1960’s, it remains a challenging problem to automatically verify heap manipulating programs written in mainstream imperative
languages. This is in part due to the use of shared mutable data structures in programs, and the need to track various program properties, such as structural numerical information (e.g. length and height) and relational numericalinformation (e.g. sortedness and binary search tree properties).
Since the emergence of separation logic [1, 2], dramatic advances have been made in automated software verification, e.g. the Smallfoot tool [3] for the verification on pointer safety (i.e. shape properties asserting that pointers cannot
go wrong), the verification on termination [4], the verification for object-oriented programs [5, 6], and Dafny [7] andHip/Sleek [8, 9, 10, 11] for handling more general properties (such as set-based and numerical properties for data
structures) in heap-manipulating programs.
As a key to prove the correctness of loops, a suitable loop invariant for each loop must be provided by users
in these verification systems. However, supplying invariants by hand in a sophisticated domain can be tedious anderror-prone. It also affects the scalability of these tools, as each program may contain many loops.
To address this problem, various shape analysis techniques have been proposed in, e.g., the separation logic
based SpaceInvader tool [12, 13, 14], which, as a further step of Smallfoot, can automatically infer loop invariants
as well as method specifications for pointer safety properties. The Hob system [15] offers a set-based analysis forloop invariant synthesis. Another tool THOR [16] incorporates simple numerical information into the shape domain
to allow automated synthesis of properties involving length of list segments. These successes have demonstrated

Email addresses: s.qin@tees.ac.uk (Shengchao Qin), g.he@tees.ac.uk (Guanhua He)
URL: http://www.scm.tees.ac.uk/s.qin/ (Shengchao Qin)
Preprint submitted to Journal of Symbolic Computation

September 5, 2012

the feasibility to generate loop invariant automatically for shape analysis to help automate the program verification
process.
However, most of the prior loop invariant analyses focus on relatively simple properties, such as pointer safety forlists and list length information. It is difficult to apply them in the presence of more sophisticated program properties,
such as:• More complex user-defined data structures, such as height-balanced trees;• Relational numerical properties, like sortedness and binary search property.
These properties can be part of the full functional correctness for heap-manipulating programs. The (aforementioned)
Hip/Sleek tool can handle such properties. It allows users to define their own shape predicates in conjunction withproperties of interests, in order to capture a higher desired level of correctness for their programs.
In this paper, we present a technique to automatically discover loop invariants over the combined shape andnumerical domain to improve the level of automation for Hip/Sleek-like verification systems. Our approach is basedon the framework of abstract interpretation [17] with fixed-point computation. We make the following technicalcontributions:• We propose a loop invariant synthesis algorithm with novel operations for abstraction, join and widening overa combined shape and numerical domain.
• We demonstrate that our analysis is sound w.r.t. concrete program semantics and prove that it always terminates.
• We have integrated our solution into the Hip/Sleek tool and conducted some initial experiments. The experimental results confirm the viability of our solution and show that we can effectively eliminate the need foruser-provision of loop invariants which were previously necessary in verification.
The rest of the paper is structured as follows. We first illustrate our approach informally via an example (Section 2),
and then give our programming and specification languages (Section 3). Formal details about loop invariant synthesis
are presented in Section 4, followed by experimental results in Section 5. Related work and concluding remarks comeafterwards.
2. The Approach
Before presenting an illustrative example for the analysis, we first introduce our specification mechanism which
follows the Hip/Sleek system [9].
2.1. Specification mechanism
Separation logic [1, 2] extends Hoare logic to support reasoning about shared mutable data structures. One connective that it adds to classical logic is separation conjunction ∗. The separation formula p1 ∗ p2 asserts that two heaps
described by the formulae p1 and p2 are domain-disjoint. We make use of this connective in our specifications.
Similar to the Hip/Sleek system, we allow user-defined inductive predicates to specify both separation and numerical properties. For example, with a data structure definition for a node in a list data node { int val; node next; },we can define a predicate for a singly linked list as
root::llhni ≡ (root=null∧n=0)∨(∃v, q, m · root::nodehv, qi∗q::llhmi∧n=m+1)
The parameter root for the predicate ll is the initial pointer into the first node of the linked list, or null if thelist is empty. Its length is denoted by numerical parameter n. A uniform notation p::chv1 , . . . , vk i is used for either a singleton heap or a predicate. If c is a data node with fields f1 , . . . , fk , the notation represents a singleton
heap, p7→c[f1 7→v1 , . . . , fk 7→vk ] which says that the variable p points to a c data node and the value of its fields are
v1 , . . . , vk , e.g. root::nodehv, qi in the above formula. If c is a predicate name, then the data structure pointed to byp has the shape c with parameters v1 , . . . , vk , e.g. q::llhmi above.
2

We can also define a singly linked list segment as follows:
lshp, ni ≡ (root=p ∧ n=0) ∨ (root::nodeh , qi ∗ q::lshp, mi ∧ n=m+1)
where the parameter p denotes the next field for the last node of the list segment. Note that we use the following
shortened notation: (i) default root parameter in the left hand side (LHS) may be omitted, (ii) unbound variables,such as q and m, are implicitly existentially quantified, and (iii) the underscore denotes an existentially quantified
anonymous variable.
If the user wants to verify a sorting algorithm, they can incorporate sortedness property into the above predicatesas follows:sllhn, mn, mxi ≡ (root::nodehmn, nulli ∧ n=1 ∧ mn=mx) ∨(root::nodehmn, qi ∗ q::sllhn1 , k, mxi ∧ mn≤k ∧ n=n1 +1)
slshp, n, mn, mxi ≡ (root::nodehmn, pi ∧ n=1 ∧ mn=mx) ∨(root::nodehmn, qi ∗ q::slshp, n1 , k, mxi ∧ mn≤k ∧ n=n1 +1)
where mn and mx denote respectively the minimum and maximum values stored in the sorted list.
As a more involved example, one may define the following predicate to specify sorted doubly-linked list segments
sdshp, q, n, mn, mxi ≡ (root::node2hmn, p, qi ∧ n = 1 ∧ mn = mx) ∨(root::node2hmn, p, ri ∗ r::sdshroot, q, n − 1, k, mxi ∧ mn ≤ k)based on the data structure definition
data node2 { int val; node2 prev; node2 next; }where the parameters p and q denote, respectively, the prev field of root and the next field of the last node of thelist. Similar to the definition of sls, mn (respectively mx) is the minimum (respectively the maximum) value stored in
the double sorted list.
Such user-supplied predicates can be employed to specify loop invariants and method specifications.
2.2. Illustrative Example

0 data node { int val;

9

while (srt != null &&srt.val <= v) {node next; }1 node ins_sort(node x)

10

prv=srt; srt=srt.next;2

requires x::llhni

11

}

3

ensures res::sllhn, mn, mxi

12

cur.next=srt;

4 {int v;

13

if (prv != null) prv.next=cur;

5

node r,cur,srt,prv=null;

14

else r=cur;

6while (x != null) {

15

}

7

cur=x; x=x.next; v=cur.val; 168

srt=r; prv=null;

return r;

17 }Figure 1: Insertion sort for linked list.
We now illustrate via an example our loop invariant synthesis process. The method ins sort (Fig. 1) sorts alinked list with the insertion sort algorithm. It is implemented with two nested while loops. The outer loop traverses
3the whole list x, takes out each node from it (line 7), and inserts that node into another already sorted list r (which is
empty initially before the sorting). This insertion process makes use of the inner while loop in lines 9-11 to look fora proper position in the already sorted list for the new node to be inserted. The actual insertion takes place at lines
12-14.
To verify this program, we need to synthesise appropriate loop invariants for both while loops. Our analysis
follows a standard fixpoint iteration process. It starts with the (abstract) program state immediately before the while
loop (i.e., the initial state) and symbolically executes the loop body for several iterations, until the obtained states
converge to a fixpoint, which is the loop invariant.1 At the start of each iteration, the obtained state from the previous
iteration is joined with the initial state. In addition to this join operator, we have also defined an abstraction function
and a widening operator both of which will help the fixpoint iteration to converge. The join and widening operators
are specifically designed to handle both shape and numerical information.
As for our example, due to the presence of nested loops, each iteration of the analysis for the outer loop actuallyinfers a loop invariant for the inner loop. We shall now illustrate how we synthesise a loop invariant for the inner loop.
Suppose that in one iteration for the outer loop, the state at line 9 becomes
r::sllhnr , a, bi ∗ cur::nodehv, xi ∗ x::llhnx i ∧ srt=r ∧ prv=null ∧ nr +nx +1=nNote that since the inner loop does not mutate the heap part referred to by cur and x (i.e., cur::nodehv, xi∗x::llhnx i),
we can ignore it during the invariant synthesis and add it back to the program state using the frame rule of separation
logic [2]. Therefore, the initial state for loop invariant synthesis becomes
r::sllhnr , a, bi ∧ srt=r ∧ prv=null ∧ nr +nx +1=n(1)

From this state, symbolically executing the loop body once yields the state:
r::nodeha, srti ∗ srt::sllhns , c1 , bi ∧ prv=r ∧a≤c1 ∧ a≤v ∧ nr +1=n−nx ∧ ns +1=nr(2)which says that the pointer srt moves towards the rear of the list by one node. We then join it with the initial state (1)to obtain(r::sllhnr , a, bi ∧ srt=r ∧ prv=null ∧ nr +nx +1=n)∨(r::nodeha, srti ∗ srt::sllhns , c1 , bi ∧(3)
prv=r ∧ a≤c1 ∧ a≤v ∧ nr +1=n−nx ∧ ns +1=nr )The second iteration over the loop body starts with (3) and exhibits (also) the case that srt has moved by two nodes
towards the rear, while prv moves by one node. Its result is then joined with pre-state (1) yielding the current state:(3) ∨ r::nodeha, prvi ∗ prv::nodehc1 , srti ∗ srt::sllhns , c2 , bi ∧a≤c1 ≤c2 ∧ c1 ≤v ∧ nr +1=n−nx ∧ ns +2=nr(4)

Executing the loop body a third time returns a post-state where three nodes are passed by srt, and two by prv, as
below:(4) ∨ r::nodeha, r0 i ∗ r0 ::nodehc1 , prvi ∗ prv::nodehc2 , srti ∗srt::sllhns , c3 , bi ∧ a≤c1 ≤c2 ≤c3 ∧ c2 ≤v ∧ nr +1=n−nx ∧ ns +3=nr
where we have an auxiliary logical variable r0 . Following this trend, it is predictable that every iteration hereafter
will introduce an additional logical variable (referring to a list node). If we tolerate such increase in the subsequent
iterations, the analysis will never terminate. Our abstraction process prevents this from happening by eliminatingintermediate logical variables, as follows:(4) ∨ r::slshprv, n1 , a, c1 i ∗ prv::nodehc2 , srti ∗ srt::sllhns , c3 , bi ∧a≤c1 ≤c2 ≤c3 ∧ c2 ≤v ∧ nr +1=n−nx ∧ ns +3=nr ∧ n1 =2
1 The fixpoint iteration converges if one more iteration still yields the same result.

4Note that the heap part r::nodeha, r0 i ∗ r0 ::nodehc1 , prvi is abstracted as a sorted list segment r::slshprv, n1 , a, c1 iwith n1 denoting the length of the segment and n1 =2 added into the state. This abstraction process ensures that ouranalysis does not allow the shape to increase infinitely. Note also that the abstraction process has made use of the facta≤c1 .
This fourth iteration results in a post-state where four nodes are passed by srt, and three by prv. An abstraction is
performed to remove the newly created logical pointer variables. As a simplification of the presentation, let us denote
σ as r::slshprv,n1 ,a,c1 i ∗ prv::nodehc2 ,srti ∗ srt::sllhns ,c3 ,bi ∧ a≤c1 ≤c2 ≤c3 ∧ c2 ≤v ∧ nr +1=n−nx . The result
obtained after the fourth iteration is(4) ∨ (σ ∧ ns +3=nr ∧ n1 =2) ∨ (σ ∧ ns +4=nr ∧ n1 =3)
for which we have an observation that the last two disjunctions share the same shape part (as in σ). This disjunction
will be transferred to the numerical domain, as follows:(4) ∨ (σ ∧ (ns +3=nr ∧ n1 =2 ∨ ns +4=nr ∧ n1 =3))
This simplifies the abstraction further. After that, our widening operation compares the current state with the previous
one, to look for a common set of (numerical) constraints that both states imply, and to replace those numericalconstraints in the current state with the ones discovered by widening. This operation helps ensure the termination of
our analysis. As for the example, a set of constraints among ns , nr and n1 can be discovered to make the widened
post-state to become:(4) ∨ (σ ∧ ns +n1 =nr −1 ∧ n1 ≥2)(5)
One more iteration of symbolic execution will produce the same result as (5), suggesting that it is already the fixpoint(and hence the loop invariant):
r::sllhnr , a, bi ∧ srt=r ∧ prv=null ∧ nr +1=n−nx ∨
r::nodeha, srti ∗ srt::sllhns , c1 , bi ∧ prv=r ∧a≤c1 ∧ a≤v ∧ nr +1=n−nx ∧ ns +1=nr ∨
r::nodeha, prvi ∗ prv::nodehc1 , srti ∗ srt::sllhns , c2 , bi ∧a≤c1 ≤c2 ∧ c1 ≤v ∧ nr +1=n−nx ∧ ns +2=nr ∨
r::slshprv, n1 , a, c1 i ∗ prv::nodehc2 , srti ∗ srt::sllhns , c3 , bi ∧a≤c1 ≤c2 ≤c3 ∧ c2 ≤v ∧ nr +1=n−nx ∧ ns +n1 =nr −1 ∧ n1 ≥2Note that although it is possible to further join the third disjunctive branch with the fourth, our analysis does not doso as it tries to keep the result as precise as possible by eliminating only auxiliary pointer variables.
With the frame part cur::nodehv, xi ∗ x::llhnx i added back, the analysis for the outer loop continues. Eventually,
the following loop invariant is discovered for the outer loop:(x::llhnx i ∧ r=null ∧ nx =n) ∨ (r::nodeha, nulli ∗ x::llhnx i ∧ n=nx +1) ∨(r::sllhnr , a, bi ∗ x::llhnx i ∧ n=nx +nr ∧ nr ≥2)
which allows us to verify the entire method successfully using Hip/Sleek verifier.
3. Language and Abstract Domain
To simplify presentation, we focus on a strongly-typed C-like imperative language in Fig. 2. The program Prog
written in this language consists of declarations tdecl, which can either be data type declarations datat (e.g. node in
Section 2), or predicate definitions spred (e.g. ll, ls, sll, sls in Section 2.1), as well as method declarations meth.
The definitions for spred and mspec are given later in Fig. 3. Without loss of expressiveness, we use an expressionoriented language. So the body of a method (e) is an expression formed by standard commands of an imperative
language. Note that d and d[v] represent resp. heap-insensitive and heap sensitive commands.
Our specification language (in Fig. 3) allows (user-defined) shape predicates spred to specify both shape andnumerical properties. Note that spred are constructed with disjunctive constraints Φ and numerical formulae π. We
require that the predicates be well-formed [11].
5Prog ::= tdecl∗ meth∗tdecl ::= datat | spred
datat ::= data c { field∗ }field ::= t v
t::= c | τmeth ::= t mn ((t v)∗ ) mspec {e}τ::= int | bool | voide::= d | d[v] | v:=e | e1 ; e2 | t v; e | if v then e1 else e2 | while v {e}d::= null | kτ | v | new c(v∗ ) | mn(v∗ )d[v] ::= v. f | v. f :=w | free(v)Figure 2: A Core (C-like) Imperative Language.

spred
mspec
Φ
σ
∆
κ
π
γ
φ
b
a
p

::= root::chv∗ i ≡ Φ::= requires Φpr ensures ΦpoW::= σ∗::= ∃v∗ ·κ∧π::= Φ | ∆1 ∨∆2 | ∆∧π | ∆1 ∗∆2 | ∃v·∆::= emp | v::chv∗ i | κ1 ∗ κ2::= γ ∧ φ::= v1 =v2 | v=null | v1 ,v2 | v,null | true | γ1 ∧γ2::= b | a | φ1 ∧φ2 | φ1 ∨φ2 | ¬φ | ∃v · φ | ∀v · φ::= true | false | v | b1 = b2::= p1 =p2 | p1 ≤p2::= kint | v | kint ×p | p1 + p2 | −p | max(p1 ,p2 ) | min(p1 ,p2 )Figure 3: The Specification Language.

A conjunctive abstract program state, σ, is composed of a heap (shape) part κ and a numerical part π, where π
consists of γ and φ as aliasing and numerical information, respectively, and where p is a Presburger expression andk is a constant value. We use SH to denote the set of such conjunctive states. During the symbolic execution, theabstract program state at each program point will be a disjunction of σ’s, denoted by ∆ (and its set is recognised as
PSH ). An abstract state ∆ can be normalised to a Φ form.
The memory model of our specification formula is adapted from what is given in the classical separation logic [1,2], and our abstract domain is capable of handling user-defined shape predicates and related numerical properties
described by this model. We assume sets Loc of memory locations, Val of primitive values (with 0 ∈ Val denoting null), Var of variables (program and logical variables), and ObjVal of object values stored in the heap, withc[ f1 7→ν1 , . . . , fn 7→νn ] denoting an object value of type c where ν1 , . . . , νn are current values of the corresponding
fields f1 , . . . , fn . Let s, h |= ∆ denote the model relation that the stack s and heap h satisfy ∆, with s, h from thefollowing concrete domains:s ∈ Stacks =d f Var → Val ∪ Loch ∈ Heaps =d f Loc *fin ObjVal
Note that each heap h is a finite partial mapping while each stack s is a total mapping. The detailed model definitionis given in Fig. 4. We use h1 ⊥h2 to denote that the heaps h1 and h2 have disjoint domains, and h1 · h2 to indicate the6

s, h |= Φ1 ∨ Φ2s, h |= ∃v∗ · κ ∧ πs, h |= κ1 ∗ κ2

iff
iff
iff

s, h |= emp
iffs, h |= p::chv1 , . . . , vn i iffor
s |= π1 ∧ π2
s |= πiff
iffs, h |= Φ1 or s, h |= Φ2∃ν∗ · s[v∗ 7→ ν∗ ], h |= κ and s[v∗ 7→ ν∗ ] |= π
∃h1 , h2 · h1 ⊥h2 and h = h1 · h2 ands, h |= κ1 and s, h |= κ2
dom(h) = ∅isdatat(c) and s(p) > 0 and h = [s(p) 7→ r]
and r = c[ f1 7→v1 , . . . , fn 7→vn ]isspred(c) and chv1 , . . . , vn i≡Φand s, h |= [p/root]Φ
s |= π1 and s |= π2s |=A πFigure 4: The semantic model.

union of such heaps. Note that the test isdatat(c) returns true only if c is a data node and isspred(c) returns true
only if c is a shape predicate. The semantic model for pure formulae s |=A π is left in the Appendix (Fig. A.8).
We use the separation logic prover Sleek [11] to prove whether one abstract state ∆0 entails another one ∆:0∆ `∆ ∗ R. Along with the proof, Sleek also computes the residue part R (a.k.a the frame) which is useful for ourinference framework. To prove the entailment is to check whether heap nodes in the antecedent ∆0 are sufficiently
precise to cover all nodes from the consequent ∆. The entailment checking procedure uses unfold/fold reasoning
to deal with user-defined shape predicates with sophisticated numerical properties. During the entailment proof, theframe R is generated and it contains the nodes which are not consumed from the antecedent after matching up withthe formula from the consequent, and numerical constraints which convey the relationship between the variables in
the antecedent and consequent formulae. For instance, by entailment proof∃y · x::nodehvx, yi ∗ y::llhni ` x::llhmi ∗ R
we can generate the residue R as m = n+1, which says that x is a list of length n+1. Meanwhile, if we try to prove∃y · x::nodehvx, yi ∗ y::nodehvy, zi ∧ vx≤vy ` x::slshn, z, mn, mxi ∗ R
the residue R can be generated as n=2 ∧ mn=vx ∧ mx=vy ∧ mn≤mx, which shows that the length of the sorted list fromx to z is 2, and the minimal value of the list is vx in node x and the maximal value is vy in node y. From the above
examples, we can see that the Sleek prover can be used to eliminate quantified pointer variables, to generate more
abstract shape views, and to preserve useful numerical information.
Based on the entailment relation, we define a partial order over the abstract states:∆  ∆0 =d f ∆0 ` ∆ ∗ R

for some R

We also denote this by ∆0  ∆. Based on this partial order, we also have an induced lattice over these states as thebase of fixpoint calculation for loop invariants.
4. Analysis Algorithm
Our proposed analysis algorithm is given in Fig. 5. The algorithm takes four input parameters: T as the program
environment with all the method specifications in the program, ∆pre as the precondition for the while loop (i.e. theabstract state before the loop starts), the while loop itself while b {e}, and an upper bound n on the number of sharedlogical variables we keep during analysis.
7Fixpoint Computation in Combined Domain
Input: T , ∆ pre , while b {e}, n ;Local: i := 0; ∆i := ∆ pre ; ∆0i := ∆i ;repeat12i := i + 1;

3

∆i := widen† (∆i−1 , join† (∆i−1 , ∆0i−1 ));4∆0i := abs† (|[e]|T (∆i ∧ b));5

if ∆0i = false ∨ cp no(∆0i ) > nthen return fail end if·
6

until ∆0i = ∆0i−1 ;7return ∆0i

Figure 5: Main analysis algorithm.
Our analysis is based on abstract interpretation [17] with specifically designed operations (abs, join and widen)
over this combined domain.2 At the beginning, we initialise the iteration variable (i) and two states to begin with (∆iand ∆0i ). The starting state of the calculation is ∆ pre . Among the two states here, the unprimed version ∆i denotes
the initial state before the ith execution of the loop body, and the primed one ∆0i represents the result state after. Each
iteration starts at line 1. Firstly we join together the initial state ∆i−1 of the previous iteration with the result state∆0i−1 obtained in the previous iteration, and widen it against the state ∆i−1 (line 3). Then we symbolically executethe loop body with the abstract semantics in Section 4.1 (line 4), and apply the abstraction operation to the obtained
abstract state. If the symbolic execution cannot continue due to a program bug, or if we find our abstraction cannot
keep the number of shared logical variables/cutpoints (counted by cp no) within a specified bound (n), then a failure
is reported (line 5). Otherwise we judge whether a fixpoint is already reached by comparing the current abstract statewith the previous one (line 6). The fixpoint ∆0i is returned as the loop invariant.
We will elaborate the key techniques of our analysis in what follows: the abstract semantics, the abstraction
function, and the join and widening operators.
4.1. Abstract Semantics
The abstract semantics is used to execute the loop body symbolically to obtain its post-state during the loop
invariant synthesis. Its type is defined as|[e]| : AllSpec → PSH → PSH
where AllSpec contains all the specifications of all methods (extracted from the program Prog). For some expressione, given its precondition, the semantics will calculate the postcondition.
The foundation of the semantics is the basic transition functions from a conjunctive abstract state to a conjunctive
or disjunctive abstract state below:
rearr(x): SH → PSH[x]Rearrangement

exec(d[x]) : AllSpec → SH[x] → SH Heap-sensitive execution
exec(d): AllSpec → SH → SH

Heap-insensitive execution

2 Note that our analysis uses lifted versions of these operations (indicated by †), which will be explained in more details in Section 4.2.

8

where SH[x] denotes the set of conjunctive abstract states in which each element has x exposed as the head of adata node (x::chv∗ i), and PSH[x] contains all the (disjunctive) abstract states, each of which is composed by such
conjunctive states. Here rearr(x) rearranges the symbolic heap so that the cell referred to by x is exposed for accessby heap sensitive commands d[x] via the second transition function exec(d[x]). The third function defined for other(heap insensitive) commands d does not require such exposure of x.
isdatat(c) σ ` x::chv∗ i ∗ σ0
rearr(x)σ =d f σ
isspred(c) σ ` x::chu∗ i ∗ σ0 root::chv∗ i≡Φrearr(x)σ =d f σ0 ∗ [x/root, u∗ /v∗ ]Φ
As mentioned earlier, the test isdatat(c) returns true only if c is a data node and isspred(c) returns true only if c is ashape predicate.
The symbolic execution of heap-sensitive commands d[x] (i.e. x. fi , x. fi := w, or free(x)) assumes that the rearrangement rearr(x) has been done previously:
isdatat(c) σ ` x::chv1 , .., vn i ∗ σ0
exec(x. fi )(T )σ =d f σ0 ∗ x::chv1 , .., vn i ∧ res=vi
isdatat(c) σ ` x::chv1 , .., vn i ∗ σ0
exec(x. fi := w)(T )σ =d f σ0 ∗ x::chv1 , .., vi−1 , w, vi+1 , .., vn i
isdatat(c) σ ` x::chu∗ i ∗ σ0
exec(free(x))(T )σ =d f σ0
The symbolic execution rules for heap-insensitive commands are as follows:exec(k)(T )σ =d f σ ∧ res=kexec(x)(T )σ =d f σ ∧ res=x

isdatat(c)exec(new c(v ))(T )σ =d f σ ∗ res::chv∗ i∗t mn ((ti ui )ni=1 ) requires Φpr ensures Φpo ∈ Tρ = [xi /ui ]ni=1 σ ` ρΦpr ∗ σ f r σ po = ρΦpoexec(mn(x1 , .., xn ))(T )σ =d f σ po ∗ σ f r
Note that the first three rules deal with constant (k), variable (x) and data node creation (new c(v∗ )), respectively, while
the last rule handles method invocation. In the last rule, the call site is ensured to meet the precondition of mn, as
signified by σ ` ρΦpr ∗ σ f r , where σ f r is the frame part. In this case, the execution succeeds and the postcondition ofmn (ρΦpo ) is added into the post-state.
A lifting function † is defined to lift rearr’s domain to PSH :__rearr† (x)σi =d f(rearr(x)σi )and this function is overloaded for exec to lift both its domain and range to PSH :__exec† (d)(T )σi =d f(exec(d)(T )σi )9Based on the transition functions above, we can define the abstract semantics for a program command e as follows:|[d[x]]|T ∆=d f exec† (d[x])(T ) ◦ rearr† (x)∆|[d]|T ∆=d f exec† (d)(T )∆|[e1 ; e2 ]|T ∆=d f |[e2 ]|T ◦ |[e1 ]|T ∆|[ x := e]|T ∆=d f [x0 /x, r0 /res](|[e]|T ∆) ∧ x=r0 fresh logical x0 , r0|[if v then e1 else e2 ]|T ∆ =d f (|[e1 ]|T (v∧∆)) ∨ (|[e2 ]|T (¬v∧∆))
which form the foundation for us to analyse the loop body.
4.2. Abstraction, Join and Widening
This section describes our specifically designed abstraction, join and widening operations employed in our loop
invariant synthesis process.
Abstraction function. During the symbolic execution, we may be confronted with many “concrete” shapes in postconditions of the loop body. As an example of list traversal, the list may contain one node, or two nodes, or even morenodes in the list, which the analysis cannot enumerate infinitely. The abstraction function deals with those situations
by abstracting the (potentially infinite) concrete shapes into more abstract shapes. Our rationale is to keep only program variables and shared cutpoints; all other logical variables will be abstracted away. As an instance, the first state
below can be further abstracted (as shown), while the second one cannot:
abs(x::nodeh , z0 i ∗ z0 ::nodeh , nulli) = x::llhni ∧ n=2
abs(x::nodeh , z0 i ∗ y::nodeh , z0 i ∗ z0 ::nodeh , nulli) = -(6)where both x and y are program variables, and z0 is an existentially quantified logical variable. In the second casez0 is a shared cutpoint referenced by both x and y, and thus the state is not changed (the - denotes the same formula
as input). As illustrated, the abstraction transition function abs eliminates unimportant cutpoints (during analysis) toensure termination. Its type is defined as follows:
abs : SH → SH

Abstraction

which indicates that it takes in a conjunctive abstract state σ and abstracts it as another conjunctive state σ0 . Below
are its rules.
(Subst1)
abs(σ ∧ x0 =e) =d f σ[e/x0 ]abs(σ ∧ e=x0 ) =d f σ[e/x0 ](Subst2)x0 < Reach(σ)(Unreach)abs(x0 ::chv∗ i ∗ σ) =d f σ ∗ true
isdatat(c1 )c2 hu∗2 i ≡ Φ∗∗
p::c1 hv1 i ∗ σ1 ` p::c2 hv2 i ∗ σ2
Reach(p::c2 hv∗2 i ∗ σ2 ) ∩ {v∗1 } = ∅abs(p::c1 hv∗1 i ∗ σ1 ) =d f p::c2 hv∗2 i ∗ σ2

(Abs)

The first two rules Sub1 and Sub2 eliminate logical variables (x0 ) by replacing them with their equivalent expressions(e). The third rule Unreach is used to eliminate any garbage (heap part led by a logical variable x0 unreachable fromthe other part of the heap) that may exist in the heap. As x0 is already unreachable from, and not used by, the program
variables, it is safe to treat it as garbage true, for example the x0 in x::nodeh , nulli ∗ x0 ::nodeh , nulli where only
x is a program variable.
The last rule Abs plays the most significant role which intends to eliminate shape formulae led by logical variables(all variables in v∗1 ). It tries to fold data nodes up into a shape predicate. It confirms that c1 is a data node definitionand c2 is a predicate. The predicate c2 is selected from the user-defined predicates environments and it is the target
10shape to be abstracted against with. The rule ensures that the latter is a sound abstraction of the former by entailment
proof, and the pointer logical parameters of c1 are not reachable from other part of the heap (so that the abstraction
does not lose necessary information). For instance, given the user-defined predicate for singly-linked list root::llhni,
the following abstraction step can take place:abs(x::nodeh , z0 i ∗ z0 ::nodeh , nulli) = x::llhni ∧ n=2

where x is program variable and z0 is logical variable. The function Reach is defined as follows:[
Reach(σ) =d f
ReachVar(κ∧π, v) where σ ::= ∃u∗ ·κ∧πv∈fv(σ)returning all pointer variables which are reachable from free variables in the abstract state σ. The function ReachVar(κ ∧ π, v)
returns the minimal set of pointer variables satisfying the relationship below:{v} ∪ {z2 | ∃z1 , π1 · z1 ∈ReachVar(κ ∧ π, v) ∧ π=(z1 =z2 ∧ π1 ) ∧ isptr(z2 )} ∪ {z2 |∃z1 , κ1 · z1 ∈ReachVar(κ∧π, v) ∧ κ=(z1 ::ch.., z2 , ..i ∗ κ1 ) ∧ isptr(z2 )} ⊆ ReachVar(κ∧π, v)
namely, it is composed of aliases of v and pointer variables reachable from v. The predicate isptr(x) checks if x isa pointer variable. For example, ReachVar(x::nodeh , z0 i ∗ y::nodeh , z0 i ∗ z0 ::nodeh , p0 i, {x}) = {x, z0 , p0 }. Notethat the numerical logic parameters can be abstracted since the numerical relations are kept in pure formulae, so we
do not lose numerical information here.
We apply the above abstraction rules (following the given order) onto an abstract state exhaustively until it stabilises. Such convergence is confirmed because the abstract shape domain is finite due to the bounded numbers ofvariables and predicates, as discussed later.
Finally the lifting function is overloaded for abs to lift both its domain and range to disjunctive abstract states
PSH :
_
_
abs†
σi =d fabs(σi )which allows it to be used in the analysis.
Join operator. The operator join is applied over two conjunctive abstract states, trying to find a common shape as asound abstraction for both:join(σ1 , σ2 ) =d f
let σ01 , σ02 = rename(σ1 , σ2 ) inmatch σ01 , σ02 with (∃x1∗ · κ1 ∧ π1 ), (∃x2∗ · κ2 ∧ π2 ) inif κ1 ` κ2 ∗ true then ∃x1∗ , x2∗ · κ2 ∧ (joinπ (π1 , π2 ))else if κ2 ` κ1 ∗ true then ∃x1∗ , x2∗ · κ1 ∧ (joinπ (π1 , π2 ))else σ1 ∨ σ2

where the rename function prevents naming clashes among logical variables of σ1 and σ2 , by assigning fresh names
to logical variables with the same name in the two states. For example given a name clash on x0 , it may change states∃x0 · x0 =0 and ∃x0 · x0 =1 to ∃x0 · x0 =0 and ∃x1 · x1 =1 instead. After this procedure it judges whether σ2 is an
abstraction of σ1 , or the other way round. If either case holds, it regards the shape from the weaker state (which ismore general/abstract) as the shape of the joined state, and performs joining for numerical formulae with joinπ (π1 , π2 ),the convex hull operator over numerical domain [18]. Otherwise it keeps a disjunction of the two states (as it would
be unsound to join their shapes together in this case). We can lift this operator for abstract state ∆ as follows:W
W
W
join† (∆1 , ∆2 ) =d f match ∆1 , ∆2 with ( i σ1i ), ( j σ2j ) in i, j join(σ1i , σ2j )which essentially joins all pairs of disjunctions from the two abstract states, and makes a disjunction of them.
Widening operator. The finiteness of the shape domain is confirmed by the abstraction function. To ensure thetermination of the whole analysis, we still need to guarantee the convergence over the numerical domain. This task isaccomplished by the widening operator.
11

The widening operator widen(σ1 , σ2 ) is defined as
widen(σ1 , σ2 ) =d f
let σ01 , σ02 = rename(σ1 , σ2 ) inmatch σ01 , σ02 with (∃x1∗ · κ1 ∧ π1 ), (∃x2∗ · κ2 ∧ π2 ) inif κ1 ` κ2 ∗ true then ∃x1∗ , x2∗ · κ2 ∧ (widenπ (π1 , π2 ))else σ1 ∨ σ2

where the rename function has the same effect as above. Generally this operator is analogous to the join operator; theonly difference is that we expect (the shape part of) the second operand σ2 to be weaker than (that of) the first σ1 , sothat the widening reflects the trend of such weakening from σ1 to σ2 . In this case it applies the widening operation
widenπ (π1 , π2 ) over the numerical domain [18].
Based on the widening over conjunctive abstract states, we lift the operator over (disjunctive) abstract states:
W
W
W
widen† (∆1 , ∆2 ) =d f match ∆1 , ∆2 with ( i σ1i ), ( j σ2j ) in i, j widen(σ1i , σ2j )which is similar to its counterpart of the join operator.
The above three operations (abstraction, join and widening) provide termination guarantee while preserving soundness, as the following example demonstrates.
Example 4.1 (Abstraction, join and widening). Assume we have two abstract states, ∆0 = x::nodeh , x0 i∗x0 ::nodeh , nulliand ∆1 = x::nodeh , x0 i ∗ x0 ::nodeh , x1 i ∗ x1 ::nodeh , nulli. We would like to discover a sound approximation forboth states. Firstly we perform abstractions on both to obtain two abstract states, say, ∆00 = x::llhn0 i∧n0 =2 and ∆01 =x::llhn0 i ∧ n0 =3. Then these two are joined together according to shape similarity to be ∆001 = x::llhn0 i ∧ (n0 =2 ∨n0 =3), which transfers disjunction to the numerical domain. Finally the joined state is widened based on the first state∆00 , yielding a state x::llhn0 i ∧ n0 ≥2. It is a sound abstraction of both ∆0 and ∆1 , and finishes the analysis with one
more iteration.
4.3. Soundness and termination
4.3.1. Soundness
The soundness of our analysis relies on the underlying operational semantics of our programming language, which
is a small-step semantics consisting of transitions of the form:hs, h, ei,→hs1 , h1 , e1 iwhere s(s1 ) and h(h1 ) denote respectively the stacks and the heaps and where e(e1 ) denotes the program codes (anempty program code is denoted by -). The transitive closure of the above transition relation is denoted as ,→∗ . The
full details of the operational semantics are given in the Appendix. Soundness of analysis is important as it allows us
to directly use the loop invariant inferred without the need for another confirmation by either a user or a verifier.
We define the soundness of our analysis as follows:
Definition 4.1 (Soundness). Let ∆ denote the loop invariant synthesised by our analysis for a while loop while b {e}.
The analysis is sound if for all s, h, such that s, h |= ∆ and hs, h, ei,→∗ hs0 , h0 , -i (for some s0 , h0 ), we have s0 , h0 |= ∆.
The crux to prove the soundness of our analysis is to ensure that soundness is preserved during each step of ouranalysis. That is, the abstract semantics, the abstraction of shapes, the join operation and the widening operation
used in our analysis are all sound. From Lemma 4.2 on we will see that all these can be reduced to the soundness ofentailment proof provided by Sleek, which is already proven:
Lemma 4.1 (Soundness of entailment proof). For ∆1 and ∆2 , if ∆1 ` ∆2 holds, then for all s, h |= ∆1 , we haves, h |= ∆2 .
Proof. The soundness of the entailment proof is proven by Chin et. al [9].
12Lemma 4.2 (Soundness of abstract semantics). If |[e]|T ∆ = ∆1 , then for all s, h, if s, h |= ∆ and hs, h, ei,→hs1 , h1 , e1 i,then there always exists ∆0 such thats1 , h1 |= ∆0

and|[e1 ]|T ∆0 = ∆1

Proof. The proof is done by structural induction over program constructors and is left in the Appendix.
Lemma 4.3 (Soundness of abs). If abs(σ) = σ0 , then σ  σ0 .
Proof. The soundness proof of the first two substitution rules is trivial. For the Unreach rule, we can easily provethat x0 ::chv∗ i ∗ σ ` true ∗ σ, where σ is the frame part of the entailment check. By the Frame Rule of separation
logic, we only need to show that x0 ::chv∗ i ` true, which obviously is true. The result of rule Abs is obtained via afolding operation in Sleek against a user-defined predicate, so the soundness of this rule is guaranteed by that of theentailment proof in Sleek.
Lemma 4.4 (Soundness of join). If join(σ1 , σ2 ) = σ j , then we have σ1  σ j and σ2  σ j .
Proof. Let σ1 be (∃x1∗ · κ1 ∧ π1 ), and σ2 be (∃x2∗ · κ2 ∧ π2 ). By the definition of the join operator, we have three cases:• If κ1 ` κ2 ∗ true, we have σ j = ∃x1∗ , x2∗ · κ2 ∧ joinπ (π1 , π2 ). Then we need to show that ∃x1∗ · κ1 ∧ π1 `∃x1∗ , x2∗ · κ2 ∧ joinπ (π1 , π2 ) and ∃x2∗ · κ2 ∧ π2 ` ∃x1∗ , x2∗ · κ2 ∧ joinπ (π1 , π2 ), which are true because κ1 ` κ2 ∗ trueby condition, κ2 ` κ2 by separation logic, and π1 ` joinπ (π1 , π2 ) and π2 ` joinπ (π1 , π2 ) by the soundness of theconvex hull operator over the numerical domains [18].
• If κ2 ` κ1 ∗ true, the soundness proof is similar to the first case.
• Otherwise, we have σ j = σ1 ∨ σ2 . The soundness proof of this case is trivial.
Lemma 4.5 (Soundness of widen). If widen(σ1 , σ2 ) = σw , then we have σ1  σw and σ2  σw .
Proof. The proof of soundness of widen is similar to the soundness proof of join.
Based on the results above, we have
Theorem 4.1 (Soundness). Our analysis is sound with respect to the underlying operational semantics.
4.3.2. Termination
Next we show the termination of our analysis algorithm, which is based on two observations: the finiteness overthe shape domain and the termination over the numerical domain guaranteed by our widening operator. The first canbe proven by claiming the finiteness of the number of all possible abstract states only with the shape information:
recalling our analysis algorithm where we set an upper bound n for shared cutpoints (logical variables) that we keep
track of, we know that the number of program variables and logical variables preserved in our analysis are finite. Notethat the number of all shape predicates are also limited; therefore all the shape-only abstract states are finite. The
second is proven in the abstract interpretation frameworks for the numerical domains [18]. These two facts guarantee
the convergence of our analysis. Such a termination proof can help assure us that our analysis never goes into an
infinite loop, regardless of which loop it is made to analyse.
Lemma 4.6 (Finiteness of the abstract shape domain). With a finite number of program variables, logical variables, data node types and shape predicates, the abstract shape domain is finite.
Proof. Let the number of program variables, logical variables, data node types and shape predicates be m, n, l1
and l2 , respectively, and the maximal number of fields of data nodes or arguments of the predicates be k, wherem, n, l1 , l2 , k ∈ N are finite numbers. Note that the root parameter of a data structure is also counted in k. For example,
the number of arguments of predicate ll is 3. Based on the fact that the number of variables is (m + n), and k is
the number of holes for variables in one single predicate, we have the possible number of atomic formulae of thispredicate as (m + n)k . The number of shape structure is (l1 + l2 ), then the upper bound of the number of all possible
different atomic shape formulae is (l1 + l2 ) × (m + n)k + 1, where 1 is for when the shape formula is true. So therekare at most 2(l1 +l2 )×(m+n) +1 shape formulae in this shape domain. Since m, n, l1 , l2 and k are finite natural numbers, theshape domain is finite.
13

Definition 4.2. A (conjunctive) state σ is reducible if and only if abs(σ) 0 σ. If abs(σ) ` σ, then σ is irreducible, inwhich case we also say σ is stabilised.
Lemma 4.7 (Termination of abs). For all state σ, the application of the four abstraction operations over σ exhaustively (following the given order) will terminate in finite steps within a finite shape domain.
Proof. Let us apply abs over σ0 exhaustively to obtain a sequence σ1 , σ2 , · · · , σn , where n ∈ N. By the soundnessof abs, we have σ0 ` σ1 ` σ2 ` · · · ` σn , i.e. σ0  σ1  σ2  · · ·  σn . Since the shape parts of σ0,··· ,n are in a finite
shape domain, and the four abstraction rules do not alter the numerical parts of these states, there must exist a σi,0≤i≤nwhich is irreducible/stablised, i.e., σk = σi for all k ≥ i.
Lemma 4.8 (Termination of Widening). Within a finite shape domain, given a sequence σ0n (n ∈ N), the sequence
σn generated by σ0 = σ00 and σn+1 = widen(σn , σ0n+1 ) is ultimately stationary, i.e. ∃i · ∀k ≥ i · σk = σi .
Proof. The proof follows the idea of the widening termination proof in cofibered domains [19]. Similar to the proofof termination of abs, the shape part of σn will be stationary since the shape domain is finite. The termination of numerical part can be guaranteed by numerical join and widening [18]. Combining them together, σn will be stationary.
Based on the above results, we conclude the termination result about our analysis algorithm as follows.
Theorem 4.2 (Termination). The iteration of our fixpoint computation will terminate in finite steps, given a finite
number of method specifications, program variables and user-defined predicates, and given an upper bound on thenumber of logical variables to keep during the analysis.
5. Experiments and Evaluation
We have built a prototype system using Objective Caml. In our experiments, we use Sleek [11] as the solver forentailment proofs, and Omega constraint solver [20] and Fixcalc solver [18] for join and widening operations in the
numerical domain. Our test platform was an Intel Core 2 CPU 2.66GHz system with 8Gb RAM.
Example 5.1 (Merge). Fig. 6 shows a procedure merge which merges two sorted lists referred to by left and right
into one sorted list, and returns the merged list as result. The pre-condition of the while loop within the merge
procedure (starting at line 6) is calculated as:
left::sllhn1 , s1 , l1 i ∗ right::sllhn2 , s2 , l2 i ∧ r = null
The function append concatenates two sorted lists, which requires that the maximal value stored in the first input
list is smaller than or equal to the minimal value of the second input list, and ensures that it returns a concatenatedsorted list (referred to by res). The following is the specification of append:
node append(node x, node y)requires x::sllhn1 , s1 , l1 i∗y::sllhn2 , s2 , l2 i∧l1 ≤s2
ensures res::sllhn1 +n2 , s1 , l2 i;
By applying our analysis algorithm to the while loop in the program, we obtain the following loop invariant, which14

1 node merge(node left, node right)

14

node tmp = right;

requires left::sllhn1 , s1 , l1 i

15right = right.next;

16

tmp.next = null;17

r = append(r,tmp);

2∗ right::sllhn2 , s2 , l2 i
3ensures res::sllhn3 , s3 , l3 i∧n3 =n1 +n2∧s3 =min(s1 , s2 )∧l3 =max(l1 , l2 );

18

4 {
5

node r = null;

6

while (left != null && right != null){

7

}

19

}

20

if (left == null) {21

if (left.val <= right.val) {r = append(r, right);

22}left = left.next;

23

else {

10

tmp.next = null;24

11

r = append(r,tmp);

25}
return r;

8

node tmp = left;

9

12

}

26

13

else {

27 }r = append(r, left);

Figure 6: Merge two sorted linked list.
contains seven different disjunctive branches, with each branch describing a different situation:
left::sllhn1 , s1 , l1 i ∗ right::sllhn2 , s2 , l2 i ∧ r = null(7)

∨ r::nodehs1 , nulli ∗ right::sllhn2 , s2 , l2 i ∧ left = null ∧ s1 = l1 ∧ s1 <s2(8)∨ r::nodehs2 , nulli ∗ left::sllhn1 , s1 , l1 i ∧ right = null ∧ s2 = l2 ∧ s2 ≤s1(9)∨ r::nodehs3 , nulli ∗ left::sllhn01 , s01 , l1 i ∗ right::sllhn02 , s02 , l2 i
∧ (s3 = s1 ∧ s1 <s2 ∧ n1 = n01 + 1 ∧ n02 = n2 ∧ s1 ≤s01 ∧ s02 = s2
∨ s3 = s2 ∧ s2 ≤s1 ∧ n2 = n02 + 1 ∧ n01 = n1 ∧ s2 ≤s02 ∧ s01 = s1 )∨ r::sllhn3 , s3 , l3 i ∗ right::sllhn02 , s02 , l2 i ∧ left = null ∧ n3 = n1 + n2 − n02∧ s3 = min(s1 , s2 ) ∧ l3 = l1 ∧ l1 <s02
∨ r::sllhn3 , s3 , l3 i ∗ left::sllhn01 , s01 , l1 i ∧ right = null ∧ n3 = n2 + n1 − n01∧ s3 = min(s1 , s2 ) ∧ l3 = l2 ∧ l2 ≤s01
∨ r::sllhn3 , s3 , l3 i ∗ left::sllhn01 , s01 , l1 i ∗ right::sllhn02 , s02 , l2 i
∧ n3 = n1 − n01 + n2 − n02 ∧ s3 = min(s1 , s2 ) ∧ l3 ≤min(s01 , s02 )

(10)
(11)
(12)
(13)

The branch (7) represents the state before any iteration. The branches (8), (9), and (10) denote three special
scenarios after one iteration. The branch (8) (resp. (9)) denotes the case where initially the left (resp. right)
list contains only one node which holds a value no bigger than any value stored in the right (resp. left) list, andafter one iteration, r refers to the sole node in the initial left (resp. right) list and the left (resp. right) pointerbecomes null. The branch (10) denotes the scenario where after one iteration neither the left list nor the right
list is empty but r still refers to the node with the smallest value. The branches (11) , (12) and (13) denote possible
states reached after some (one or more) iterations. The branch (11) (resp. (12)) denotes the state reached after someiterations where the left (resp. right) pointer has traversed to the end of the list. The branch (13) denotes the case15

Zero iteration

left

sll<n1,s1,l1>

right

sll<n2,s2,l2>

null

rleft.next=null ˄
s1≤s2
left

r

left

left

right
r

sll<n1,s1,l1>

null

right

sll<n2,s2,l2>
Node<s1,null>(8)

tail of left is reachedMore iterations

otherwise, after one
iterationright.next=null
˄ s2 ≤ s1

null

One iteration right(7)

r

Node<s2,null>

left

sll<n1’,s1’,l1’>

rightsll<n2’,s2’,l2’>

r

(9)

left
sll<n2’,s2’,l2’>sll<n3,s3,l3>

(11)

left

sll<n1’,s1’,l1’>

rightsll<n2’,s2’,l2’>sll<n1’,s1’,l1’>

right

null

r

(10)

otherwise

tail of right is reachednull

Node<s3,null>

sll<n3,s3,l3>

(12)

r

sll<n3,s3,l3>(13)

Figure 7: Shape of each branch of the generated loop invariant in the merge example.

where neither the left pointer nor the right pointer has reached the end of their list after some iterations. In allthese three branches, r refers to the merged list obtained so far. The shape of each branch is demonstrated in Fig. 7.
Note that branches (8), (9) and (10) are, respectively, special cases of branches (11), (12) and (13) (logically, theformer formulae entail the latter ones, respectively). So we can simplify the loop invariant as
r::sllhn3 , s3 , l3 i ∗ right::sllhn02 , s02 , l2 i ∧ left = null ∧ n3 = n1 + n2 − n02∧ s3 = min(s1 , s2 ) ∧ l3 = l1 ∧ l1 <s02
∨ r::sllhn3 , s3 , l3 i ∗ left::sllhn01 , s01 , l1 i ∧ right = null ∧ n3 = n2 + n1 − n01∧ s3 = min(s1 , s2 ) ∧ l3 = l2 ∧ l2 ≤s01
∨ r::sllhn3 , s3 , l3 i ∗ left::sllhn01 , s01 , l1 i ∗ right::sllhn02 , s02 , l2 i
∧ n3 = n1 − n01 + n2 − n02 ∧ s3 = min(s1 , s2 ) ∧ l3 ≤min(s01 , s02 )An immediate benefit to simplify the generated loop invariant is to reduce the number of disjunctions. Therefore, it
can lead to the increase of the scalability of our inference system. It also simplifies the verification process whichmakes use of the loop invariant. Note that the soundness of our analysis ensures that we do not need to re-verify thewhile-loop with the inferred invariant; instead, we can directly move on to verify the code fragment after the while
loop, starting with the inferred loop invariant conjoined with the negation of the loop test (a sound postcondition for
the while loop). 2
Table 1 depicts some of the programs we have conducted experiments with, including list processing programs,
sorting algorithms, tree processing programs, and loops code from FreeRTOS [21]. Total LOC is the total numberof lines of the code. The first column denotes the names of the programs. The second column states the programs’
functionalities. The last column exhibits the time in second taken by our analysis. As can be seen from their functions,these programs involve recursive data structures such as (sorted) linked lists and binary (search) trees, and employ
loops to manipulate these data structures (and some of them even have nested loops). Our target is to verify these16Program
FunctionTime
List processing programs(Total LOC: 232)
createCreates a list with given length parameter
0.452
deleteDisposes a list
0.720
traverse
Traverses a list
0.636
lengthCounts the length of a list
0.772
appendAppends two sorted lists
0.312
take
Takes the first n elements of a list, or itself
0.852
drop
Returns suffix of a list after the first n elements, or empty 0.844
reverse
Reverse the elements of the list, in place
1.032
filterDrops the elements bigger than k of a list
1.182
lookupReturns the first node whose values equals to k, or null 0.876
drop evenDrops all the elements whose indexes are even
1.332
Sorting list processing programs(Total LOC: 178)
ins sort(inner) Inner loop of Fig. 1
0.824
ins sort(outer) Outer loop of Fig. 1
4.372
partition
Auxiliary operation used by Quick-sort
1.497
merge
Merges two sorted lists to be one sorted list
1.972
Divides
a
list
into
two
sublists
with
split
0.354
length difference of at most one
selectSelects the smallest node of a list
0.692
select sort
Outer loop of selection sort
4.892
Tree processing programs(Total LOC: 87)
tree search
Finds a node in a binary search tree
1.294
tree insert
Inserts a node into a binary search tree
1.364
list2tree
Inserts nodes of a list into a binary search tree
5.176
FreeRTOS(Total LOC: 331)
list.cOne loop in FreeRTOS list.c with heap manipulation
4.124
task.cSix loops in FreeRTOS task.c with heap manipulation
32.18
Table 1: Selected Experimental Results.

programs without the need of user annotations for loops that occurred in them. Our analysis is employed to automatically infer loop invariants for those while loops. Our experiments confirms that Hip/Sleek can verify all these
programs successfully when supplied with loop invariants discovered by our analysis. According to our experience,these experiments just require the bound of shared cutpoints be a reasonably small number, say no more than twice ofthe number of program variables. Note that, it takes longer to analyse the procedures that have nested loops, such as
select sort, list2tree, and so on, because we need to analyse the inner loop multiple times. We translated thesource code of the FreeRTOS kernel to our language, and successfully inferred the loop invariants of the loops which
do not involve pointer arithmetic in list.c and task.c. We employ double linked sorted list predicate for the verificationof FreeRTOS.
We have two main observations from our experimental results. The first is that we can handle many different
kinds of data structures with rich program properties they exhibit. To analyse these loops, we need to deal withboth single linked and double linked list predicates to capture the list data structure, as well as their sorted version
for the sorting algorithms. We can also handle tree-like predicates such as binary trees and binary search trees.
Meanwhile these predicates also capture various numerical information such as the length of the list and size/heightof the tree, and the minimum/maximum value of a sorted list/binary search tree. With these predicates, our analysis iscapable of capturing sophisticated numerical invariants, which are simply captured as constraints over the parametersof predicates involved.
17

Beyond the number of predicates and properties we can process, another observation on our analysis is that wecan process them rather precisely. For example, the list creation program creates a list with the same length as a user
input; the list traverse program does not change list’s length; all elements of the return list of the filter program aresmaller than or equal to the input value k; and the length of the return list of the drop even program is between halfand half+1 of the length of the original list.
Moreover, critical information may be required from some loops for their enclosing procedures to function correctly. For example, the quicksort algorithm partitions a list into three parts, where two are lists and the third just
one node, whose value is exactly in the middle of that of the two other lists (partition in the table). We use a list
bound predicate to indicate that fact which is successfully inferred by our analysis. We can also infer that the first
loop of a mergesort (split in the table) can divide the list into two where their length difference is at most one; suchinformation might be unimportant for the algorithm’s functional correctness but can be essential for its performance.
For tree insert, we have the result that the tree’s height is increased at most one, and the minimum/maximum
value of the new binary search tree will be exactly the inserted value, if that value is outside the value bounds of theoriginal tree. For code in FreeRTOS, the invariants we inferred maintain the sortedness property for the double linked
list used for tasks. The invariants we discovered are sufficiently precise to prove the functional correctness of theircorresponding programs with the given predicates.
6. Related Work and Conclusion
Related work. For heap-manipulating programs with any form of recursion (be it loop or recursive method call),dramatic advances have been made in synthesising their invariants/specifications. The local shape analysis [13] infers
loop invariants for list-processing programs, followed by the SpaceInvader tool to infer full method specifications
over the separation domain, so as to verify pointer safety for larger industrial codes [12, 14]. The SLAyer tool [22]implements an inter-procedural analysis for programs with shape information. The Hob system [15] employs a setbased specification technique to describe heap objects and to reason about the programs, where a similar loop invariant
inference algorithm is proposed. In their fixed-point iteration algorithm, the join operator is designed to find common
conjuncts of pre- and post-states, and there is no need for a widening operator since it is designed for a simple
heap abstract domain. Their analysis allows certain conjuncts to be dropped from the post-state to avoid too many
iterations and to enforce termination. Our analysis is designed for a more complex abstract domain leveraging bothshape and numerical information. It requires a widening operator to ensure convergence, and it avoids direct pruningon post-states in order to make inferred loop invariants as precise as possible. To deal with also size information(such as number of nodes in lists/trees), THOR [16] derives a numerical program from the original heap-processing
one in a sound way, such that the size information can be obtained with a traditional loop invariant synthesis. A
similar approach [23] combines a set domain (for shape) with its cardinality domain (for corresponding numericalinformation) in a more general framework. Compared with these works, our approach can handle data structureswith stronger invariants such as sortedness and binary search property, which have not been addressed in the previous
works.
One more work to be mentioned is the relational inductive shape analysis [24]. It employs inductive checkers
to express both shape and numerical information. Our approach has two advantages over theirs: firstly, we try tokeep as many as possible shared cutpoints (logical variables) during the analysis (within a preset bound), whereas
they do not preserve such cutpoints (which is witnessed by their joining rules over the shape domain). Therefore ouranalysis is essentially more precise than theirs, e.g. in the second scenario of (6) described in Section 4.2. Meanwhile,
our approach can deal with data structures with loops in them (say cyclic linked-lists), whereas they do not have amechanism to handle it. An example in point is the state x::lshm, yi ∗ y::lshy, ni ∧ n>0 involving both a sharedcutpoint y and a circled list y::lshy, ni ∧ n>0, neither of which can be handled by their work (while ours is capableof that). Another advantage of our approach over theirs is that they only demonstrate how to analyse a program with
one particular shape. For instance, they analyse programs which manipulate binary search trees and red-black trees
without changing the variety of shapes in the heap. Comparatively, we allow different predicates to appear in theanalysis of one program, like in our motivating example (thanks to our more flexible abstraction operation).
There are also many other approaches that can synthesise shape-related program invariant, other than those basedon separation logic. The shape analysis framework TVLA [25] is based on three-valued logic. It is capable ofhandling complicated data structures and properties, such as sortedness. Guo et al. [26] report a global shape analysis
18

that discover inductive structural shape invariants from the code. Kuncak et al. [27] develop a role system to express
and track referencing relationships among objects, where an object’s role (type) depends on, and changes according
to, the mutation of its referencing. Hackett and Rugina [28] can deal with AVL-trees but is customised to handle only
tree-like structures with height property. Compared with these works, separation logic based approach benefits fromthe frame rule and hence supports local reasoning.
Classical abstract interpretation [17] and its applications such as automated assertion discovery [29, 30, 31, 32]
mainly focus on finding numerical program properties. Compared with their works, ours is also founded on the
abstract interpretation framework but tries to discover loop invariants with both separation and numerical information.
Meanwhile, we can also utilise their techniques of join and widening to reason about the numerical domain, as we didfor the work [18].
Concluding Remarks. We have reported an analysis which allows us to synthesise sound and useful loop invariants
over a combined separation and numerical domain. The key components of our analysis include novel operations for
abstraction, join and widening in the combined domain. We have built a prototype system and the initial experimental
results are encouraging.
Acknowledgement. This work was supported in part by EPSRC Projects EP/G042322 and MOE Project 2009-T2-1063. We thank Florin Craciun for his invaluable comments on an earlier version of this paper and to Steve Dunne forhis help in proof reading.
Reference[1] S. Ishtiaq, P. O’Hearn, Bi as an assertion language for mutable data structures, in: POPL ’01: Proceedings of the 28th
ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, New York, NY, USA, 2001, pp. 14–26.
doi:http://doi.acm.org/10.1145/360204.375719.
[2] J. C. Reynolds, Separation logic: a logic for shared mutable data structures, in: Proceedings of the Seventeenth Annual IEEE Symposium on
Logic in Computer Science, 2002, pp. 55–74. doi:10.1109/LICS.2002.1029817.
[3] J. Berdine, C. Calcagno, P. O’Hearn, Smallfoot: Modular automatic assertion checking with separation logic., in: International Symposium
on Formal Methods for Components and Objects, Vol. 4111 of LNCS, Springer, 2005.
[4] J. Berdine, B. Cook, D. Distefano, P. OHearn, Automatic termination proofs for programs with shape-shifting heaps, in: Computer Aided
Verification, Springer, 2006, pp. 386–400.
[5] W. Chin, C. David, H. Nguyen, S. Qin, Enhancing modular oo verification with separation logic, in: Proceedings of the 35th annual
ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL ’08, ACM, New York, NY, USA, 2008, pp. 87–
99. doi:http://doi.acm.org/10.1145/1328438.1328452.
URL http://doi.acm.org/10.1145/1328438.1328452[6] M. Parkinson, G. Bierman, Separation logic, abstraction and inheritance, in: Proceedings of the 35th annual ACM SIGPLANSIGACT symposium on Principles of programming languages, POPL ’08, ACM, New York, NY, USA, 2008, pp. 75–86.
doi:http://doi.acm.org/10.1145/1328438.1328451.
URL http://doi.acm.org/10.1145/1328438.1328451[7] K. Leino, Dafny: An automatic program verifier for functional correctness, in: International Conference on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR), Citeseer, 2010.
[8] W. Chin, C. David, H. Nguyen, S. Qin, Automated verification of shape, size and bag properties, in: Proc. 12th IEEE International Conference
on Engineering Complex Computer Systems, 2007, pp. 307–320. doi:10.1109/ICECCS.2007.17.
[9] W. Chin, C. David, H. Nguyen, S. Qin, Automated verification of shape, size and bag properties via user-defined predicates in separation
logic, Science of Computer Programming 77 (9) (2012) 1006 – 1036. doi:DOI: 10.1016/j.scico.2010.07.004.
[10] H. H. Nguyen, W. Chin, Enhancing program verification with lemmas, in: CAV ’08: Proceedings of International Conference on Computer
Aided Verification 2008, LNCS, Springer, 2008.
[11] H. Nguyen, C. David, S. Qin, W. Chin, Automated verification of shape and size properties via separation logic., in: VMCAI 2007: Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation, Vol. 4349 of Lecture Notes in
Computer Science, 2007.
[12] C. Calcagno, D. Distefano, P. O’Hearn, H. Yang, Compositional shape analysis by means of bi-abduction, in: Proceedings of the ACM
Symposium on Principles of Programming Languages (POPL), ACM Press, Savannah, Georgia, USA, 2009.
[13] D. Distefano, P. O’Hearn, H. Yang, A local shape analysis based on separation logic, in: Tools and Algorithms for the Construction andAnalysis of Systems, Vol. 3920 of LNCS, Springer, 2006.
[14] H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O’Hearn, Scalable shape analysis for systems code, in: Proceedingsof the 20th international conference on Computer Aided Verification, CAV ’08, Springer-Verlag, Berlin, Heidelberg, 2008, pp. 385–398.
doi:http://dx.doi.org/10.1007/978-3-540-70545-1 36.
URL http://dx.doi.org/10.1007/978-3-540-70545-1_36[15] P. Lam, The hob system for verifying software design properties, Ph.D. thesis, Massachusetts Institute of Technology (February 2007).
[16] S. Magill, M. Tsai, P. Lee, Y. Tsay, Thor: A tool for reasoning about shape and arithmetic, in: Computer Aided Verification, Springer, 2008,
pp. 428–432.

19[17] P. Cousot, R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of
fixpoints, in: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
ACM Press, New York, NY, Los Angeles, California, 1977, pp. 238–252.
[18] C. Popeea, W. Chin, Inferring disjunctive postconditions, in: Proceedings of the 11th Asian computing science conference on Advances incomputer science: secure software and related issues, Springer-Verlag, 2006, pp. 331–345.
[19] A. Venet, Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs, in: Proceedings of the Third International
Symposium on Static Analysis, Springer-Verlag, 1996, pp. 366–382.
[20] W. Pugh, The omega test: a fast and practical integer programming algorithm for dependence analysis, in: Proceedingsof the 1991 ACM/IEEE conference on Supercomputing, Supercomputing ’91, ACM, New York, NY, USA, 1991, pp. 4–13.
doi:http://doi.acm.org/10.1145/125826.125848.
URL http://doi.acm.org/10.1145/125826.125848[21] The FreeRTOSTM project website, uRL: http://www.freertos.org.
[22] A. Gotsman, J. Berdine, B. Cook, Interprocedural shape analysis with separated heap abstractions, in: Static Analysis Symposium 2006
(SAS’06), 2006.
[23] S. Gulwani, T. Lev-Ami, M. Sagiv, A combination framework for tracking partition sizes, in: Proceedings of the 36th annual ACM
SIGPLAN-SIGACT symposium on Principles of programming languages, POPL ’09, ACM, New York, NY, USA, 2009, pp. 239–251.
doi:http://doi.acm.org/10.1145/1480881.1480912.
URL http://doi.acm.org/10.1145/1480881.1480912[24] B. E. Chang, X. Rival, Relational inductive shape analysis, in: Proceedings of the ACM SIGPLAN - SIGACT Symposium on Principles ofProgramming Languages, 2008.
[25] M. Sagiv, T. Reps, R. Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems
24 (3) (2002) 217–298.
[26] B. Guo, N. Vachharajani, D. I. August, Shape analysis with inductive recursion synthesis, in: Proceedings of the ACM SIGPLAN 2007
Conference on Programming Language Design and Implementation, 2007.
[27] V. Kuncak, P. Lam, M. Rinard, Role analysis, in: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, 2002, pp. 17–32.
[28] B. Hackett, R. Rugina, Region-based shape analysis with tracked locations, in: POPL ’05: Proceedings of the 32nd ACM
SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, New York, NY, USA, 2005, pp. 310–323.
doi:http://doi.acm.org/10.1145/1040305.1040331.
[29] P. Cousot, R. Cousot, On abstraction in software verification, in: Proceedings of the 14th International Conference on Computer Aided
Verification, Springer-Verlag, London, UK, 2002, pp. 37–56.
URL http://portal.acm.org/citation.cfm?id=647771.734276[30] L. Kovacs, T. Jebelean, An algorithm for automated generation of invariants for loops with conditionals, in: Proceedings of the SeventhInternational Symposium on Symbolic and Numeric Algorithms for Scientific Computing, IEEE Computer Society, Washington, DC, USA,2005, pp. 245–. doi:10.1109/SYNASC.2005.19.
URL http://portal.acm.org/citation.cfm?id=1114699.1115427[31] K. Leino, F. Logozzo, Loop Invariants on Demand, in: Programming languages and systems: third Asian symposium, APLAS 2005, Tsukuba,
Japan, November 2-5, 2005: proceedings, Springer Verlag, 2005, p. 119.
[32] C. A. Furia, B. Meyer, Fields of logic and computation, Springer-Verlag, Berlin, Heidelberg, 2010, Ch. Inferring loop invariants using
postconditions, pp. 277–300.
URL http://portal.acm.org/citation.cfm?id=1983702.1983719

Appendix A. Appendix
Appendix A.1. Semantic for Pure Formulae
The semantic model for pure (numerical) formulae s |=A π is given in Figure A.8.
Appendix A.2. Operational Semantics
This section defines the operational semantics of our programming language. It is a small-step semantics which
are essentially transitions between machine configurations. Each machine configuration is a triple consisting of:• Heap h. As mentioned earlier we model heaps as finite partial maps from locations to object values. Object
values are expected to conform to their defined class types.
• Stack s. Stacks are modelled as finite maps from variables to values. Note that a stack s is viewed as a “stackable” mapping, where a variable v may occur several times, and s(v) always refers to the value of the variable vthat was popped in most recently. A more formal definition for stacks would mkare different occurrences of thesame variable with different “frame” numbers. We omit the details here.
• Current program code e. Program execution terminates when e is -, a value of type void.
20

s |=A γ1 ∧ γ2
s |=A p1 ./ p2
s |=A p ./ nulls |=A trues |=A falses |=A vs |=A b1 = b2
s |=A v1 = v2
s |=A v1 ≤ v2
s |=A φ1 ∧ φ2
s |=A φ1 ∨ φ2
s |=A ¬φs |=A ∃v · φs |=A ∀v · φ

iff
iff
iff
always
never
iff
iff
iff
iff
iff
iff
iff
iff
iff

s |=A γ1 and s |=A γ2
s(p1 ) ./ s(p2 ), where ./ ∈ {=, ,}s(p) ./ 0, where ./ ∈ {=, ,}s(v) = trues(b1 ) = s(b2 )s(v1 ) = s(v2 )s(v1 ) ≤ s(v2 )s |=A φ1 and s |=A φ2
s |=A φ1 or s |=A φ2
s |=A φ does not holds |=A [k/v]φ for some ks |=A [k/v]φ for all k

Figure A.8: The semantic model for numerical constraints.

Each reduction step can then be formalised as a small-step transition of the form:hs, h, ei,→hs1 , h1 , e1 i
The full set of transitions is given in Figure A.9. We explain some of the notations used in them. The operation[v 7→ ν] + s “pushes” the variable v to s with the value ν, and ([v 7→ ν] + s)(v) = ν. The operation s − v∗ “pops out”
variables v∗ from the stack s. s[v7→k] is a mapping which keeps all the mappings in s except that of v (which is
now specified to be mapped to k). We also abuse this notation for a class type identifier c to denote a region of heap
(mappings) in the form c[ f1 7→ s(v1 ), . . . , fn 7→ s(vn )], which is essentially a heap location where fields fi are further
mapped to values s(vi ), i = 1, . . . , n. ⊥ represents an arbitrary value. We also introduce an intermediate construct as
results returned by expressions/method calls ret(v∗ , e), where v∗ will be dropped from s after the evaluation/invocationof e, to simulate the behaviour of stack. Whenever such a result is yielded, we assume it is stored in a special logicalvariable res, although res is never explicitly put in the stack s.
Appendix A.3. Proof of Soundness of Abstract Semantics
In this section we prove the following lemma to complete the soundness proof for our analysis:
Lemma 4.2 (Soundness of Abstract Semantics). If |[e]|T ∆ = ∆1 , then for all s, h, if s, h |= ∆ and hs, h, ei,→hs1 , h1 , e1 i,then there always exists ∆0 such thats1 , h1 |= ∆0

and|[e1 ]|T ∆0 = ∆1

Proof. The proof is done by structural induction over program constructors:• Case null | k | v | v. f . Straightforward.
• Case v := e. There are two cases according to the operational semantics:– e is not a value. From operational semantics, there is e1 s.t. hs, h, ei,→hs1 , h1 , e1 i, and hs, h, v=ei,→hs1 , h1 , v=e1 i.
From abstract semantics for assignment, if |[e]|T ∆ = ∆2 , and ∆1 =[v1 /v, r1 /res](∆2 )∧v=r1 . By induction
hypothesis, there exists ∆0 ,s1 , h1 |= ∆0 and |[e1 ]|T ∆0 = ∆2 . It concludes from the assignment rule that |[v = e1 ]|T ∆0 = ∆1 .
– e is a value. Trivial.
21

OS-VARhs, h, vi,→hs, h, s(v)i

OS-CONSThs, h, ki,→hs, h, ki

OS-SEQhs, h, -; ei,→hs, h, ei

OS-ASSIGN-1

hs, h, v:=ki,→hs[v7→k], h, -i

OS-FIELD-READ

hs, h, v. f i,→hs, h, h(s(v))( f )i

OS-LOCALhs, h, {t v; e}i,→h[v7→⊥]+s, h, ret(v, e)i

OS-RET-1

hs, h, ret(v∗ , k)i,→hs−{v∗ }, h, ki
hs, h, e1 i,→hs1 , h1 , e3 ihs, h, e1 ; e2 i,→hs1 , h1 , e3 ; e2 ihs, h, ei,→hs1 , h1 , e1 ihs, h, v:=ei,→hs1 , h1 , v=e1 ihs, h, ei,→hs1 , h1 , e1 ihs, h, ret(v∗ , e)i,→hs1 , h1 , ret(v∗ , e1 )ir = h(s(v1 ))[ f 7→ s(v2 )] h1 = h[s(v1 )7→r]
hs, h, v1 . f := v2 i,→h(s, h1 )is(v)=truehs, h, if v then e1 else e2 i,→hs, h, e1 is(v)=false
hs, h, if v then e1 else e2 i,→hs, h, e2 i

OS-PROG

OS-ASSIGN-2

OS-RET-2

OS-FIELD-WRITE

OS-IF-1

OS-IF-2

OS-NEW

OS-WHILE-1

OS-WHILE-2

OS-CALL

data c {t1 f1 , .., tn fn }ι<dom(h) r=c[ f1 7→ s(v1 ), .., fn 7→ s(vn )]hs, h, new c(v∗ )i,→hs, h[ι 7→ r], ιis(b)=truehs, h, while (b) {e}i,→hs, h, e; while (b) {e}is(b)=false
hs, h, while (b) {e}i,→hs, h, -i
s1 =s[wi 7→ s(vi )]ni=1
t0 mn((ti wi )ni=1 ){e}hs, h, mn(v∗ )i,→hs1 , h, ret({wi }ni=1 , e)i

Figure A.9: Operational semantics.

22• Case new c(v∗ ). From abstract semantics for new, we have |[new c(v∗ )]|T ∆ = ∆1 , where ∆1 = ∆ ∗ res::chv01 , . . . , v0n i.
Let ∆0 = ∆1 . From the operational semantics, we have hs, h, new c(v∗ )i,→hs, h+[ι 7→ r], ιi, where ι < dom(h).
From s, h |= ∆, we have s, h+[ι 7→ r] |= ∆0 . Moreover, |[ι]|T ∆0 = ∆1 .
• Case v1 . f := v2 . Take ∆0 = ∆. It concludes immediately from the exec rule for field update and the underlying
operational semantics.
W
W• Case free(x). Denote ∆ as i (x::chy∗i i ∗ σi ) and ∆0 as i σi , then from free’s operational semantics we knowthat if s, h |= ∆ and hs, h, free(x)i,→hs1 , h1 , -i, then s1 , h1 |= ∆0 and ∆0 = ∆1 .
• Case e1 ; e2 . We consider the case where e1 is not a value (otherwise it is straightforward). From the operationalsemantics, we have hs, h, e1 i,→hs1 , h1 , e3 i. From the abstract semantics rule for sequence, we have ` {∆}e1 {∆2 }.
By induction hypothesis, there exists ∆0 s.t. s1 , h1 |= ∆0 , and ` {∆0 }e3 {∆2 }. By the sequential rule we have|[e3 ; e2 ]|T ∆0 = ∆1 .
• Case if v then e1 else e2 . There are two possibilities in the operational semantics:– s(v)=true. We have hs, h, if v then e1 else e2 i,→hs, h, e1 i. Let ∆0 = (∆∧v). It is obvious that s, h |= ∆0 .
From the if-conditional rule of abstract semantics, we have:|[e1 ]|T ∆0 = ∆2|[e2 ]|T ∆∧¬v0 = ∆3
And we also have (due to sound weakening of postcondition)|[e1 ]|T ∆0 = ∆2 ∨∆3That is, |[e1 ]|T ∆0 = ∆1 .
– s(v) = false. Analogous.
Wp• Case mn(v1...n ). For the method invocation rule, we know ∆`ρΦipr ∗ ∆i , for i = 1, . . . , p. Take ∆0 = i=1
ρΦipr ∗∆i .
From the operational semantics and the above heap entailment, we have s1 , h1 |= ∆0 . Then the method invocation rule implies ∀i∈1 . . . p · |[e1 ]|T ρΦipr ∗∆i = ∆i ∗Φipo . Therefore we have |[e1 ]|T ∆0 = ∆1 which concludes.

23