Enhancing Modular OO Verification with Separation Logic
Wei-Ngan Chin 

Cristina David

Huu Hai Nguyen Shengchao Qin

Departmentof Computer Science, National University of Singapore, SingaporeComputer
Science Programme, Singapore-MIT Alliance, Singapore
Department of Computer Science, Durham University, UKchinwn,davidcri,nguyenh2 @comp.nus.edu.sg shengchao.qin@durham.ac.uk

Abstract
Conventional specifications for object-oriented (OO) programsmust adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently
weakens the specifications of overridden methods in superclasses,
leading to imprecision during program reasoning. To address this,we advocate a fresh approach to OO verification that focuses on the
distinction and relation between specifications that cater to callswith static dispatching from those for calls with dynamic dispatching. We formulate a novel specification subsumption that can avoid
code re-verification, where possible. Using a predicate mechanism,
we propose a flexible scheme for supporting class invariant andlossless casting. Our aim is to lay the foundation for a practicalverification system that is precise, concise and modular for sequential OO programs. We exploit the separation logic formalism toachieve this.
Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; D.3.3 [Programming Languages]: Language Construct and Features; F.3.1 [Logics andMeanings of Programs]: Specifying, Verifying and Reasoning
about Programs
General Terms

Languages, Theory, Verification

Keywords Automated Verification, Enhanced Subsumption, Separation Logic, Lossless Casting, Static and Dynamic Specifications.

1. Introduction
Object-based programs are hard to statically analyse mostly because of the need to track object mutations in the presence ofaliases. Object-oriented (OO) programs are even harder, as we haveto additionally deal with class inheritance and method overriding.
One major issue to consider when verifying OO programs is
how to design specification for a method that may be overridden byanother method down the class hierarchy, such that it conforms tomethod subtyping. In addition, it is important to ensure that subtyping is observed for object types in the class hierarchy, including any
class invariant that may be imposed. From the point of conformance
to OO semantics, most analysis techniques uphold Liskov’s Substitutivity Principle (Liskov 1988) on behavioral subtyping. Under

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
POPL’08, January 7–12, 2008, San Francisco, California, USA.
Copyright c 2008 ACM 978-1-59593-689-9/08/0001. . . $5.00

this principle, an object of a subclass can always be passed to alocation where an object of its superclass is expected, as the object from each subclass must subsume the entire set of behaviors
from its superclass. To enforce behavioral subtyping for OO programs, several past works (Dhara and Leavens 1996; Barnett et al.
2004; Kiniry et al. 2005) have advocated for class invariants to be
inherited by each subclass, and for pre/post specifications of theoverriding methods of its subclasses to satisfy a specification subsumption (or subtyping) relation with each overridden method of
its superclass.
Each specification of a method (or a piece of code) is typicallygiven as a pair   of precondition  and postcondition . We use an infix notation   to denote such a specification. A basic specification subsumption mechanism was originally formulated as follows. Consider a method   in class with ! "# as its pre/post specification, and its overriding method $  in subclass $ , with a given pre/post specification
#%& '%! . The specification #%& (%# is said to bea subtype of !) *# in support of method overriding, if
the following subsumption relation holds:+-,-. / type 021354678:9 ;'<>=+-,-. %+@? 61%A<>=+0 -,-. %CB D +@? 61%!7E8:9 %F0 +-,-. &B D +@? 617+@? 61

The two conditions are to ensure contravariance of preconditions, and covariance on postconditions. They follow directly fromthe subtyping principle on methods’ specifications. As the two
specifications are from different classes, we add the subtype constraint type #G-H##JILK $ to allow the above subsumption relation to bechecked for the same $ subclass. To reflect this, we parameterize
the subsumption operator ILK % with a $ -class as its suffix.
The main purpose of using specification subsumption is to support modular reasoning by avoiding the need to re-verify the codeof overriding method $  with the specification #) '#
of its overridden method   . In the case that specification subsumption does not hold, an alternative way to achieve behavioral
subtyping is to use the specification inheritance technique of Dhara
and Leavens (1996) to strengthen the specification of each overriding method with the specification of its overridden method, as
follows:
Consider a method   in class  with #M '# as its
pre/post specification, and its overriding method $  in subclass $ ,with pre/post specification #%) N%# . To ensure specification subsumption, we can strengthen the specification of the overriding method via specification inheritance with the intersection of
their specifications, namely:#%O P%#RQS !T type #G-H##JILK $& P# .
Specification inheritance requires the use of multiple specifications (or intersection type) to provide for a more expressive mechanism to describe each method. By inheriting a new specification
for the overriding method, this technique uses code re-verificationitself to ensure that a behavioral subtyping property would be enforced. We can generalise a definition of the subsumption relation
between two multiple specifications, as follows:[##u$!LAH]lu$!_Helj#G-H# luK ellHZ]H#[Zv-2#G-H# luK L#G-H# lu c#
HF#2>#G-H# lulHZR!#_H]#G-H# luK e

D EFINITION 1.1 (Multi-Specifications Subsumption). Given two
multiple specifications, QLUVXW>YRZ[ V (for class  ) and Q]\ ^_W>YRZ[!$ ^(for subclass $ ), where each of Z[ V and Z[!$ ^ is a pre/post
annotation of the form E * . We say that they are in specification subsumption relation, 2QL\ ^_W>YOZ[!$ ^ EILK %]2QRUVXW>YOZ[ V  ,if the following holds : `5ab>c  edfHbgc  ihZ[!$ ^ ILK %jZ[ V .
While modular reasoning can be supported by the above subsumption relations, the reasoning were originally formulated in theframework of Hoare logic. Recently, separation logic has been proposed as an extension to Hoare logic, providing precise and concise reasoning for pointer-based programs. A key principle followed in separation logic is the use of local reasoning to facilitate
modular analysis/reasoning. An early work on applying separation
logic to the OO paradigm was introduced by Parkinson and Bierman (2005). In that work, two key concepts were identified. Firstly, 
an abstract predicate family k l Y   l  was used to capture someUprogram states for objects of class hierarchy with type  . Each abstract predicate has a visibility scope and is allowed to have a different number of parameters, depending on the actual type of its
root object. Moreover, each predicate family acts as an extensible
predicate for which incremental specification is given and verified
for each class. Secondly, the concept of specification compatibility was introduced to capture the subsumption relation soundly, as
follows:
A specification #%m n% is said to be compatible with
!C P# under all program contexts, if the following holds:
ogp ?q-.:r  +-,-.

 +-,-.
pp% ?q-. +@? 61%s<>= ?q-. +@? 61
0 +-,-. %CB D +@? 61%!7E8:90 +-,-. &B D +@? 617

Specification compatibility can be viewed as a more fundamental way to describe specification subsumption in terms of Hoare
logic triples. However, it cannot be directly implemented, since its
naive definition depends on exploring all possible program codes
for compatibility. In this paper, we provide a practical alternative
towards automated verification of OO programs that can support
better precision and avoid unnecessary code re-verification. We use
key principles of separation logic to achieve this.
1.1

Towards Better Precision and Reuse

The focus on specifications that support method overriding has apotential drawback that these specifications are typically imprecise(or weaker) for methods of superclasses. Such specifications typically have stronger preconditions (which restrict their applicability)
and/or weaker postconditions (which lose precision). This drawback can cause imprecision for OO verification which has in turnspurred practical lessons on tips and tricks for specification writers(Kiniry et al. 2005). Furthermore, mechanisms such as specification
inheritance may have unnecessary code re-verification, especiallywhen specification subsumption holds.
Let us consider the specification of a simple up-counter classin Figure 1. This $! class is accompanied by three possible subclasses (i) tu$! to support a faster H#[Zv operation, (ii) w!$!
which works only with positive numbers, (iii) x#y#$! which supports an extra backup counter.
Let us first design the specifications for instance methods ofclass $! without worrying about method overriding. A possible
set of pre/post specifications is given below where #G-H# and are variables denoting the receiver and result of each method.
p#}
zf? 4 q 
; {-15| 1@4
0_7~##5 13546f9 9 ;{-1{@B D13546f9 9 ;{-1j{@C
zf? 4 q .
; {-15| 6 10X4{-1:f7~##5 13546f9 9 ;{-1j {@B D13546f9 9 ;{-1jf
4{-1;{-15|  . 10_7~##513546-9 9 ;{-1j{@B D13546f9 9 ;{-1j{@/ ,-. 6<R{[##uEtu$!e#!F$!Ltu$!_HLlj#G-H# luK LllHZ]H#[Zv-2#G-H# luK L#G-H# luL[##uw!$!e#!F$!RHl]#G-H# lu]ew!$!_HLlj#G-H# luK ellHZR!#_H]HZ¡FF#G!e#G-H# luK e]!]#!2[##ux#y#$!e# !F$!LAHF¢u!v-x#y#$!_HLl H¢#G-H# luK elX#G-H# ¢u!v-K ]¢lHZR!#_H]#G-H# ¢u!v-K e#G-H# luJ#G-H# luK elHZRZy-HZ[ZG-_HeHiHK F#G-H# luJ#G-H# luK e#G-H# ¢u!v-J#G-H# ¢u!v-K H#

Figure 1. Example: ;{-1 and its subclasses

We refer to these as static specifications and precede them with the£¤!¥¤¦ § keyword. They can be very precise as they were considered
statically on a per method basis without concern for method overriding, and can be used whenever the actual type of the receiver is 
known. The notation ¨K K [©l Y   l denotes that variable ¨ is pointUª
ing to an object with the actual type1 of [ -class and where each^field ¨ ¡ is denoted by variable l ^ . For example, in #G-H#K K $!©  ,ªthe field #G-H# lu is denoted by variable  . This format for objects
is used primarily for static specification. To describe an object typewhose type is merely a subtype of the [ -class, we shall use a different notation, namely ¨K K [©l« , which implicitly captures an objectªX¬
extension with extra fields from its subclass.
If we take into account the possible overriding of the H#[Zvmethod by its corresponding method in the tu$! subclass, we
may have to weaken the postcondition of $! H#[Zv . Furthermore,to guarantee the invariant #G-H# lue of the w!$! class, we may
have to strengthen the preconditions of methods $! !# , $! H#[Zvand $! # . These weakenings result in the following dynamic
specifications which are the usual ones being considered for dynamically dispatched methods, where the type of the receiver is asubtype of its current class.
zf? 4 q ;{-15| 1@4 p#} 0_7®­g¯g°gj±²i13546f9 9 ;{-1j {@Z³/g{´iµB D13546f9 9 ;{-1j¶@³/E{@O·L¶·L{@:¸
zf? 4 q ;{-15| 6 . 10X4{-1:f7­g¯g°gj±²i13546f9 9 ;{-1j {@Z³/E5´iµeB D13546f9 9 ;{-12f³
4{-1;{-15|  . 10_7­g¯g°gj±²i13546f9 9 ;{-1j {@Z³/g{´iµeB D13546f9 9 ;{-1{@³/ ,-. 6<R{

Such changes make the specifications of the methods in superclasses less precise, and are carried out to ensure behavioral subtyping. Furthermore, these specifications must also cater to potential
modifications that may occur in the extra fields of the subclasses by
their overriding methods either directly or indirectly. Due to conflicting requirements, we advocate the co-existence of both staticand dynamic specifications. The former is important for precisionand shall be used primarily for code verification, while the latter isneeded to support method overriding and must be used for dynamically dispatched methods. Formally:
1 To make our static specifications more reusable through inherited meth-ods, we shall avoid the use of an explicit constraint, like ¨# #G-H##_[ ,on the actual type of the receiver.

D EFINITION 1.2 (Static Pre/Post). A specification is said to bestatic if it is meant to describe a single method declaration, andneed not be used for subsequent overriding methods.
D EFINITION 1.3 (Dynamic Pre/Post). A specification is said tobe dynamic if it is meant for use by a method declaration and its
subsequent overriding methods.
Past works, such as America (1991); Dhara and Leavens (1996);
Liskov and Wing (1994); Parkinson (2005); Barnett et al. (2004);
Muller (2002), are based primarily on dynamic specifications,though implicit static specifications via ¨# #G-H##_[ can also be
used in ESC/Java and Spec#, while JML uses code contract (Leavens et al. 2007, ch 15) as a form of static specification. However,these proposals for static specifications are somewhat ad-hoc, as
they do not impose any relation between static and dynamic specifications. In our approach, we emphasize static specifications overdynamic specifications. Most importantly, we always ensure thatthe static specification of a method from a given class is always asubtype of the dynamic specification of the same method within thesame class. This principle is important for modular verification, as
we need only verify the code of each method once against its static
specification. It is unnecessary to verify the corresponding dynamic
specification since the latter is a specification supertype. Our proposal uses the following principles for OO verification, achieving
both precision and reuse.
D EFINITION 1.4 (Principles for Enhanced OO Verification).
¹

Static specification is given for each new method declaration,and may be added for inherited methods to support new auxiliary calls and subclasses with new invariants.
¹
Dynamic specification is either given or derived. Whether given
or derived, each dynamic specification must satisfy two subsumption properties. Each must be a :specification supertype of its static counterpart. This helps
keep code re-verification to a minimum.
specification supertype of the dynamic specification of eachoverriding method in its subclasses. This helps ensure behavioral subtyping.
¹
Code verification is only performed for static specifications.
1.2

Our Contributions

The main contributions of our paper are highlighted below:¹

Enhanced Specification Subsumption : We improve on a classical specification subsumption relation. Apart from the usual
checking for contravariance on preconditions and covariance on
postconditions, we allow postcondition checking to be strengthened with the residual heap state from precondition checking.
This enhancement is courtesy of the frame rule from separation
logic which can improve modularity.
¹
Static and Dynamic Specifications : We advocate the coexistence of static and dynamic specifications, with an emphasis on
the former. We impose an important subsumption relation between them. This principle allows for improved precision, while
keeping code re-verifications to a minimum.
¹
Lossless Casting : We use a new object format that allows lossless casting to be performed. This format supports both partial
views and full views for objects of classes that are suitable forstatic and dynamic specifications, respectively.
¹
Statically-Inherited Methods : New specifications may be
given for inherited methods but must typically be re-verified.
To avoid the need for re-verification, we propose for specification subsumption to be checked between each new static specification of the inherited method in a subclass against the static

specification of the original method in the superclass. We identify a special category of statically-inherited methods that cansafely avoid code re-verification for static specifications.
¹
Deriving Specifications : We propose techniques to derive
dynamic specifications from static specifications, and show how
refinement can be carried out to ensure behavioral subtyping.
¹
Prototype System and Correctness Proof : We have implemented a prototype system to validate our proposal, and formulated a set of lemmas on its correctness.
The next section provides more details of our approach in supporting objects for class inheritance, and methods via an enhanced
specification subsumption relation.

2. Our Approach
Our approach to enhancing OO verification is based on separation
logic. We shall describe how we adapt separation logic for reasoning about objects from a class hierarchy and how to write precise
specifications that avoid unnecessary code re-verification.
2.1

Separation Logic and Aliasing

Separation logic (Reynolds 2002; Isthiaq and O’Hearn 2001) extends Hoare logic to support reasoning about shared mutable data
structures. It adds two more connectives to classical logic: separating conjunction  , and separating implication ºº! . »  »  assertsthat two heaps described by »  and »  are domain-disjoint. »  ºº!#» asserts that if the current heap is extended with a disjoint heap described by »  , then »  holds in the extended heap. In this paper we
use only separating conjunction.
Existing formalisms from separation logic literature (e.g. Isthiaq
and O’Hearn (2001); Reynolds (2002); Parkinson and Bierman(2005)) capture heap constraints (with an initial reference from) using two different notations, namely : i) ½¼¿¾ Z À to denotea pointer to a single data object represented by [. . . ], and ii)
#    for a pointer to a set of linked objects in accordance
to a predicate named # . In order to express both notations in a
uniform manner, we introduce the notation -K K [©X  where [ is eitherªa data object or a heap predicate.
Aliasing can be locally specified and captured in separation
logic. For instance, the formula K K w!$!f©u !¨K K w!$!-© ¢ speciªªfies two distinct w!$! objects referenced respectively by  and¨ that are non-aliased. In contrast, the formula K K w!$!f©u Tj]¨ªspecifies a single w!$! object referenced by both  and its local
alias ¨ . There may be other aliases to an object of the heap formula
but the ability to perform local reasoning in separation logic allows us to ignore them. The following static method’s specification
captures both scenarios using multiple specifications of the form
Q U ^_W>Y  ^  ( ^  below:p#}
zf? 4 q 
6 4!Á@Â@40Ã ? 6;{-1:5ÄgÃ ? 6;{-1:Åf7?
59 9 Ã 6;{-1j_ÆZBÅ59 9 Ã ? 6;{-1¶@5B D
59 9 Ã ? 6;{-1j_ÆCBÅ59 9 Ã ? 6;{-1j¶@CÇ? 6;{-1j_Æ/f< ÅLB D59 9 Ã ? 6;{-1_Æ:¸
5

9
9
Ã

p#}
p#}
5| 1@40_7ÈÅ5| 1@4
0_7

Note the effect of the method (specified in the post-conditions) canbe very different depending on whether  and ¨ are aliased, or not.
We support a heap predicate mechanism that can be userspecified to capture a group of related objects. As an example,
we may use an  predicate (or view) to capture a linear linked-listof  nodes, as follows:,f?? 19 9 ÉÉ@2{@ÊË0 ,f?? 1@<i{Ì@ÉÉ-/g{@<µ-7>ÍÎ0_Ï4-Ä_ÁÄÐ r,f?? 19 9 { ?q-. X4-ÄZÐfZBÐ59 9 ÉÉ@ Á/E{@<LÁC7O°Ñs{´iµpÉÆ-66L{ ?q-. 4{-1 z ÆÉfÈg{ ?q-. { . 15Èe| | Á . 13 ?q 6-| |For convenience, we name the first parameter of each predicate
with a default name, called ! , that may be omitted in the LHS.
Each predicate may also have other parameters, such as pointers,
integers or even bags and lists. These parameters correspond tomodel fields of some specification languages (Barnett et al. 2004;
Muller 2002). Existential quantifiers may also be omitted without
ambiguity. These simplifications result in the following more concise predicate definition:
ÉÉ@{@ÊË0 ,f?? 1@<i{Ì@ÉÉ-/g{@<µ-7Í,f?? 19 9 { ?q-. X4-ÄÐ@ZBÐ59 9 ÉÉ@{ÒÓO°ÑÔ{´iµFor simplicity, we shall also restrict our constraint domain to
support essential features such as pointers, class subtyping andintegers. The above definition captures an equivalence between a
predicate and a heap formula in separation logic. Whenever thepredicate holds, we can replace it by its heap formula. Similarly,
whenever the formula holds, we can replace it by its corresponding
predicate. The first technique is known as unfolding (or unrolling),
while the second technique is known as folding (or rolling). These
reasonings are sound and can be automated, as shown in Nguyen
et al. (2007).
An important facet of separation logic is the frame rule:
Ö
Ö×

Õ

Õ Ö
B

 Ö 
. 
. Ö  B Ö×modifies 0 . 7>Ø vars 0Ö×

D EFINITION 2.1 (Entailment
with Frame Capability). The entail×
ment ÚÛÜ@Ú:ÝCÚchecks that heap nodes in the antecedent Ú:Û
are sufficiently precise to cover all nodes
× from the consequent ÚÓÝ ,and can return a residual heap state Ú(from ÚÛ ) that is not used.
For example if we have Ú:Û&K K ©  T-ÞFß and Ú:ÝMK K !© ¨ ,ªªthe entailment process would succeed (via unfolding ©  in Ú:Ûª
to match × with the object ! in Ú:Ý ) and also return residual (orframe) Úm¨K K © -ºRc T-Þ]ß . That is:

2.2

Û

  
¨K K x#y#$!©2 l ¢ªÊà59 9 ÉÉ@{@/g{á â?q-.
Ö 59 9 { Ö×  ÄÐfZBÐ59 9 ÉÉ@{ÒÓJ/E{á â
ÕÊà
Ý
B
Ö×
Õ
?q-.
Õ 0259 9 { ?q-.  ÄÅ@J7gB
0259 9 { ÄÅ@J7gB 02Å59 9 ÉÉ@{ÒÓ/g{á â7

Object View and Lossless Casting

For separation logic to work with OO programs, one key problem
that we must address is a suitable format to capture the objects ofclasses. We should preferably also address the problem of performing upcast/downcast operations statically in accordance with the
OO class hierarchy, and without loss of information where possible.
Consider two variables,  and ¨ , which point to objects from$! class (with a single field) and x#y#$! class (with two fields), respectively. Intuitively, we may represent the first object by K K $!©l ªwhere l denotes its field, and the second object by ¨K K x#y#$!©2l ¢ª
where l ¢ denote its two fields. However, a fundamental problem
that we must solve is how to cast the object of one class to that ofªTj]x#y#$!TFãThe above formula indicates that the actual type of the object is]x#y#$! and that there is no need for any record extension sinceFã . With this object format, we can now perform an upcast to
its parent $! class by transforming it to: _ä ä 
¨K K $!© l
 K K å©x#y#$! ¢Tj]x#y#$!TFãªªThough this cast operation is viewing the object as a memberof $! class, it is still a x#y#$! object as the type information
]x#y#$! indicates. Furthermore, we have created an extensionä that can capture the extra ¢ field ofrecord K K å©x#y#$! ¢ªthe x#y#$! subclass. For simplicity, we currently use an implicitäpointer to capture the extension record. This model allows asequence of upcast operations to be easily captured. Such an upcast
operation is lossless as we have sufficient information to performthe inverse downcast operation back to the original x#y#$! format.
To allow lossless casting between $! and x#y#$! , we add anequivalence rule :  x#y#$!©æ l ¢7<sÙThe side-condition
says that the program  does not modify the×variables in Ú . The frame rule captures the essence of “local
reasoning”: to understand how a piece of code works it should
only be necessary to reason about the memory it actually accesses.
Ordinarily, aliasing precludes such a possibility but the separation
enforced by the  connective allows local reasoning to be capturedby the above rule. Through this frame rule, a specification of theheap being used by  can be arbitrarily extended as long as freevariables of the extended part are not modified by  .
To automate the reasoning process, we have formalised in
Nguyen et al. (2007) a procedure for entailment with frame inference capability :Ö

its superclass, and vice-versa when needed. To do this without lossof information, we provide two extra information : (i) a variable tocapture the actual type of a given object and (ii) a variable to capture the object’s record extension that contains extra field(s) of its
subclass. When a x#y#$! object is first created, we may capture its
state using the formula :ªç _ä ä 
!-K K $!© l
 K K å©x#y#$! ¢ªª

An unfold step (which replaces a term that matches the LHS
by RHS) corresponds to an upcast operation, while the fold step
(which replaces a term that matches the RHS by LHS) corresponds
to a downcast operation. Such a rule can be derived from eachsuperclass-subclass pairing. Formally:
D EFINITION 2.2 (Lossless Casting). Given a class [©l « withª
fields l « and its immediate subclass ©l « y « where y « denotesª
its extra fields, we shall generate the following casting rule that is
coercible in either direction:p,f?? 19 9 q æ15Ä z « ÄJè « Ä + )Ê

,f?? 19 9 215Ä z « ÄZÐfZBÐ59 9 é-1 q Äè « Ä + Note that for any object view © ZZ it is always the case thatªthe subtype relation ILK  holds as its invariant. Furthermore, thedefault ! parameter on the LHS may be omitted for brevity.

Lossless casting is important for establishing the subsumption
relation between each static specification and its dynamic counterpart, as the extension record can be preserved, if needed, by eachstatic specification. Lossless casting is also important for the static
specification of inherited methods which should preferably be inherited without the need for re-verification. This can be achievedby exploiting local reasoning which allows us to assert that an extension record need not be modified by each inherited method.
There are also occasions when we are required to pass thefull object with all its (extended) fields. This occurs for dynamic
specifications where subsequent overriding method may change theextra fields of its subclass. To cater to this scenario, we introduce anåê©2 Y ë view that can capture all the extension records fromªa class  Y for an object with actual type ë . This scenario occurs forthe dynamic specification of $! !# method, as shown below:
13546-9 9 ;{-1æ15Ä Ä + B + 9 9 é-1ìfÉÉ@_;{-15ÄZ1f/E5´iµ
B Dn13546-9 9 ;{-1215Ä5Ä + ZB + 9 9 é-1ìfÉÉ@_;{-15ÄZ1f

Such a dynamic specification may be used with any subtype
of $! . The entire object view must be passed to support dynamic
specifications which are expected to cater to the current method andall subsequent overriding methods. The åê predicate itself canbe defined as follows:é-1ìfÉÉ@_1 Y Ä1ë!FÊí1 Y < 1ë!/ ,f?? 1@<i{Ì@ÉÉiÍ ,f?? 19 9 é-121îÄ z « ÄZÐfBÐ59 9 é-1ìfÉÉ@æ1îÄ1ë!/E1î8R1 Y /1ë#8:9 1îg°Ñ&1ë8:9 1 Y

The notation îI Y denotes a class î and its immediate superclass  Y . The åê predicate is used to generate all the ex-tension records from class  Y to ë . For example, expressionK K åê©_$! $!
yields Fã , and K K åê©æ$! x#y#$!
ª  ªyields K K å©x#y#$! ¢ ã .
ª
Our format allows two kinds of object views to be supported:
D EFINITION 2.3 (Full and Partial Views). We refer to the use of formula K K [© l«
-K K åê©X[  as providing a full view forªªan object with actual type  that is being treated as a [ -class object, 
provides only a partial view with no extension
while K K [© l«ªrecord. For brevity, full views are also written as K K [©l« , whileª_¬partial views are coded using K K [©l« .
ªThis distinction between partial and full views (for objects) follows directly from our decision to distinguish static from dynamic
specifications. Partial views are typically used for the receiver object of static specifications, while full views are used by dynamic
specifications. Some readers may contend that lossless casting ofan object  from ©l« y« to [©l« may also be captured with theªªhelp of separating implication by representing the extension recordusing K K [©l « ºº!jK K © l « y « . This approach works well for partialªªviews, but cannot easily handle the åê predicate required byfull views. Moreover, by omitting separating implication, our current approach to automated verification is easier to build and prove.
2.3

Ensuring Class Invariants

Ensuring that class invariants hold can be rather intricate, withthe key problems being how and when to check for the invariants.
Based on the simplest assumption, one would expect object invariants to hold at all times. However, this assumption is impracticalfor mutable objects. One sensible solution is to expect invariants
to hold based on visible state semantics, which is typically aligned
to the boundaries of public methods. Even this approach may not
be flexible enough. Thus, in Boogie (Barnet et al. 2004; Leino
and Müller 2004), programmers are also allowed to use a specification field, called luHZ , that can indicate if the invariant foran object is being preserved or temporarily broken for mutation.
Similarly, in (Middelkoop et al. 2006), programmers are allowed
to indicate invariants that are inconsistent (not preserved) at somemethod boundary.
We aim for a similar level of flexibility but which still remains easy to use. To achieve this, we introduce the concept of aninvariant-enhanced view for each class with a non-trivial invariant,as follows:
D EFINITION 2.4 (Invariant-Enhanced View). Consider a class[ with a non-trivial invariant ïZðRZñ]#ã over the fields l « of theobject. We shall define a new view of the form [#òFó©l « to captureªits class invariant, as : [#òFó©l «!-K K [©l « #ïZð . Furthermore,ªeçª
for each subclass © l « y « with an extra invariant ïô over theªfields l « y « , we expect its invariant to be ïð#ïô and shall provide a
corresponding view : òFó©l « y «!-K K ©l « y « ïZð#ïô .
ªçª

The use of separating conjunction to capture the class invariant
allows a form of object ownership to be specified for heap objects
present in ïZð . Furthermore, invariant-enhanced view can easily andexplicitly indicate when an invariant can be enforced and when it
can be assumed. If a [©l « is being used, the class invariant is neiªther enforced nor assumed. If a [#òFó©l « is used in the precondiªtion, its invariant must be enforced at each of its call sites, but canbe assumed to hold at the beginning of its method declaration. If a[#òFó©l« is used in the postcondition, its invariant must be enforcedªat the end of its method declaration, but can be assumed to hold at
the post-state of each of its call sites.
With the help of invariant-enhanced views, we can provide
pre/post specifications that guarantee class invariants are always
maintained by public methods. This can help ensure that all objects

created and manipulated by public methods are guaranteed to satisfy their class invariants. Alternatively, it is also possible to allow
some methods (typically private ones) to receive or produce objects
without the invariant property. This corresponds to situations where
the class invariant is temporarily broken. Our invariant-enhanced
views can achieve this as they can be selectively and automaticallyenforced in pre/post annotations.
For example, the invariant-enhanced view of w!$! is:Ã ? 6;{-1fòFõf215Ä z Ä + >Ê

,f?? 19 9 Ã ? 6;{-1æ15Ä z Ä + ZB z ´iµ

Two methods # and H#[Zv are being inherited from the $! superclass, while a third method !# is re-defined to ensure the class invariant. We may provide new static specifications for these three respective methods, to incorporate the invariant-enhanced view. Figure 2 shows how this is done for our running example. It is sufficient to use a weaker precondition of the form #G-H#K K w!$!©æl
ªfor static-spec w!$! !# without compromising its postcondition
#G-H#K K w!$!òeó©  . This corresponds to a temporary violation ofªthe class invariant of w!$! .
2.4

Enhanced Specification Subsumption

With our use of more precise static specifications, we can now
leverage on a better specification subsumption that can exploit the
local reasoning capability of separation logic. In particular, theextended fields of objects that are not used should be preserved by
specification subsumption. More formally, we define the enhanced
form of specification subsumption, as follows:
D EFINITION 2.5 (Enhanced Spec. Subsumption). A pre/post annotation # s is said to be a subtype of another pre/post
annotation #ê íê if the following relation holds:+-,-. ì Õ +-,-.ö B÷+@? 61 ö B÷ Õ +@? 61ì
0 +-,-.ö B D +@? 61 ö 78:90 +-,-. ìRB D +@? 61ìf7Note that ø captures the residual heap state from the contravariancecheck on preconditions that is carried forward to assist in thecovariance check on postconditions.
As an example of its utility, consider the following specification
subsumption that is expected to hold for enhanced OO verification.
static-spec 0æ;{-15| 6 . 1@78:9 dynamic-spec 0æ;{-15| 6 . 157
For the above to hold, we must prove:13546-9 9 ;{-1æ15Ä z Ä + 5B D13546f9 9 ;{-1215ÄZ5Ä + 
8:913546f9 9 ;{-1215Ä z ÄÐfZBÐ59 9 é-1ìfÉÉ@_;{-15ÄZ1@J/5´iµeB D
13546f9 9 ;{-1æ15Ä5ÄÐ@BÐ59 9 é-1ìfÉÉ@_;{-15ÄZ1f

The above subtyping cannot be proven with the basic specification subsumption relation from Sec 1 (without the use of a residual
heap state), but succeeds with our enhanced subsumption relation.
We first show the contravariance of the preconditions:13546f9 9 ;Õ {-1æ15Ä z ÄZÐfZBÐ59 9 é-1ìfÉÉ@_;{-15ÄZ1f/E5´iµ13546f9 9 ;{-1215Ä z Ä + ZB÷This succeeds with ø -K K åê©æ$!  TjF . We then proveçªcovariance on the postconditions using:13546f9 9 ;{-1215ÄZ5Ä + ZB÷Õ

13546f9 9 ;{-1æ15Ä5ÄÐ@BÐ59 9 é-1ìfÉÉ@_;{-15ÄZ1f

This is proven with the help of residual heap state ø (with anextension record) from the entailment of preconditions.
Our preservation of residual heap state is inspired by the needsof static specification. By the use of a new object format (with lossless casting) and a novel specification subsumption mechanism,
we can now support a modular verification process in which reverification is always avoided for dynamic specifications. Our enhanced specification subsumption can also be viewed as a practical

[##u$!R]HFlu$!_Hel £¤!¥¤¦ § #ãE ÔK K $!©lª
#G-H# luK Ll

£
!
¤

¥

¤
¦
§
lHZù]újû H#[Zv-2
#G-H#K K $!©2l  s#G-H#K K $!©2lic ¥@üý¦ § #G-H#K K $!©2l TlFª g s#G-H#K K $!©y ª Tlicþy-þle
ª_¬ª_¬
#G-H# luK L#G-H# lu cH]ùúj#û 2 £¤!¥¤¦ § #G-H#K K $!©l  Ô#G-H#K K $!©l Tj]l¥@üý¦ § #G-H#K K $!©2l Tª lFg s#G-H#K K $!ª ©2lª_¬ª_¬
#G-H# lulHZùRúj!û #_He £¤!¥¤¦ § #G-H#K K $!©l  Ô#G-H#K K $!© ªª¥@üý¦ § #G-H#K K $!©2l TFg s
#G-H#K K $!©2
ª_¬ª_¬
#G-H# luK L[##uw!$!e#!F$!
HlF#G-H# lu]ew!$!_Hel £¤!¥¤¦ § lFg sK K w!$!òeó©lª
#G-H# luK el

£
!
¤

¥

¤
¦
§
lHZù]újû H#[Zv-2
#G-H#K K w!$!ò]ó©l  Ô#G-H#K K w!$!ò]ó©licªª¥@üý¦ § #G-H#K K w!$!ò]ó©l s#G-H#K K w!$!òeó© l c
ªX¬
ª_¬

£
!
¤

¥

¤
¦
§
HF#2
#G-H#K K w!$!òeó©l  s#G-H#K K w!$!òeó©l Tj]lªªlHZùRúj!û #_H] £¤!¥¤¦ § #G-H#K K w!$!©2l TjFg s#G-H#K K w!$!ò]ó©ªª¥@üý¦ § #G-H#K K w!$!©2l TjFg s
#G-H#K K w!$!ò]ó©
ªX¬ªX¬
HZ¡F]#G!e#G-H# luK e]!]#!2[##uEtu$!L#!$!Rtu$!_HLl £¤!¥¤¦ § #ãE ÔK K tu$!©2lª
#G-H# luK Ll

£
!
¤

¥

¤
¦
§
lHZ]H#[Zv-2
#G-H#K K tu$!©æl  ª
#G-H#K K tu$!©æle #G-H# luK e#G-H# luRª[##ux#y#$!e# !F$!L]H¢u!v-
x#y#$!_Hel H¢ £¤!¥¤¦ § #ãE ÔK K x#y#$!©2l ¢ª
#G-H# luK elX#G-H# ¢u!v-K ]¢lHZR!#_H] £¤!¥¤¦ § #G-H#K K x#y#$!©2l s#G-H#K K x#y#$!©2 lªª
#G-H# ¢u!v-K e#G-H# luJ#G-H# luK e



£
!
¤

¥

¤
¦
§
lHZRZy-HZ[ZG-_He
#G-H#K K x#y#$!©2l ¢  s#G-H#K K x#y#$!©¢ lªª
HiHK F#G-H# luJ#G-H# luK e#G-H# ¢u!v-J#G-H# ¢u!v-K  H

Figure 2. Static and Dynamic Specifications given for ;{-1 and its Subclasses
algorithm for implementing Parkinson’s specification compatibility (Parkinson 2005). This link shall be formally proven later inLemma 6.1.

3. Conformance to the OO Paradigm
We present mechanisms to ensure that method overriding andmethod inheritance are supported in accordance with the requirements of the OO paradigm.
3.1

Behavioral Subtyping with Dynamic Specifications

Dynamic specifications are meant for the methods of a given classand its subclasses. They must conform to the behavioral subtyping
principle to support method overriding (and inheritance), as definedby the requirement below:
D EFINITION 3.1 (Behavioral Subtyping Requirement). Givena dynamic specification $E í$ in a method  in class$ and another dynamic specification !ÿ í#ÿ of the corresponding method  in a subclass ÿ . We say that the two specifications adhere to the behavioral subtyping requirement using
!ÿ í#ÿ>ILK  $E í$ , if the following subsumption
holds : !ÿ í#ÿ ILK $T type #G-H##JILK ÿ í$ .
As shown above, we can use the enhanced specification subsumption relation to check for behavioral subtyping. For an example, consider the dynamic specification of method $! !# and its
overriding method w!$! !# . Assuming that these dynamic specifications are given, the behavioral subtyping requirement can bechecked using:
dynamic-spec 0Ã ? 6;{-15| 6 . 178:9 % k dynamic-spec 0æ;{-15| 6 . 1@7
U

Hence, we have:13546-9 9 Ã ? 6;{-1 ³/5´iµeB D
13546f9 9 Ã ? 6;{-1fòFõf2f³
8:9
13546-9 9 ;{-1 z ³/E5´iµ-/L0 type 021354678:9 Ã ? 6;{-1f7jB D13546f9 9 ;{-1æf³

By contravariance of preconditions, we successfully prove:13546f9 9 ;{-1 z ³/E5´iµ-/L0 type 021354678:9 Ã ? 6;{-1f713546f9 9 Ã ? 6;{-1 ³/5´iµ B]÷

Õ

where ø is derived to be F . By covariance of postconditions, we
can prove:Õ13546f9 9 Ã ? 6;{-1fòFõfæf³B÷
13546f9 9 ;{-12f³

Hence, the above two dynamic specifications of $! !# andw!$! !# conform to the behavioral subtyping requirement.

Dynamic specifications may also be given (or derived) for inherited methods, especially when their static specifications havebeen modified. As with method overriding, we continue to expectthat the behavioral subtyping requirement holds between a dynamic
specification (as supertype) for a method in a class and anotherdynamic specification (as subtype) for the same inherited methodin the subclass. Let us consider $! H#[Zv and its inherited methodw!$! H#[Zv . Though no method overriding is present, we must still
ensure dynamic-spec w!$! H#[ZvEILK% k dynamic-spec $! H#[Zv .
U

3.2

Statically-Inherited Methods

Under the OO paradigm, it is possible for a method  in a class $ to
be inherited into its subclass ÿ without any overriding. Furthermore,
the user is free to add a new static/dynamic specification to such aninherited method for each subclass. Such a scenario may occur fora subclass with a strengthened invariant. For each inherited methodof this subclass, we anticipate a new static specification possiblyusing its invariant-enhanced view. An important question to ask is
if there is a need to re-verify this new static specification against
the body of the inherited method.
We shall first consider static specification where the receiver is 
specified using partial view of form #G-H#K K [© l «. For this catªegory of static specifications, we are expecting that each method
invocation by #G-H# -_   does not modify any fields in the extension record and is the same as that in the original method prior
to method inheritance. To support the inheritance of static specifications which use partial views for their receivers, without reverification, we identify a category of inherited methods that is semantically equivalent (modulo the receiver) to the original methodin the superclass.
D EFINITION 3.2 (Statically-Inherited Methods). Given a method with body  from class ê that is being inherited into a subclass , we say that this method is statically-inherited, if the following

conditions hold:¹¹

it has not been overridden in the  subclass.
for all auxiliary calls #G-H# _   for which ñ  , it must be
the case that   is statically-inherited from ê  .

We can show that each statically-inherited method is semantically equivalent to the original method from its superclass. The
above conditions ensure this by checking that the inherited method
always invokes the same sequence of semantically equivalentmethod calls, as that when executed with a receiver object fromits superclass. With this classification for statically-inherited methods, we can check inherited static specifications, as follows:

Let us initially assume that none of the dynamic specifications
are given for our running example. We first present a simple technique for deriving a dynamic specification from its static counterpart, as follows:

D EFINITION 3.3 (Checking Inherited Static Specifications).
Consider a method  with static specification Zê (using a partial view for its receiver) from class ê that is being inherited into
a subclass  with static specification Z . If this method has beenstatically-inherited into subclass  , we only need to check for specification subsumption ZêILK Z . Otherwise, we have to re-verify themethod body of  with the new static specification Z .

D EFINITION 4.1 (From Static to Dynamic Specification). Givena static specification Z[ for class $ , we shall derive its dynamic
counterpart Z[Zÿ , as follows:

As an example, w!$! H#[Zv is statically-inherited from $! H#[Zv(with a partial view #G-H#K K $!©l ), and we can conclude that bothªmethods are semantically equivalent modulo the receiver. To avoid
the re-verification of the static specification of w!$! H#[Zv , weonly need to check for the following subtyping:Some examples of dynamic specifications that can be automatically derived from their static counterparts are:

p#}

p#}
78:9 static-spec 0Ã ? 6;{-15| 1@47Some other methods, such as w!$! # tu$! # tu$! !#
x#y#$! H#[Zv and x#y#$! # , are also statically-inherited. For astatic-spec 0æ;{-15| 1@4

counterexample that is not statically-inherited, consider:ppÉÆ-66mì
 ??
4{-1
4{-1² ??



 ,-.
,
?? 0_7E
 ,-. 1Ì , { 13546-| 
1Ì {seÉÆ-66 ö .  1 . { q 6Îì
,-. 1Ì , {4{-1² ??

¸i

The ¡ method cannot be statically-inherited in subclass  , since
it invokes an auxiliary  method that is not statically-inherited(in this case overridden). In other words, method  ¡2 is not
semantically equivalent (modulo the receiver) to ê ¡2 since they
invoke different sequences of method calls when given the same
parameters except for the receiver. As a result, we expect that thestatic specification (with partial view) for  ¡ must be re-verified
against its inherited method body from ê ¡ .
We have two solutions for handling methods that are notstatically-inherited. One solution is to transform each methodthat is not statically-inherited into an overriding method. This isachieved by cloning the method declaration for each such method
in its subclass. By doing so, we force code re-verification to be
performed for the cloned methods, when inheriting static specifications into such non statically-inherited methods. A second solution
is to utilize full views on the receivers of static specifications. By
using full views on receivers, we shall be handling each method
invocation of the form #G-H# _    by using its corresponding
dynamic specification. As a consequence, each such static specification (with full views on receiver) can always be inherited into any
subclass without the need for re-verification, regardless of whether
the method is statically-inherited or not. However, some loss inprecision may occur since dynamic specifications are now used byeach receiver during the verification of its method’s body.

4. Deriving Specifications
While a static specification can give better precision, having tomaintain both static and dynamic specifications may seem likemore human effort is required by our approach to OO verification.
To alleviate this, we provide the following set of derivation techniques that can be used, where needed.
¹

derive dynamic specifications from static counterparts.
¹¹

refine dynamic specifications to meet behavioral subtyping.
inherit static specifications from method of superclass.

6 +f.

p

p

f%Î6 +f.
where
f%à< 13546@9 9 ;5 z « D 13546f9 9 ;5 z « ³-Ä
13546f9 9 ;-òõf z « D 13546f9 9 ;-òõf z « ³ <

dynamic-spec 0æ;{-15|  . 1f7]<f% k static-spec 0æ;{-15|  . 1f7

Uz,-. 6< z<í13546f9 9 ;{-1 z ³Fp#B D
} 13546f9 9 ;{-1 ³L/
p#}
dynamic-spec 0æ;{-15| 1@47]
< f% k static-spec 0æ;{-15| 1@4
7U<í13546f9 9 ;{-1 z ³FB D13546f9 9 ;{-1 z O³
dynamic-spec 0Ã ? 6;{-15|  . 1f7e
< % k static-spec 0Ã ? 6;{-15|  . 1f7
U<í13546f9 9 Ã ? 6;{-1fòFõf z p#³F} B D13546f9 9 Ã ? 6;{-1fòFõf z ³R/ ,-. 6< zdynamic-spec 0 fÆ-61-;{-15| 1@4
7p#}<  k_% k static-spec 0 fÆ-61-;{-15| 1@4

7Uz<í13546f9 9 fÆ-61-;{-1 ³FB D13546f9 9 fÆ-61-;{-1 z :¸-J³This technique can help us derive dynamic specifications thatare almost identical to static specifications, and are especially relevant for methods (e.g. in final classes) where overriding is not possible. However, these automatically derived dynamic specifications
may fail to meet the behavioral subtyping requirement. Failure of
behavioral subtyping can be due to two possible reasons:
1. Dynamic specification of method in superclass is too strong, or
2. Dynamic specification of method in subclass is too weak.
We propose two refinement techniques for related pairs of dynamic specifications to help them conform to behavioral subtyping.
A conventional way is to use specification inheritance (or specialization) to strengthen the dynamic specification of the overriding
method. However, in our approach, this technique of strengthening
the dynamic specifications of a method in the subclass may violate
a key requirement that the dynamic specification be a supertype of
its static counterpart. Thus, prior to using specification specialization, we must either check that each inherited dynamic specification
is indeed a supertype of the static specification from the overriding
method, or can be made to inherit the static specification from theoverridden method, as follows :D EFINITION 4.2 (Specification Specialization). Given a dynamic
specification !ÿ > '#ÿ  and its static specification    for a method  in class ê , and its overriding method in a
subclass  with static specification  !! ! . A dynamic
specification !ÿ T type #G-H##LILK-En#ÿ  can be added tothe overriding method of the  subclass if either of the following
occurs:¹ ! '!]ILK >!ÿ > '#ÿ  holds, or!   > '  can be inherited into the static specification of  in class  and successfully verified.

Note that  ! e ¾ #G-H#K K ê©l « ¼®#G-H#K K ©l « y « #G-H#K K êòFó©l «ªªª¼®#G-H#K K © l« y« #ï ZÀ where y« are free variables of the extendedªrecord, while ï  captures the invariant of ê class. The refined¹

dynamic specification for the overriding method is obtained via
intersection type, !ÿ í#ÿ Q
!ÿ T type #G-H## ILK
E s#ÿ  .
As an example, the pair of dynamic specifications for $! #
and w!$! # do not conform to behavioral subtyping. Wemay therefore attempt to strengthen the dynamic specification ofw!$! # by specification specialization through the following
multi-specification:

0 +-,-. Y B D +@? 61 Y 7
0 +-,-. ë>B D +@? 61ë#7<>=
0 +-,-. Y / +-,-. ë!7iB D 0 +@? 61 Y Í +@? 61ë#7Ç
13546-9 9 Ã ? 6;{-1fòFõf z ³]B D13546-9 9 Ã ? 6;{-1fòFõf z Z³L/ ,-. 6< z?
zz
13546-9 9 ;{-1 ³/ type 021354678:9 Ã 6;{-1iB D13546-9 9 ;{-1 ³/ ,-. 6< z

For brevity, we shall omit the formal details of how normalization (of separation logic formulae) is carried out for the abovetranslation. In the case of $! H#[Zv , we can perform normalization
to obtain the following weakened dynamic specification:

However, the inherited dynamic specification from $! # is
not a supertype of static-spec w!$! # . Hence, in order to proceed with this refinement, we must also inherit the static specification of static-spec $! # into w!$! # , as follows:13546f9 9 Ã ? 6;{-1fòFõf z B D13546f9 9 Ã ? 6;{-1fòFõf z >/ ,-. 6< z13546f9 9 Ã ? 6;{-1 z B D13546f9 9 Ã ? 6;{-1 z g/ ,-. 6< zÇ

This strengthened static specification is now a subtype of thecorrespondingly derived dynamic specification. Furthermore, behavioral subtyping holds between the new dynamic specificationsof $! # and w!$! # . A caveat about specification specialization is that the strengthened static specification of the methodin the subclass may not always guarantee the invariant property.
For example, #G-H#K K w!$!òeó© l  Ô#G-H#K K w!$!òeó© l TÓ#]lªªguarantees that the class invariant of w!$! is preserved, but not
#G-H#K K w!$!©2l BXD
#G-H#K K w!$!©2l TC]l . It is thus possibleªªfor successfully verified calls of this method to violate the class invariant property, but the above multi-specification is fully aware ofwhen each such violation occurs through the use of different predicates. This violation of a class invariant is one reason why Findler
et al. (2001) considered specification inheritance to be a potentially‘unsound’ derivation technique.
As a complement to specification specialization, we propose adual mechanism that weakens the specification of the overridden
method instead. We refer to this new technique as specification
abstraction. Instead of an intersection type, we use a union type toobtain a weaker dynamic specification for the overridden method.
Formally:
D EFINITION 4.3 (Specification Abstraction). Given a dynamic
specification !ÿ  í#ÿ  for a method  in class ê , andits overriding method in a subclass  with dynamic specification
!ÿ>J#ÿ . If behavioral subtyping does not hold between
these dynamic specifications, we can generalise the specification of
the overridden method using the following union type:02ì5| Áf{@7F<Ë0 +-,-.
dynamic-spec"+@? 61 7
 BDE-!#0 +-,-. #7B D
Ï-è « r -!#0 +@? 61 #7-!#L<$ 13546@9 9 ö  z « Äè « ³D 13546f9 9 ì z « ³-Ä
13546f9 9 ö òõf z « ÄJè « J³D 13546-9 9 ìfòõf z « ³B%!&We refer to this process as specification abstraction. It is a safe
operation that weakens the dynamic specification of an overridden
method to the point where behavioral subtyping holds.

"

13546f9 9 ;{-1 z Z³FB D13546f9 9 ;{-12è@³L/½0è@< z CÍEè@< z :¸7

It would appear that the use of specification abstraction loses
modularity, due to its dependence on the dynamic specificationsof overriding methods. However, this is not true. Firstly, the purpose of specification abstraction is to derive dynamic specifications which need not be re-verified. Secondly, we maintain modularity as each static specification is verified once, but need only be
re-verified when the specifications it depends on change. Thoughchanges may occur for a dynamic specification that a method depends on; the necessity for re-verification is analogous to a modular
compilation system which re-compiles a module whenever the typeinterface it depends on changes.
While our approach can theoretically derive all dynamic specifications, we shall also allow the option for users to directly specify
dynamic specifications, where required. This option is especiallyhelpful in supporting modular open-ended classes that could befurther extended with new subclasses. Our overall procedure forselectively but automatically deriving dynamic specifications shallbe as follows:
D EFINITION 4.4 (Deriving Dynamic Specifications). We deriveand refine dynamic specifications, as follows:¹

If the dynamic specifications of both overridden and overriding
methods are given, check for the behavioral subtyping requirement.
¹
If only the dynamic specification of an overridden method
is given, derive the dynamic specification of the overriding
method and then use specification specialization to refine it.
¹
If only the dynamic specification of an overriding method
is given, derive the dynamic specification of the overridden
method and then use specification abstraction to refine it.
¹
Otherwise, derive both dynamic specifications and then use
specification abstraction to refine the dynamic specification of
the overridden method in the superclass.
Note that the procedure is geared towards the preservation ofclass invariants, where possible, as it favours specification abstraction over specification specialization.
Lastly, it may also be possible for static specifications to beomitted for some statically-inherited methods. We propose a way
to derive static specifications for such methods, as follows:
D EFINITION 4.5 (Deriving Static Specifications). Given a method

As an example, consider the derived dynamic specifications
from a pair of methods $! H#[Zv and tu$! H#[Zv where behavioral subtyping does not currently hold. We are unable to apply specification specialization, as the inherited static specification of $! H#[Zv cannot be verified by the overriding method oftu$! H#[Zv . However, with the help of specification abstraction,
we can obtain the following union type for dynamic-spec $! H#[Zv
instead.
13546f9 9 ;{-1 z ³FB D13546f9 9 ;{-1 z CJ³
13546f9 9 ;{-1 z ³FB D13546f9 9 ;{-1 z :¸-J³"

Our current separation logic prover is able to directly handle intersection types but not union types for its multi-specifications. We
propose to handle union type by the following translation instead: from class ê with static specification Zê , and a subclass  where

the same method has been statically-inherited. If no static specification is given for   , we can derive a static specification for it,
as follows :static-spec 0 ö | Áf{@7F<$ 13546f9 9 ì z « D

13546f9 9 ö  z « ÄJè « 6 + ìThe extra fields, y « , in the subclass are never modified by eachstatically-inherited method.
The above substitution is only applicable for partial views, and
it is not needed for full views which will remain unchanged when
deriving static specifications.
Though specification derivation techniques are important aidsthat make it easier for users to adopt our OO verification methodology, they are not fundamental in the current work. In the rest of thisP
KKclasst K K 

tdecl « etdecl K K  classt ' viewt[##u)(  #!)(  Hl+*@T-,C] .0/X« meth « 
11
K K  H2
 'J¢3'ZlHZ
.EK K 4(5'viewt K K ½lH!y c 6© / «Hl9,sp K K  Q½ pr  
po  «ªj8
ç 7
77
meth K K 4. mn _ .:/X«>¾ u#H#[ sp  À@¾ ¨#uZ@H#[ sp  À@¾ ;ZÀ
;K K Îã< '&=>'/>'/- ? '/-K @ ;+'/  ?5K A
 / 'J!@y (# / « B
 '&/-K ('&;  
 ;  '.0/-C
 ;+'&/- mn / « B
 'HZA¡ /]#G!@ ;  !A ; '#6(0 />'JyG-H!#A
 /FyG# sp ) ;KKE DÓ2dF/«h *@G
T ,jX«,)K K I
 H5K
T J5G
T L
7




H
KK4
 / 5
 / '&/Fã< '/ 5 ñ / '/]ñ ã3
 'H  T H *
K K ²Z>'/-K K c 6© / « 'M*  N
 * LËK K O /@ (@'/-ILK ( P Ú  'ª Ú:Ú
KK
'ZÚ M
T ,Q'ZÚ  Ú  'Fd /-h Ú7
JK K Ó#ã> '!¡u!R
 'S  + S  ' S  Aþ S  'T(#)
I / 'TJ  C
T J  P J  ' UCJV'F'TJ d /iMh JV'Z0` /Lh JS
KKW =X'/X'T=CYKS 'TS  # S  'Aº S ' max 6S  S  ) ' min 6S  S  erator, (ii) Inheritance Checker, and (iii) Code Verifier. These are
elaborated next.
5.2.1

Ã ? 6;{-1æ15Ä{Ä + +fÆ-61-;{-1_15ÄJ{Ä ?
Âè ;{-1æ15Ä{ÄJ¶Ä + ,f?? 19 9 ;{-1æ15ÄJ{ÄZÐfZBÐ59 9 é-1% k- + ,f?? 19 9 ;{-1æ15ÄJ{ÄZÐfZBÐ59 9 é-1\ k_U% k- + U
Ê ,f?? 19 9 ;{-1æ15ÄJ{ÄZÐfZBÐ59 9 é-1]^æ% k-¶Ä + 
UCorrespondingly, we may also provide an åê view for the

Figure 3. A Core Object-Oriented Language
paper, we shall assume that all required dynamic and static specifications are available, and proceed to describe core components ofour enhanced OO verification system.

5.1

A Core OO Language

We provide a simple OO language in Figure 3, and assume that
type-checking is done on the program and specified constraints
prior to verification. This core language is the target of some preprocessing steps. A program consists of a list of class and view declarations and an expression which corresponds to the uH method
in many languages. We assume that the super class of each class is
explicitly declared, except for Z¢a[ at the top of the class hierarchy. We also use #G-H# as a special variable referring to the receiverobject, and Zã# to refer to a superclass’s method invocation. For
each view definition, we declare an invariant , over the parameters! /« that is valid for each instance of the view. Also, is a7
normalised form of Ú , H captures pointer constraint, L type information, J arithmetic constraints, while , a pure formula without
any heap. Each method meth and yG-H!# loop is declared with intersection type(s) of the form QÓ pr  po X« . For simplicity, we
7
7
assume that variable names declared in each method are all distinct
and use the pass-by-value parameter mechanism. Primed notation
is used to capture the latest value of local variables and may appear
in the postcondition of loops. For example :yG-H!#FIFyG#F#ãE  ÞFT [] P þ]Tj [2e]EK ]ic
Here  and  [ denote the old and new values of variable  at theentry and exit of the loop, respectively. Note that precondition #ã
captures the loop’s invariant, while postcondition ÞFT [] Pþ]Tj [2] captures the loop’s effects.

5.2

Verification System

Our verification system for OO programs is implemented in a modular fashion. It processes the class declarations in a top-down manner whereby the methods of superclasses are verified before thoseof the subclasses. We shall assume that static specifications are
given, and that dynamic specifications are already given (or automatically derived). Also, for each method that is not staticallyinherited in a subclass, we shall clone the method for that subclass.
There are three major subsystems present, namely: (i) View Gen-ÊÊ

class hierarchy. In the case of our running example, we can generate
the following definition for the åê view:é-1ìfÉÉ@æ1 Y Ä1ë!Ês021 Y < 1ë!7/ ,f?? 1@<i{Ì@ÉÉÍ ,f?? 19 9 é-
1 % k2ÐfZBÐ59 9 é-1ìfÉÉ@æÃ ? 6;{-15ÄZ1ë!
U?
/EÃ 6;{-158i1 Y /1ë#8:9 Ã ? 6;{-1Í ,f?? 19 9 é-\
1  k_% k-2ÐfZBÐ59 9 é-1ìfÉÉ@ fÆ-61-;{-15Ä1ë!
U/ fÆ-61-;{-158i1 Y /E1ë8:9 fÆ-61-;{-1
N
f
,

?
?
Í
19 9 é-1 ]^æ% k¶ÄÐ@BÐ59 9 é-1ìfÉÉ@æÂè ? ;{-15Ä1ëU?
/Âè ;{-158i1 Y /1ë#8:9 Âè ? ;{-1

5. Enhanced OO Verification
We shall now formalise our verification system. We consider asimple sequential language with just the basic features from the OO
paradigm. Some omitted features, such as exceptions, static fields
and static methods, can be handled in an orthogonal manner and do
not cause any difficulty to our verification system.

View Generator

For each subclass in the class hierarchy, we must generate a lossless
upcasting rule in accordance with Defn 2.2. However, the format å©_[ l «actually denotes a family of record extensions thatªis distinct for each subclass [ . To distinguish them clearly in our
implementation, we provide a set of specialised record extensions

of the form åð© l «instead. With this change, we can generateªthe following casting rules for our running example:

Lastly, for each subclass with a non-trivial invariant, we also
generate two invariant-enhanced views for this subclass. For our
running example, only the subclass w!$! has an invariant. Hence,
our generator will provide the following:Ã ? 6;{-1fòFõf215ÄJ{Ä + Ê

,f?? 19 9 Ã ? 6;{-1æ15ÄJ{ÄZÐf/g{´iµIn summary, the above shows how we explicitly generate predicate views for casting and class invariants. In practice, our prototype verification system creates these views on demand duringentailment checking itself.
5.2.2

Inheritance Checker

This subsystem ensures that specifications of added methods are
consistent with class inheritance and method overriding requirements. Whenever a new subclass  is added, we expect a set of new
overriding methods and another set of statically-inherited methods.
We propose to check for consistency, as follows:¹

Firstly, we check that each static specification is a subtype ofthe dynamic specification.
¹
For each new overriding method   , we identify the nearest
overridden method in a superclass of  . We then check that eachgiven dynamic specification is a subtype of the given dynamic
specification of its overridden method in its superclass.
¹
For each statically-inherited method   , we check that its
given static specification is a supertype of the corresponding
static specification in its superclass. If a dynamic specificationis also given, we check that it is a subtype of the given dynamic
specification in its superclass.
Some of the static and dynamic specifications may have been
automatically derived. As these derived specifications are correct
by construction, we shall not be checking for the specification
subsumption relation amongst them.
5.2.3

Code Verifier

To support verification, we shall use Hoare-style rule of the form
Ü!Ú  ;!Ú   . This rule is applied in a forward manner. Given aheap state Ú  and an expression ; , we expect the above verification

to succeed and also produce a poststate Ú  . There are four featuresin our core language that are peculiar to the OO paradigm, namely(i) the object constructors, (ii) the cast constructs, (iii) instancemethod invocations and (iv) Zã# calls. Let us discuss how they
are handled.
For the object constructor, we use the following rule where eachprimed variable l [^ captures the latest value of variable l ^ :
Ö  Ö
p p
<
B ,-. 6f9 9  Ä_ [ Ä#| | Ä&_ `[ ÄJ{Ì@ÉÉ-
Ö 
Õ Ö
p
.
>{ è 0_  Ä| | Ä_ ` 7This rule produces an object of actual type [ using partial view.
Consider a cast construct æ[#J lK [ Y  where lK [ Y captures thecompile-time type of l inserted before verification. We shall treat it
as being equivalent to a primitive call of the form:
pRppÆ-61-ðF0 Y z 7~##5

z 9 9 p Y 215Ä| | ÓB D z 9 9 p Y 215Ä#| | /E158:9 p/®1 , Ì . B D
1 , Ì .

The above declaration allows the cast construct to possibly failat runtime. If casting succeeds, we may expect that the actual
type of the object to be a subtype of [ , as captured by the firstpre/post annotation. The second pre/post annotation is added forcompleteness, and may be used if we are unable to establish theheap state of l .
Another important feature to consider is instance method call of
the form lK [#J - l Y   l  . We first identify the best possible type ofUl using Lj]¡H¨# ø lK [# . The result L will tell us if we have theactual type R[ Y or the best static type ILK [ Y where  type l and[ Y ILK [ . Note that [ Y can be more precise than the compile-time type
[ due to our use of flow- and path-sensitive reasoning. If the actual type is known, we choose the static specification of method from class [ Y . Otherwise, we choose its dynamic specification in 
stead. This decision is captured by Z[#e¡HZ[ w L  wherew denotes the entire OO program. The overall rule is:Ö
4 { q 1Å +fp . 0 a Ä_9 b7<_ [ Ä#| | | Ä&_ ` Dc_ ` [ ÇX$de  _ +-Dc
qf+.
,-. ^ B D +@? 61 ^ 74{ 60Ö ÃÕ Ä ÄXÁf{@7<0WeÖ e ÖXj
Ö e +@?
r 0
Ïf)g4h| | i
06 +-,-. ^ 7B<Ë0B
61 77


Xj
Ö
Õ Ö
e0_9 b7| Áf{0_  | | _ ` 7
a

<





If Ú is a disjunctive formula with different types for l , we
can use ¡H¨# /¡HZ[ operations in the entailment procedure,so that the best specification is selected for either the actual or
the static type of the object at l for each disjunct. For multispecifications, we choose the first specification whose precondition
holds. We assume that these multiple specifications are ordered toyield a more precise result ahead of the less precise ones.
We can easily deal with the invocation of Zã# methods. Thisfeature can be used in place of the receiver #G-H# parameter to referto the overridden method. It can be easily handled by our approachsince Zã# method calls are essentially static calls that can be
precisely captured by static specifications. Consider an overridden
method  in a superclass ê and a call Zã# -_   being usedin an overriding method in subclass  . We can handle this Zã#call by re-writing it to #G-H# ê -_   . In this case, our verification
process will select the static specification of the overridden method
in class ê to use. Past works, such as Parkinson and Bierman(2005); Kiniry et al. (2005), do not handle Zã# method calls forverification well, as there is an inherent mismatch between Zã#
method calls (which are static calls) and the mechanism based on
dynamic specifications.

6. Correctness
There are several soundness results that are needed to show theoverall safety of our verification system.
The semantics of our constraints is that of separation logic(Reynolds 2002), with extensions to handle our shape views. To

define the semantic model we assume sets Loc of locations (positive integer values), Val of primitive values, with klg Val denoting {Ì@ÉÉ , Var of variables (program variables and other metavariables), and ObjVal of object values stored in the heap, with 
(¾ ?  ¼Im    ? ` ¼9m ` À denoting an object value of data type ( where
  `

m
  m are current values (from the domain Val n Loc) of the cor 
responding fields ?    ? ` . This object denotation shall be abbre  `viated as (#6m   m  . Let oÄ&prq <ts denote that stack o and heap
p form a model of the constraint s , with p>ÄMo from the following
concrete domains:
Heaps <#v6w
Stacks <#v6w

pug
oyg

Loc x
Var D

fin ObjVal

Val z Loc

As we use a first-order language, lexical scoping can be easily
enforced by only allowing elements from the topmost stack frame
to be accessible at runtime. A complete definition of the model for
separations constraints can be found in Nguyen et al. (2007).
We use a small-step dynamic semantics for our language (Fig.
3) but extended with pass-by-reference parameters. For simplicity,
we assume that all yG-H!# loops have been transformed to equivalent
tail-recursive methods with the help of pass-by-reference parame 
ters. The machine configuration is represented by ©{ » ; where {ªdenotes the current stack, » denotes the current heap, and ; denotes
the current program code. The semantics assumes unlimited stackand heap spaces. Each reduction step can then be formalized as asmall-step transition of the form: oÄ&p>Ä&|} Dso  Ä&p  Ä&|   . The fullset of transitions is given in Fig. 4. We have introduced an inter
mediate construct # /« ;# , with ; to denote the residual code ofits call, to model the outcome of call invocation. It is also used tohandle local blocks.
The following lemma highlights a key result showing that ouruse of specification subsumption relation is sound for avoiding reverification, as follows:
L EMMA 6.1 (Soundness of Enhanced Spec. Subsumption).
Given that method body  has been successfully verified using # s . If specification subsumption # sFILK
#ê sê holds, then its specification supertype #ê íêis guaranteed to verify successfully against the same method body.
Proof: From the premise of specification subsumption (Defn 2.5),
we can obtain: #ê Ü@#jø and øÜfê . In our context,
preconditions #ê # and their entailment’s residual ø do notcontain any primed variables, while only primed variables are modified indirectly by our program. Hence, adding a formula with only
unprimed variables, such as ø , to both pre/post always satisfies theside condition of the frame rule. Let  denote the method bodywhich has been preprocessed to a form  where pass-by-value parameters are never modified. Let l Y   l  denote the set of freevariables in  , and let ~)Q U ^_W>Y l [^ ]l ^  .U From the premise that# s is a verified specification for the code, we have
Ü Z#TK~jEZ . In order to show that its specification supertype #ê íê is also verifiable for the same code, we needto derive ÜCZ#êTK~jEZê . We conclude based on the following steps:ÜCZ#TK~jEZ
ÜCZ#K
T ~#øjEZø
ÜCZ#êK
T ~jEZø
ÜCZ#êK
T ~jEZê

premiseframe ruleprecondition strengthening
postcondition weakeningThe above proof uses the following Consequence Lemma stating the soundness of precondition strengthening and postcondition
weakening:
L EMMA 6.2 (Consequence Rule). The following verification holds:


[ Ü



Ü 
C

Ü



jETi$RÜ:+[[ [ jEToÄ&p>Ä&_@} DsoÄ&p>ÄMo0_@7oÄ&p>Ä&5} DÔoÄ&p>ÄM5
oÄ&p>Ä&_| j} DÔoÄ&p>ÄMpg0o0_@77!0j7oÄ&p>Ä_9 <25} Dso\ _0DOæÄMp>Ä0_7
T

,
.
,
.
oÄ&p>Ä0_7È&|} DsoÄ&p>Ä&| o&
Ä p>Ä
_N
È |} Ds _0D >oÄ&p>Ä
10_Ä&|7¿oÄ&p>Ä
10_ « Ä&57} DÔoÒ _ « ÄMp>Ä&5, .
o0_@7<i1 Ìo0_@7<ÆÉ-6 .
oÄ&p>Ä&|  } DÔo  Ä&p  Ä&|  


.
.
.
.
.










oÄ&p>ÄM| È&| } DÔo Ä&p Ä&| È&| oÄ&p>Ä!4 _ 13 {R|É-6 | } DsoÄ&p>Ä&| oÄ&p>Ä!4 _13 {>|É-6 . |  } DsoÄ&p>ÄM|   oÄ&p>Ä&|} Dso  ÄMp  ÄM|  oÄ&p>Ä_9 <2|} Dso  ÄMp  Ä&_9 <2|   o&
Ä p>&Ä | } Ds o  Ä&p  Ä&|  ,.
oÄ&p>Ä
10_ « Ä&|7} Dso  Ä&p  Ä ,-. 1j0_ « Ä&|  7eee<pg0o0_  77 GDo0_  7p  <pB o0_  7D o&Ä p>Ä_  | ý9 <_  } DÔoÄ&p  Ä0_7

 <X  Do0_ 7 ` WCd >opg0o0_77<b ||#| eeee,-.    7 ed<W    Ä0   7 e` WGd 7  |Rg meth 0b7
 mn 00ee ed<  e `eoÄ&p>Ä{ . è2b0_  Ä#Ä_ ` 7} DsoÄ&pjX ND
æÄ&XoÄ&p>Ä&_| mn 0 _  Ä#| | &Ä _ ` 7 } DÔ o  &Ä p>Ä ,-. 10 
W dOÄ  _   W  |7
C
e
e `e
e
e
e
e


,-.    7 ed<W    Ä0   7 `e G
W d 7 |Rg meth 0 b7o  < Do0_ 7 WCd >o mn 00eeeed< `eoÄ&p>Ä&_| b| mn 0_  Ä| | Ä_ ` 7 } Ds o  MÄ p>Ä ,-. 1j0 
W dÓÄ  _   W  |7
K

fields 0b7<    Ä#| | Ä ` Fg dom 0pj7<<b   Do0_  7Ä#| | Ä ` DOo0_ ` 7`oFigure 4. Dynamic Semantics


Proof Sketch: Based on the premise, we have a set of { » such thatoÄ&p>Ä . } D « o  Ä&p  Ä_@ and { »' 
TX{   ¾ #¼9/À »  '  Post R .
   ¾ #9
By Galois connection, we Õ have
{
¼

/
À
»
'

Post
+[ . Thus,




[ .
[ .
[ , we havefor all { »' 
We extract the post-state of a heap constraint by:

If we assume a similar object from a subclass  such that
and we call the overriding method, then we obtain :

D EFINITION 6.1 (Poststate). Given a constraint Ú , Post Ú: captures the relation between primed variables of Ú . That is :
Ö

rÖ

where
Post 0  7m<#v6w0_Ï V 7ÄÖV<_  Ä| | Ä_ `denotes all unprimed program variables in<$ _ [ Dc_  Ä#| | Ä&_ `[ DE_ ` The next two lemmas state some results on statically-inherited
methods for which re-verification is proven not to be needed.
L EMMA 6.3 (Equivalence of Statically-Inherited Methods).
Consider a method  from class ê that satisfies the conditions ofbeing statically-inherited into a  subclass. Assuming thatoÄ&p  Ä ? | Áf{j0 + « 7} D « o  Ä&p  Ä_@p  #< pjX o0 ? 7D ì0_  | | _ ` 7
p  #< p [X  o0 ? 7D ì0  | |  ` 7



then



L EMMA 6.5 (Soundness of Behavioral Subtyping). Consider amethod  from class ê with dynamic specification !ÿ> í#ÿ 
and that q < +-,-. 
?
p <#pjX o0 7D ì0_ « 7oÄp  Ä ? | Áf{j0 + « 7J} D « o  Ä&p  Ä_@,-. 6\Dc+@? 61o  
 _\æÄ&p  q < Post 0
oÄ&p

#7

Proof Sketch : Follows from Defn 3.1 of the behavioral subtyping
requirement and Lemma 6.1.
Lastly, we prove the soundness of our verification system usingpreservation and progress lemmas.
L EMMA 6.6 (Preservation). If
Õ Ö

@|

Ö 
oÄ&pIq <Post 0Ö7Then there exists Ú  such that {  »  ' 

Proof Sketch: By induction on ; .

oÄ&p>Ä&|} Dso  Ä&p  Ä&|  Post Ú   and Ü!Ú  N;  !Ú   .
Proof Sketch: By induction on ; .

L EMMA 6.4 (Soundness of Statically-Inherited Specifications).
Consider a method  from class A that has been successfully
verified against its static specification  T> í , and a
subclass B that statically-inherits  with static specification !> í! . Assuming that a specification subsumption relation of the form   íLILK! ! í! holds, then  is guaranteed to verify successfully against its specification !> í! .

7oÄ&p>Ä&|} Dso  ÄMp  Ä&|  |

Proof Sketch : Using the conditions of Defn 3.2, we can prove theabove by an induction on the dynamic semantics (see Fig. 4) over
execution of the body of statically-inherited methods.
Proof Sketch : Follows from Lemmas 6.3 and 6.1.
We shall now show a result regarding behavioral subtyping.

oÄ&p  Ä ? | Áf{j0 + « 7} D « o Ä&p-Ä_@
,-. \
6 c
D _\æÄMp-Rq < Post 0 +@? 61o ]

L EMMA 6.7 (Progress). If ÜC!ÚÓN;F!Ú   and { »'  Post Ú: , then
either ; is a value, or there exist {  »  , and ;  , such thatoÄ&p  Ä ? | Áf{j0 + « 7} D « o  ÄMp-Ä_@p  2< pjX o0 ? 7D ö 0_  | | _ ` Ä_ `\  | | _ d 7
p-2< p [X  o0 ? 7 D ö 0  | |  ` Ä_ `\  | | _ d 7 q < +-,-. 
 <2pjX o0 ? 7D ö 0_ « Ä « 7

oÄ&p
p



T HEOREM 6.8 (Soundness of Verification). Consider a closed
term ; without free variables in which all methods have beensuccessfully verified. Assuming that Ü#ãN;!ÚÓ , then either æÄ  æÄM|} D «  æÄMp>Ä_@ terminates with a value / such that the fol
lowing X¾ ¼/À »@)' ²Ú holds, or it diverges  æÄ æÄM|F}D « .
Proof Sketch: Follows from Lemma 6.6 and Lemma 6.7.



7. Related WorkIn support of modular reasoning on properties of object-oriented
programs, the notion of behavioral subtyping has been intensively studied in the last two decades, e.g. Liskov (1988); America (1991); Liskov and Wing (1994); Dhara and Leavens (1996);
Meyer (1997); Findler et al. (2001); Muller (2002); Parkinson(2005). The notion of specification inheritance, where an overriding method inherits the specifications of all the overridden methods, was first introduced in Eiffel (Meyer 1997). As an effort torelate these two notions, Dhara and Leavens (1996) presented a
modular specification technique which automatically forces behavioral subtyping through specification inheritance. More recently,
Leavens and Naumann (2006) proposed a formal characterization
for behavioral subtyping and modular reasoning. The basic idea ofmodular reasoning, which the authors call supertype abstraction, isthat reasoning about an invocation, say å @2 , is based on the specification associated with the static type of the receiver expression
å . In Leavens and Naumann (2006), the authors proved the equivalence between supertype abstraction and behavioral subtyping. The
new formalization is supposed to serve as a semantic foundationfor object-oriented specification languages.
Various embodiments of these proposals have been implemented in both static and runtime verification tools and been applied to rich specification and programming languages such as
ESC/Java (Flanagan et al. 2002), JML (Leavens et al. 2006), Spec#(Barnett et al. 2004), and ESpec (Ostroff et al. 2006). The Krakatoa
tool (Marché et al. 2004; Marché and Paulin-Mohring 2005) translates JML specifications into the input language for the Why verification tool (Filliâtre 2003). Verification conditions generated by
the Why tool can then be discharged by different theorem provers.
However, to the best of our knowledge, neither inheritance nor
method overriding is supported by their system. Software model
checking frameworks (Robby et al. 2003; Hatcliff et al. 2003) havealso been used in the verification of OO programs. Inference mechanisms for loop invariants have been proposed in Nimmer and Ernst(2002); Pasareanu and Visser (2004) amongst others, and they canmake verification even easier to use. However, most of these works
are based primarily on the idea of dynamic specifications. Even
when static specifications are added, like code contracts in JML(Leavens et al. 2007, ch 15), they did not enforce an important
subtyping relation between a static specification and its dynamic
counterpart. Moreover, in comparison with our approach, Spec#is more restrictive in handling overriding as it does not allow anychanges in the precondition of the overriding method.
Using the rules of behavioral subtyping, Findler et al. have formalized hierarchy violations and blame assignment for pre andpostcondition failures (Findler and Felleisen 2001; Findler et al.
2001). They identified a problem (related to preservation of classinvariants) that arises from synthesizing the specifications of overriding methods through specification inheritance. This problem iscaused by specification inheritance’s manner of enforcing behavioral subtyping which may wrongly assume that the original specification of an overriding method is too weak. In our proposal, we
can avoid this problem by using specification abstraction instead of
specification inheritance, if class invariants are to be preserved forthe overriding methods. Furthermore, while Findler and Felleisen(2001) and Findler et al. (2001) focus on checking the correctnessof contracts at run-time, we propose a static verification system.
The problem of writing specifications for programs that use various forms of modularity where the internal resources of a module
should not be accessed by the module’s clients, is tackled in several
papers (O’Hearn et al. 2004; Parkinson and Bierman 2005; Leavens
and Muller 2007). In O’Hearn et al. (2004) the internal resourcesof a module are hidden from its clients using a so called hypothetical frame rule, whereas in Parkinson and Bierman (2005) thenotion of abstract predicates is introduced. While O’Hearn et al.
(2004) only supports single instances of the hidden data structure,
abstract predicates can deal with dynamic instantiation of a module. To support the reasoning of concurrent programs, a rule similar
to the hypothetical frame rule is used in O’Hearn (2007) to model
critical regions with resource invariants. For soundness reason, precise resource invariants were also required in O’Hearn et al. (2004)
and O’Hearn (2007) due to the desire to support both the conjunction rule and the hypothetical frame rule. As both rules are not usedin our current system, we do not suffer from this problem and cansafely support less precise heap states and multiple specifications.
Visibility modifiers are taken into consideration in Leavens andMuller (2007) where a set of rules for information hiding in specifications for Java-like languages is given. Moreover, the authors
demonstrate their application on the specification language JML.

However, some JML tools, including ESC/Java2 (Flanagan et al.
2002; Cok and Kiniry 2004) ignore visibility modifiers in specifications.
The emergence of separation logic (Isthiaq and O’Hearn 2001;
Reynolds 2002) provides a novel way to handle the challenging
aliasing issues for heap-manipulating programs. Parkinson and
Bierman (2005) and Parkinson (2005) recently extended separation
logic to handle OO programs. They advocated the use of abstract
predicate families indexed by types to reason about objects froma class hierarchy. Their approach supports full object views andessentially dynamic specifications, though for one class at a time.
They also require every inherited method to be re-specified andmostly re-verified for OO conformance. Furthermore, no implementation exists. In comparison, we have designed a more comprehensive system with static specifications, partial views and modular mechanisms to minimise on re-verification and to handle Zã#
method calls. These issues were informally referred to as untamed
open problems in Sec 6.5 of Parkinson (2005).

8. Conclusion
We have presented an enhanced approach to OO verification basedon the co-existence of both static and dynamic specifications, together with a principle that each static specification be a subtype of
its corresponding dynamic specification. Our approach attempts totrack the actual type of each object, where possible, to allow static
specifications to be preferably used. We have built our work on theformalism of separation logic, and have designed a new object format that allows each object to assume the form of its superclassvia lossless casting. Another useful feature of our proposal is a new
specification subsumption relation for pre/post specifications that is
novel in using the residual heap state from precondition checking
to assist in postcondition checking.
We have constructed a prototype system for verifying OO
programs. Our prototype is built using Objective CAML augmented with an automatic Presburger solver, called Omega (Pugh1992). While Presburger arithmetic is limited to integer constraints, we have also provided hooks in our system to invoke Isabelle and MONA provers. These extensions allow us to support
sets/bags/lists constraints, where required. The main objective forbuilding this prototype is to show the feasibility of our approachto enhanced OO verification based on a synergistic combinationof static and dynamic specifications. As an initial study, we havesuccessfully verified a set of small benchmark programs. The verification process consists of two parts: verification of the given
static specifications against the bodies of the corresponding methods (VS) and the specification subtyping checking meant to avoid
re-verification of all dynamic specifications and some static specifications of statically-inherited methods (SSC). What we are mainlyinterested in is the ratio between the VS timing and the SSC timing. As subsumption checking on specification is typically cheaper
than verifying a piece of program code against its specification,
we expect that VS will dominate the total verification time. This
assumption is indeed validated by the examples we tried. For instance, in the counter example presented in the paper, the time takenby the SSC (with 16 checks) is 0.06 seconds, while VS (with 11
verifies) takes 0.18 seconds. For examples with larger code bases,
we expect the ratio between the VS and SSC to increase.
One fundamental question that may arise is whether static specifications are really necessary? Some readers may contend that it ispossible to incorporate the effect of static specification by adding
type #G-H##_ [ into the precondition of a dynamic pre/post annotation. As discussed in our paper, this approach is only a partial
solution to static specification as (i) it does not cater to staticallyinherited methods which support reuse of static specifications, (ii) it
does not handle Zã# method calls which are really static method

invocations, and (iii) it does not help enforce class invariants in
subclasses when dynamic specifications of a superclass (without
the class invariant property) are being inherited. By making eachstatic specification be a subtype of its dynamic specification, we
can limit code verification to only static specifications. The underlying philosophy of static specification is better served by partial
view and lossless casting. Perhaps, the ultimate goal for OO verification is to use completely static specifications – with dynamic
specifications derived on demand! Our solution can be viewed as asignificant step towards this utopia.
Post-Submission Note : Independent of our work, Parkinson and
Bierman (2008) proposed in the same proceedings a similar distinction and relation between static and dynamic specifications, in
support of modular verification and the handling of direct method
calls. Like us, they can support inheritance and overriding, while
avoiding unnecessary re-verifications. However, there are at least
two differences. Firstly, they continue to rely on the rather powerful concept of abstract predicate families, while we have avoided its
use in our work. Secondly, we have a marginal emphasis on static
specifications over dynamic specifications, as we advocate for thelatter to be derived from the former, when needed, using the refinement techniques of specification specialization and abstraction.
Acknowledgments : Cristian Gherghina implemented a prototype
system for OO verification. Florin Craciun, Hugh Anderson, Martin
Rinard, Peter O’Hearn and anonymous reviewers provided insightful feedbacks on various aspects of this work. Matthew Parkinson
and Gavin Bierman conducted helpful last minute discussions withus. This work is supported by an A*STAR-funded research project
R-252-000-233-305 on “A Constructive Framework for Dependable Software”. Shengchao Qin is supported in part by the EPSRC
project EP/E021948/1.

References
P. America. Designing an object-oriented programming language withbehavioural subtyping. In the REX School/Worshop on Foundations of
Object-Oriented Languages, pages 60–90, 1991.
M Barnet, R. DeLine, M. Fahndrich, K.R.M Leino, and W. Schulte. Verification of object-oriented programs with invariants. Journal of Object
Technology, 3(6):27–56, 2004.
M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming
system: An overview. In Workshop on Construction and Analysis ofSafe, Secure, and Interoperable Smart Devices, 2004.
D. R. Cok and J. Kiniry. ESC/Java2: Uniting ESC/Java and JML. In Int’lWorkshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pages 108–128, 2004.
K. K. Dhara and G. T. Leavens. Forcing behavioral subtyping through specification inheritance. In IEEE/ACM Intl. Conf. on Software Engineering,
pages 258–267, 1996.
J. C. Filliâtre. Why: a multi-language multi-prover verification tool. Technical Report 1366, LRI, Université Paris Sud, March 2003.
R. B. Findler and M. Felleisen. Contract soundness for object-oriented
languages. In SIGPLAN Object-Oriented Programming Systems, Languages and Applications, pages 1–15, 2001.
R. B. Findler, M. Latendresse, and M. Felleisen. Behavioral contracts
and behavioral subtyping. In ESEC/SIGSOFT Foundations of Software
Engr., 2001.
C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and
R. Stata. Extended Static Checking for Java. In ACM PLDI, June 2002.
J. Hatcliff, X. Deng, M. B. Dwyer, G. Jung, and V. P. Ranganath. Cadena:
An integrated development, analysis, and verification environment forcomponent-based systems. In IEEE/ACM Intl. Conf. on Software Engineering, 2003.
S. Isthiaq and P.W. O’Hearn. BI as an assertion language for mutable data
structures. In ACM POPL, London, January 2001.

J. Kiniry, E. Poll, and D. Cok. Design by contract and automatic verification
for Java with JML and ESC/Java2. ETAPS tutorial, 2005.
G. T. Leavens and Peter Muller. Information hiding and visibility in interface specifications. In IEEE/ACM Intl. Conf. on Software Engineering,
pages 385–395, Washington, DC, USA, 2007. IEEE Computer Society.
G. T. Leavens and David A. Naumann. Behavioral subtyping is equivalent
to modular reasoning for object-oriented programs. Technical Report
06-36, Department of Computer Science, Iowa State University, 2006.
G. T. Leavens, A.L. Baker, and C. Ruby. Preliminary design of JML: A
behavioral interface specification language for Java. ACM SIGSOFT
Software Engineering Notes, 31(3):1–38, 2006.
G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, P. Mller, andJ. Kiniry. JML Reference Manual (DRAFT), February 2007.
K. R. M. Leino and P. Müller. Object invariants in dynamic contexts. In
ECOOP, pages 491–516, 2004.
B. H. Liskov. Data abstraction and hierarchy. ACM SIGPLAN Notices, 23(5):17–34, May 1988. Revised version of the keynote address given at
OOPSLA’87.
B. H. Liskov and J. M. Wing. A behavioral notion of subtyping. ACM Trans.
on Programming Languages and Systems, 16(6):1811–1841, 1994.
C. Marché and C. Paulin-Mohring. Reasoning about Java programs withaliasing and frame conditions. In 18th Int’l Conf. on Theorem Proving
in Higher Order Logics. Springer, LNCS, August 2005.
C. Marché, C. Paulin-Mohring, and X. Urbain. The K RAKATOA tool for
certification of JAVA /JAVA C ARD programs annotated in JML. Journalof Logic and Algebraic Programming, 58(1–2):89–106, 2004.
B. Meyer. Object-oriented Software Construction. Prentice Hall. Second
Edition., 1997.
R. Middelkoop, C. Huizing, R. Kuiper, and E. J. Luit. Invariants for nonhierarchical object structures. In L. Ribeiro and A. Martins Moreira,editors, Proceedings of the 9th Brazilian Symposium on Formal Methods(SBMF’06), Natal, Brazil, 2006.
P. Muller. Modular specification and verification of object-oriented programs. Springer, New York, NY, USA, 2002. ISBN 3-540-43167-5.
H. H. Nguyen, C. David, S.C. Qin, and W.N. Chin. Automated Verificationof Shape And Size Properties via Separation Logic. In Intl Conf. on
Verification, Model Checking and Abstract Interpretation, Nice, France,
January 2007.
J. W. Nimmer and M. D. Ernst. Invariant inference for static checking. In
ESEC/SIGSOFT Foundations of Software Engr., pages 11–20, 2002.
P. W. O’Hearn. Resources, concurrency, and local reasoning. Theor.
Comput. Sci., 375(1-3):271–307, 2007.
P. W. O’Hearn, H. Yang, and J. C. Reynolds. Separation and Information
Hiding. In ACM POPL, Venice, Italy, January 2004.
J. Ostroff, C. Wang, E. Kerfoot, and F. A. Torshizi. Automated model-based
verification of object-oriented code. Technical Report CS-2006-05, York
University, Canada, May 2006.
M. J. Parkinson. Local Reasoning for Java. PhD thesis, Computer Laboratory, University of Cambridge, 2005. UCAM-CL-TR-654.
M. J. Parkinson and G. M. Bierman. Separation logic and abstraction. In
ACM POPL, pages 247–258, 2005.
M. J. Parkinson and G. M. Bierman. Separation logic, abstraction andinheritance. In ACM POPL, 2008.
C. Pasareanu and W. Visser. Verification of Java programs using symbolic
execution and invariant generation. In SPIN Workshop, April 2004.
W. Pugh. The Omega Test: A fast practical integer programming algorithm
for dependence analysis. Communications of the ACM, 8:102–114,
1992.
J. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In IEEE Logic in Computer Science, Copenhagen, Denmark, July
2002.
Robby, M. B. Dwyer, and J. Hatcliff. Bogor: an extensible and highlymodular software model checking framework. In ESEC/SIGSOFT Foundations of Software Engr., pages 267–276, 2003.