Verifying Safety Policies with Size Properties and Alias Controls
Wei-Ngan Chin1,2 , Siau-Cheng Khoo1 , Shengchao Qin3∗, Corneliu Popeea1 , and Huu Hai Nguyen2
1
Department of Computer Science, National University of Singapore
2Computer Science Programme, Singapore-MIT Alliance3
Department of Computer Science, University of Durham{chinwn|khoosc|popeeaco|nguyenh2}@comp.nus.edu.sg

Abstract
Many software properties can be analysed through a relational
size analysis on each function’s inputs and outputs. Such relational analysis (through a form of dependent typing) has been successfully applied to declarative programs, and to restricted imperative programs; but it has been elusive for object-based programs.
The main challenge is that objects may mutate and they may bealiased. In this paper, we show how safety policies of programs
can be analysed by tracking size properties of objects and be enforced by objects’ invariants and the preconditions of methods.
We propose several new ideas to allow both mutability and sharing of objects, whilst aiming for precision in our analysis. We introduce the concept of size-immutability to facilitate sharing, andalso a set of alias controls to track unaliased objects whose size
properties may change. We formalise our results through a setof advanced type checking rules for an object-based imperative
language. We re-affirm the utility of the proposed type system byshowing how a variety of software properties can be automaticallyverified according to size-inspired safety policies.

Categories and Subject Descriptors
D.2.4 [Software Engineering]: Software/Program Verification—
Dependent Types; F.3.1 [Logics and Meanings of Programs]:
Specifying and Verifying and Reasoning about Programs

General Terms
Languages, Theory, Verification
This work was mostly done while the author was affiliated with
the Singapore-MIT Alliance, National University of Singapore.
∗

ICSE 2005, St. Louis, Missouri, USA.

shengchao.qin@durham.ac.uk

Keywords
Object-based programs, Safety verification, Dependent types,
Size properties, Alias control

1. Introduction
Size properties are extremely useful in program analysis to support program optimization and verification. Each piece of data
structure typically has one or more associated size properties. For
simple types, such as int, bool or file, size property can capture
their values (or abstract states). For aggregate types, size may referto the length/height of linked structures, cardinality of collections
or bounds of arrays. We may also ascribe size property to memory utilization in order to estimate space required for execution.
For functions, size property can capture relations between input
and output sizes, input preconditions, and also size invariance forparameters in recursion[10].
Past research into size properties has been most explored forfunctional [23, 22, 36, 10] and logic programming languages [34,3]. Such properties have been applied to a range of important
problems, including: (i) array bound check elimination [38, 39],(ii) memory space estimates for both region model [22] and heapwith-reuse model [21], (iii) complexity analysis [18], (iv) termination analysis[3, 26], and (v) support for safer programming where
size invariants (e.g. balanced AVL trees) are guaranteed at compile time[36]. These applications are important towards supporting the goal of more reliable (and rigorous) software engineering
processes. They constitute a realization of the automated verification for size-based software contracts.
To track size properties accurately, a relational analysis is required. This is expressible through a form of dependent typing[36],known as sized type[23, 10], that has been applied to declarative
paradigms. To the best of our knowledge, no one has successfully
designed a relational size analysis (or corresponding dependent
type system) for static reasoning of object-based imperative programs.
Two key problems with objects are mutability and aliasing.
Objects may mutate and their property changes be tracked. Objects may also alias with each other, and this must be analysed
and/or be controlled. To highlight the problem of aliasing in thepresence of mutation, consider the following Int object type expressed as an abstract data type (ADT), with an increment method.

adt Int { int val ;void incr(Int x, int v) { x.val = x.val + v } }Each object of the Int type has a primitive integer val field,
whose size we may wish to track. To do so, we introduce an annotated object type, say Inthni, where n is a size variable for capturing the value of the val field via n=m and with true as theobject’s invariant, as follows:adt Inthni where n=m ; true { inthmi val ; · · · }Consider two variables a and b of the Int type. We can provide
an annotated type for these variables using a :: Inthxi, b :: Inthyi,
where x and y denote the sizes of current objects referenced by aand b, respectively. Consider now a program fragment with aliasing and updates.
Int a = new Int(5); // x0 = 5
Int b = a;// y0 = x ∧ x0 = x
incr(a, 1);// x0 = x + 1
Ideally, we would like to perform size analysis, locally for eachstatement, as shown on the RHS. This would result in the following state x0 = 6 ∧ y0 = 5, after composing the effects of the threestatements. However, this reasoning is unsound as we did not takealias relationships into account. Note the use of the prime notation(e.g. x0 , y0 ) to denote new states of the size variables after eachstatement.
Accurately tracking the sizes of mutable objects requires thealiasing problem to either be carefully analysed or be tightly controlled. In this paper, we chose the latter path, as analysing global
aliases could quickly become unmanageable. Our main contributions are:
• We have successfully designed a sized type system for objects, which is able to track size information accurately. To
the best of our knowledge, no one has applied such an advanced relational analysis to object-based imperative programs before.
• Each object declaration is expressed as an ADT. Our motivation for using ADTs is to allow each set of software properties to be specified via a safety policy (or protocol), whose
correct usage can be automatically verified against the size
invariant of each ADT and the preconditions on its libraryof operations.
• Our approach provides an elegant balance between mutability and sharing, while working towards accurate size tracking. We achieve this using a novel property, called sizemutability, obtained with a set of alias controls. We use
read-only annotation for size-immutability, and uniquenessand lent annotations to limit aliasing for mutable size properties.
• We formalise a set of advanced type checking rules withalias controls and size constraints. We have implemented a
prototype to validate our proposal and have also proven key
safety theorems to confirm the desired properties of welltyped programs.
Sec 2 proposes a core imperative language with objects, andhighlights how size properties are captured via an annotated typesystem. Sec 3 introduces the basic concept of size-mutability andhow to track it using alias controls. Sec 4 shows how safety protocols may be specified through size invariants and methods’ preconditions in ADTs. Sec 5 presents a set of advanced size-checking
type rules, followed by key correctness properties. Sec 6 describes
related work, followed by a short conclusion.

2. Kernel Language
We design a simple kernel language, called OI MP, with alias
and size annotations. We present an object-based rather than an
object-oriented language to focus on the key issues for the size
analysis of objects. We intend for OI MP to be used as a backend
to existing programming languages, such as Java, C or C++. Its
syntax is given in Fig. 1. Note that the suffix notation y ∗ denotes
a list of zero or more distinct syntactic terms that are suitably separated. For example, (t v)∗ denotes t1 v1 , . . . , tn vn where n≥0.
P ::= prim∗ user∗ meth∗prim ::= adt pnhn1 , . . . , np i where {n∗ }; φI {pmeth∗ }user ::= adt cnhn1 , . . . , np i where φ ; φI {field∗ meth∗ }pn ::= void | bool | int | float | · · ·pmeth ::= t mn ((t v)∗ ) where φpr ; φpometh ::= t mn ((t v)∗ ) where φpr ; φpo {e}τw::= cn | pn::= v | v.ft ::= τ hn∗ i@A
field ::= t f

A ::= U | L | S | R

e ::= (cn) null | k | w | w = e | if v then e1 else e2| new cn(v ∗ ) | mn (v ∗ ) | t v = e1 ; e2
| bind v of (v1 , .., vn ) in eφ∈ F(Presburger Size Constraint)::= b | φ1 ∧ φ2 | φ1 ∨ φ2 | ¬φ | ∃n · φ | ∀n · φb ∈ BExp(Boolean Expression)::= true | false | α1 = α2 | α1 < α2 | α1 ≤ α2α ∈ AExp(Arithmetic Expression)::= c | n | c ∗ α | α1 +α2 | −α | max(α1 ,α2 ) | min(α1 ,α2 )where c ∈ Z is an integer constant ; n ∈ SV is a size variablef ∈ Fd is a field name ; v ∈ Var is an object variable

Figure 1. Syntax for the OI MP language
Local variable declaration is supported by block structure of theform: (t v = e1 ; e2 ) with e2 denoting its result. For convenience,
we may also use τ instead of t and rely on fresh size variables
and alias defaults for annotations. We assume a call-by-valuemechanism for OI MP, where values (primitives or references) are
passed as arguments to parameters of methods. For simplicity, we
do not allow parameter updates (or re-assignments). There is noloss of generality, as we can always copy parameters to local variables for updating, without altering the observable behaviour of
method calls. Each user-defined method declaration meth contains
a precondition φpr and a postcondition φpo . The former must be
satisfied for each caller, while the latter must be ensured by themethod’s body. For size constraints used (e.g φpr and φpo ), we
restrict to Presburger arithmetic, as decidable (and practical) constraint solvers exist, e.g. [32]. For each reference (variable, parameter or field) of an object type, we add an alias control, namedA, as follows: τ hn1 , . . . , nm i@A. Each alias control could either be
R, U, S or L to denote read-only, unique, shared or lent-once, respectively. They are primarily used to track the mutability of size
properties for objects and uniqueness of their references, and will
be elaborated later in Sec 3.
The OI MP language has been kept simple to make easier theformulation of static and dynamic semantics. Typical language
constructs, such as multi-declaration block, sequence, calls with

complex arguments, etc. can be automatically translated to constructs in OI MP. Also, loops can be viewed as syntactic abbreviations for tail-recursive methods, and are supported by our analysis.

2.1 Primitive ADTs
We provide two kinds of object type, namely primitive (prim)
type or user-definable (user) type. Both are expressed using the
ADT mechanism to allow safety policies on objects to be specified. For each primitive ADT, we specify a set of size variables
n1 , . . . , np with a size invariant φI that holds for each object, and{n∗ } to capture a subset of the size variables that are mutable. We
also specify a set of primitive method declarations that are trusted
to meet its postcondition φpo , whenever its precondition φpr is satisfied. An example is the bool primitive ADT, with no mutablesize variables and 0≤n≤1 as its size invariant.
adt boolhni where {} ; 0≤n≤1{ boolhri@S not(boolhmi@S) where
true; m0 =m∧(m=0∧r=1∨m=1∧r=0); · · · }Another example is the array ADT, with a safety policy that noarray bound violations ever occur, as given below:
adt Arrayhsi where {}; s>0{Arrayhsi@U newArray(inthni@S a, inthvi@S val)
where n>0 ; s = n∧noX {n, v};
inthri@S sub(Arrayhsi@S a, inthii@S idx)
where 0 ≤ i < s ; noX {s, i} ;voidhi@S update(Arrayhsi@S a, inthii@S idx,
inthvi@S val) where 0 ≤ i < s ; noX {s, i, v} ;inthri@S len(Arrayhsi@S a) where true ; r = s∧s0 =s; }Safe array bound is guaranteed by the precondition 0≤i < s forthe sub method (to retrieve an element of the array) and update
method (to modify a location of the array), while n > 0 is for the
newArray method (to create a new array of positive size). Furthermore, the array’s size is never changed by any of the operations. This may be specified through noX which returns a formula where the original and prime variables are made equal, e.g.
noX {s, i}≡(s0 =s∧i0 =i). As every call’s precondition is checked,
no array bound violation occurs. The binary search method below
adheres to this safe array policy, with the help of the precondition0≤i∧j<s.
inthri@S bs(Arrayhsi@S a, inthii@S i, inthji@S j, inthvi@Sval) where 0≤i∧j<s ; noX {s, i, j, v}∧(r=−1∨i≤r≤j) {if j<i then −1 else { int m=(i+j)/2; int p=sub(a, m);
if p<val then bs(a, i, m−1, val)else if p>val then bs(a, m+1, j, val) else m } }For some problems, e.g. sparse matrix, the indexes may comefrom another array, called an indirection array. To handle suchprograms, we can provide:
adt ArrayIhs, mn, mxi where {mn, mx}; s>0∧mn≤mx {voidhi@S update(ArrayIhs, mn, mxi@L a,
inthii@S idx, inthvi@S val) where 0 ≤ i < s ;mx0 = max(mx, v)∧mn0 = min(mn, v)∧noX {s, i, v}

inthri@S sub(ArrayIhs, mn, mxi@L a, inthii@S idx)
where 0 ≤ i < s ; mn ≤ r ≤ mx∧noX {s, mn, mx, i}; · · · }Apart from s which captures the size of the array, we also havemn and mx to capture the min/max values for the elements in thearray. The last two size variables are mutable and may be changedby the update method, but is guaranteed to satisfy the size invariant mn≤mx. Furthermore, we can bound the result of sub method
whenever indexes are retrieved from an indirection array.

2.2 User-Defined ADTs
Each user-defined ADT is specified with a set of fields thatare visible only to its accompanying methods. (In particular, eachnew or bind construct may only be used within its ADT declaration.) For each ADT declaration, we specify a set of size variables
n1 ,V. . . , np that can be tracked via the constraint φ, that is limited
to pi=1 ni =αi whereby V(αi )∩{n1 , . . . , np }=∅. This defines
size properties that depend solely on object components. Anotherconstraint φI is used to capture the size invariant of each instanceof this object type. For example, a user-defined Bool object typecan be specified in terms of a primitive bool field, as follows. Notethat this primitive field may be updated.
adt Boolhni where n=m ; 0≤n≤1 { boolhmi@S val;
voidhi@S Not(Boolhmi@L v) where true;m=0∧m0 =1∨m=1∧m0 =0 {b.val=not(b.val)}; · · · }A more complex example is the binary tree with a size variable s
to track the number of nodes, defined as:
adt Treehsi where s=1+s1+s2 ; s≥0{ inthvi@S val ; Treehs1i@U left ; Treehs2i@U right; · · · }Alternatively, if we desire AVL trees, we could add a size variable
h for height and another invariant −1≤h1−h2≤1 to enforce a balanced height requirement, as shown below. This invariant can beviewed as a safety policy for our type system to ensure that only
proper AVL trees (with this invariant) are constructed.
adt AVLTreehh, si where h=1+max(h1, h2)∧s=1+s1+s2; h≥0∧s≥0∧(−1≤h1−h2≤1){ inthvi@S val ; AVLTreehh1, s1i@U left ;AVLTreehh2, s2i@U right; · · · }Size invariant is safely verified within each ADT, while a method’s
precondition is verified for each of its callers.

2.3 A Special Construct
Our kernel language includes a special construct, called bind,which is used to associate the fields f1 , . . . , fn of an object v toa set of local variables v1 , . . . , vn . This binding is valid over thescope of an expression e and results in local variables being usedas synonyms to the corresponding fields. Unlike the usual patternmatching construct (see [37]), bind is based on a pass-by-name(instead of pass-by-value) mechanism. Furthermore, it is used only
for the purpose of analysis and do not cause runtime overheads.
This construct is particularly crucial for tracking the size properties of objects that depend on multiple components. For example,
consider a method to insert an element into a binary search tree.

voidhi@S insert(Treehsi@L t, inthci@S i)
where s>0 ; c0 =c{ if i<t.val then if t.left=null thent.left = new Tree(i, null, null)else insert(t.left, i)else if t.right=null thent.right = new Tree(i, null, null)else insert(t.right, i) }With the field access construct, we can only capture the size
relation between an object and a single field. With the bind construct, we can capture the size relation between an object and allits fields. Hence, we can capture a more precise size mutation
for size variables that depend on multiple fields, as illustrated in
the following alternative definition of insert. The local variables
w, l, r are associated with the corresponding fields, in the sameorder as their declaration.
voidhi@S insert(Treehsi@L t, inthci@S i)
where s>0 ; c0 =c∧s0 =s+1
{ bind t of (w, l, r) in
if i<w then if l=null then l = new Tree(i, null, null)else insert(l, i)else if r=null then r = new Tree(i, null, null)else insert(r, i) }Despite being special, we can automatically insert bind constructs into our program as follows. For each field access v.f ofa variable v, we identify the largest expression scope that anticipates a field access but does not access v itself (unless it is inshared mode), before introducing a binding for v and its fields
v.f1 , . . . , v.fn through a fresh set of local variables.

lendings for a single object, and of allowing lents to be reassigned
to other lent locations, may cause aliasing problems to re-surface.
To avoid this problem, we propose a refined policy, called lentonce1 :D EFINITION 4 (L ENT-O NCE ). A parameter that is marked
as lent-once (denoted by L) has the following properties: (i) its
value does not escape the method, (ii) the lent-once parameter isnever re-assigned, (iii) it has exclusive access to the object in its
method’s scope.
The last two conditions prevent aliases from occurring in the scopeof each lent-once location. As we exclude local variable fromthe L-mode, call sites are the only places where lendings can occur. While this lent-once policy may appear restrictive, its shortcoming can be addressed by preprocessing (converting lent to lentonce, where possible) and intersection types[30] (allowing different parameter aliasing for each call site).

3.1 Alias Subtyping
As we deal with the types of expressions, our subtype relation (shown below) need not include R. Each value retrieved froman R-field is automatically casted to the S-mode. Note that Umode references act as universal sources, while L-mode locations
serve as sinks only. This subtyping effectively prevents an Sreference from being copied into a U-location. Unlike [1], we disallow S ≤a L to enforce non-aliasing of the L-mode parameters.
A ≤a AU ≤a LU ≤a S

3.2 Size Mutability

3. Alias Controls for Size Tracking
We adopt four alias controls from [7, 1], namely read-only (R),lent (L), shared (S) and unique (U). Each reference in a location(field, parameter or local variable) can be marked with any of theannotations, except that L-mode applies only to parameters. While
the alias controls are adapted from [1, 7], there are differences in
how the type rules are being checked, as described later in Sec 5.
Formal definitions of these alias properties are given below.

Our main idea for tracking size properties is the concept of sizemutability. To help identify size properties that are immutable forobjects, we shall use the read-only mode to protect certain fields
from being changed. We classify each field and size variable, as
follows:
D EFINITION 5 (S IZE -M UTABILITY FOR F IELD ). A field isclassified as size-immutable, if it is marked with the R-mode. Otherwise, it is classified as size-mutable.

D EFINITION 1 (R EAD -O NLY ). A location that is marked as
read-only (denoted by R) can be initialized with a reference, butcannot be changed thereafter via the location.

D EFINITION 6 (S IZE -M UTABILITY FOR S IZE VARIABLE ).
A size variable of an object type is size-immutable if it depends
on only size-immutable variable(s) that come from size-immutable
field(s). Otherwise, it is size-mutable.

D EFINITION 2 (U NIQUENESS ). A reference to an object is
unique (denoted by U) if it is the only reference to the object at thecurrent scope.

For some primitive type, like inthni, its size variable is automatically classified as size-immutable, as its values cannot be changed
after they have been created. For user-defined object type, like
Inthni, its field (size property) may change after its objects havebeen created and is therefore size-mutable, in general. Nevertheless, we can obtain more size-immutable fields/variables with thehelp of the R-mode. Consider:

D EFINITION 3 (S HARED ). A reference (from a location) to
an object is shared (denoted by S) if it may be globally aliased
with other reference(s).
In classical alias annotation work[1], the L-mode is used to describe variables whose references do not escape their declaration
blocks. Such locations are candidates for lending, as the uniqueness of source objects are not compromised. As a result, each object can be lent out multiple times. The uniqueness property isalways restored once all locations that are lent out (including transitive lending) are dead. However, the policy of allowing many

adt Pairha, b, ci where a = p ∧ b = q ∧ c = p+q ; true
{ inthpi@S x; inthqi@R y; · · · }adt Listhni where n = m+1 ; n≥0{ Inthvi@S val; Listhmi@R next; · · · }1
Subsequent to our formulation, we found out that a similar policy,
called limited unique, has already been proposed in [9], though
their focus has been on the specification of such properties and not
on a formal mechanism, such as the type-based one proposed here.

In Pair, the first field is size-mutable, while the second field issize-immutable. Of its three size variables {a, b, c}, only b is sizeimmutable. This is because b depends on only size-immutable q
which came from a read-only field. In List, we use n to track
the length of the linked list, and this is made size-immutable byprotecting the next field with the R-mode.
Objects may be freely shared without losing track of the properties of their size-immutable variables. However, the same cannot
be said for size-mutable variables, as global aliasing can quickly
invalidate local analysis. Our solution for objects with size-mutable
fields to track, is to make their references unique. Uniqueness canguarantee that the references of these fields are never aliased.
For example, we can design another list structure whose next
field can be updated but must be unique, as shown below. Notethat uniqueness allows the length of this linked list to be tracked,
even with mutation on its tail.
adt List2hni where n=m+1 ; n≥0{ Inthvi@S val; List2hmi@U next; · · · }3.3 Classification of Size Variables
Thus far, we have classified size variables into two main groups,
namely size-mutable and size-immutable. However, the size-mutablegroup can be further classified into either trackable or non-trackablesize variables, due to the absence or presence of global aliasing,respectively. This classification of size variables can be inferredfrom the objects’ type declarations. We provide a pair of mutual recursive definitions, named Vobj and Vfield , to classify thesize variables of annotated object type and fields/parameters (withsuffixes I, T , and N to denote immutable, trackable and nontrackable respectively), as follows:
Vobj (τ hs∗ i) = (dI , dT , dN )Vfield (τ hs∗ i@R) =df (dI , ∅, dT ∪ dN )Vobj (τ hs∗ i) = (dI , dT , dN )Vfield (τ hs∗ i@S) =df (∅, dI , dT ∪ dN )A ∈ {U, L}
Vobj (τ hs∗ i) = (dI , dT , dN )Vfield (τ hs∗ i@A) =df (∅, dI ∪ dT , dN )adt pnhn∗ i where MVar; φI {pmeth∗ } ∈ P
Vobj (pnhn∗ i) =df (n∗ − MVar, MVar, ∅)adt cnhn∗ i where φ ; φI {(ti fi )i:1..p meth∗ } ∈ P
N
Vfield (ti ) = (dIi , dT), i ∈ {1..m}i , di S∗
I
nI = depends(n , Sm
i=1 di , φ)m∗nT = depends(n , Si=1 dTi , φ)NnN = depends(n∗ , m
i=1 di , φ)Vobj (cnhn∗ i) =df (nI − (nT ∪ nN ), nT − nN , nN )For each field with size variables s ∗ , we extract from n ∗ thosethat depend on some s ∗ via φ. This dependency is defined below.
Each primitive constraint from φ is of the restricted form n = α.
We define V to return all free size variables in a formula. For example, V(x0 = z + 1 ∧ y = 2) = {x0 , y, z}. We extend it to annotatedtype and type environment, e.g. V(τ hn∗ i@A) = {n∗ }.

depends(n ∗ , s ∗ , φ) =dfS(n=α)∈φ {n | (V(α)∩s∗)6=∅ }

Given φP = (a = p ∧ b = q ∧ c = p+q) from the Pair object
definition, we can infer that {b} is size-immutable, {a, c} aretrackable size-mutable and ∅ denotes an empty set of non-trackablesize-mutable variables.
nI = depends([a, b, c], [q], φP ) = {b, c}nT = depends([a, b, c], [p], φP ) = {a, c}
Vobj (Pairha, b, ci)= ({b}, {a, c}, ∅)For each object type declaration that is recursive, we may derive
definitions for Vobj and Vfield that are circular, but they can still beanalysed via fixed-point computation.

4. Specification of Safety Protocols
With the help of size (and alias) annotations, we can specify
suitable safety policies for software through the use of size invariants for each object type and the use of preconditions for eachmethod declaration. Apart from enforcing data structure invariant(e.g. AVL tree) and avoiding bound violations (e.g. safe array),
we may also check if operations of an ADT are invoked according
to a temporal protocol.
Let us highlight how we can specify the safety policy for a file
protocol (defined below) that allows read/write from a file only after it has been opened. The state of each file is encoded by s∈1..3
with 1, 2, 3 to denote initial, open, and close states, respectively.
(While the states of protocol are encoded using integer values, westress that it is easy to use syntactic sugar to make protocol specification more natural to programmers. Furthermore, our use of
integer domain to encode values of finite states is meant to support
a more convenient relational analysis via Presburger constraints.)
Once closed, no more read/write operations can be performed.
These temporal requirements are enforced by the sized preconditions of each method. In general, not all the safety preconditions
can be enforced directly, but we allow programmer to insert runtime tests to ensure conformance. For example, opening a file may
fail if it does not exist and this situation can be co-related with thereturned flag (of open) that can be tested at runtime.
adt Filehsi where {s}; 1≤s≤3 {Filehsi@U newFile() where true; s=1
boolhbi@S open(Filehsi@L f, stringhi@S name)where s=1; (b=1∧s0 =2)∨(b=0∧s0 =1)
stringhi@S read(Filehsi@L f) where s=2; s0 =2
voidhi@S write(Filehsi@L f, stringhi@S buf)
where s=2; s0 =2
voidhi@S close(Filehsi@L f) where s=2; s0 =3
inthri@S getState(Filehsi@L f)where true; r=s∧s=s0 }Capturing such a protocol as a primitive ADT assumes that its implementation has been separately verified against its stated interface. We can also rely on user-defined ADTs for the specificationof safety protocols. An example is the following bounded buffer
ADT which is guaranteed to neither underflow nor overflow eachbuffer of a given capacity.

adt Bufferhs, ci where s=n∧c=a;0≤s≤c∧0≤h<c∧0≤t<c∧c = e {Arrayhai@R arr; inthei@R cap; inthhi@S h; inthti@S t;
Bufferhs, ci@U newBuffer(inthni@S n)
where n>0; s=0∧c=n∧n0 =n{ new Buffer(newArray(n, 0), n, 0, n−1) }voidhi@S add(Bufferhs, ci@L b, inthni@S n)
where s<c; s0 =s+1∧noX {c, n}{ bind b of (a, c, h, t) in {update(a, h, n); h=mod(h+1, c)} }inthni@S get(Bufferhs, ci@L b)
where s>0; s0 =s−1∧c0 =c{ bind b of (a, c, h, t) in {t=mod(t+1, c); sub(a, t)} } · · · }Note the use of a cyclic array to store the contents of the buffer,with the help of the following mod primitive.
inthri@S mod(inthai@S x, inthbi@S y)
where b>0 ; 0≤r<b∧noX {a, b}This example illustrates how we can safely build a more sophisticated ADT from simpler ones. As an example of the use of thisbuffer ADT, we have the following method which can safely add
n elements, provided that the precondition s+n≤c is satisfied.
voidhi@S addMany(Bufferhs, ci@L b, inthni@S n,
inthvi@S val) where s+n≤c; s0 =s+max(0, n)∧noX {c, n, v}{ if n≤0 then ()else add(b, val); addMany(b, n−1, val) }track the liveness of each unique field with the help of the bindconstruct and the dead set. These changes improve both the accuracy and usability of our alias analysis.
In the rest of this section, we highlight important aspects of oursized type system via examples. Before that, we introduce somepreliminary definitions. The function prime takes a set of size variables and returns their primed version, e.g. prime({s1 , . . . , sn })= {s01 , . . . , s0n }. Note that prime operation is idempotent, namely
v 00 = v 0 . We extend this to annotated type, type environment andeven substitution. For example, we have prime(τ hn1 , . . . , nk i) =τ hn01 , . . . , n0k i, and prime [x 7→ a, y 7→ b] = [x0 7→ a0 , y 0 7→ b0 ].
We use n∗ = fresh() to generate new size variables n∗ . We extend it to annotated type, so that t̂ = fresh(t) will return a new
type t̂ with the same underlying type as t but with fresh size variables instead. The function equate(t1 , t2 ) generates equality constraints for the corresponding size variables of its two arguments,
assuming that they share the same underlying type. For example,
equate(Inthri, Inths0 i)=(r=s0 ). The function rename(t1 , t2 )returns a mapping instead, e.g. rename(Inthri, Inths0 i)=(r7→s0 ).
To extract the alias of an annotated type, we use ann(τ hv ∗ i@A) = A.
The function inv(t) returns the size invariant of t (after quantifying the size variables of its fields), while inv(Γ) extends to typeenvironment. The function unify(t1 , t2 ) returns a new fresh typewhose alias annotation is an upper bound of t1 and t2 . Also, conditional is expressed as ξ1 ¢b¤ξ2 =df if b then ξ1 else ξ2 .
Updates of size constraint due to change of program state are
effected by a sequential composition operator, ◦X , with X denoting the set of size variables that are being updated. For example, if∆=(a0 =a+b ∧ b0 =3 ∧ i=a0 ), then we can obtain the following
where the a size variable is being updated.
(∆◦{a} a0 =i+1) = ∃a0 · a0 =a+b∧b0 =3∧i=a0 ∧a0 =i+1
= b0 =3∧i=a+b∧a0 =i + 1
More formally, sequential composition is defined as:

5. Verification via Sized Typing
We present type judgements for expressions, method declarations, object declarations and programs to check for their welltypedness, using relations of the form:
Γ; C; ∆; Θ ` e :: t, ∆1 , Θ1
C `meth meth`pmeth pmeth`prim prim`user user
`P prim∗ user∗ meth∗
Note that Γ is a type environment mapping program variables
to their annotated types; ∆(∆1 ) denotes the size constraint that
holds for the size variables associated with Γ (Γ and t) for expression e before (after) its evaluation; t is an annotated type. C
captures a set of user-defined ADTs whose fields are visible. Also,Θ(Θ1 ) is used to hold the variables whose uniqueness have been
consumed before (after) the evaluation of e. We shall refer to suchreferences as dead, as they are not to be accessed. Take note thatboth ∆(∆1 ) and Θ(Θ1 ) are tracked flow-sensitively.
The major syntax-directed type rules for these judgements are
given in Fig 2, whereas the rest of the rules are given in our technical report [11]. Compared to [1], we have attained two key innovations. Firstly, we do not require a separate last-use analysis
to determine when a unique reference (from a variable) becomesdead, as we keep track of consumed uniqueness via the dead set(denoted by Θ). Secondly, we do not require destructive read forfield access (which nullifies the field after each read). Instead, we

φ1 ◦X φ2 =df ∃R · ρ1 (φ1 ) ∧ ρ2 (φ2 )where X = {s1 , . . . , sn } are size variables being updated
R = {r1 , . . . , rn } are fresh size variablesρ1 = {s0i 7→ ri }nρ2 = {si 7→ ri }ni=1i=1

5.1 Variable Read
The [VAR] rule is used to return an object via a reference captured by variable v. Here, a unique reference loses its uniquenessand must not be referenced again (unless it has been re-assigned).
It is thus added to a dead set using Θ1 =Θ∪({v}¢A=U¤∅) where
A is the alias annotation for the type of v. This rule also returns a freshly annotated type t1 =fresh(t) and a size constraint
φ=equate(t1 , prime(t)) to relate the resulting annotated type withthat of variable v. Assuming Γ={v::Inthdi@U}, ∆=noX {d}, wehave:
φ = (r1 =d0 )v∈/ΘU 6= L
Γ; C; ∆; Θ ` v :: Inthr1 i@U, ∆∧φ, Θ ∪ {v}Note how the dead set has changed, and how the size property of
the result (namely r1 ) is associated with the latest size variables(namely d0 ) from the type environment. L-mode references cannot
escape via this rule.

[ASSIGN]
Γ; C; ∆; Θ ` e :: t1 , ∆1 , Θ1 Γ ` v::t, φ, Yann(t) 6∈ {L, R} ` t1 <: t, ρ X = V(t1 ) ∪ V(t)¬ isParam(v) ∆2 = ∃X · ∆1 ◦Y ρ(φ)Γ; C; ∆; Θ ` v = e :: voidhi@S, ∆2 , Θ1 /v[AUX]
Γ(v) = t t1 = fresh(t)φ = equate(t1 , prime(t))Γ ` v::t1 , φ, V(t)[VAR]Γ ` v::t, φ, Y A=ann(t) A6=Lv ∈Θ/
Θ1 =Θ∪({v}¢A=U¤∅)
Γ; C; ∆; Θ ` v :: t, ∆ ∧ φ, Θ1[CON−UL]
AS =ann(tS ) AT =ann(tT ) `tS <:tT , ρ
Θ1 =Θ∪({v}¢AS =U∧AT 6=L¤∅)v ∈(Θ∪Λ)/
Λ1 =Λ∪({v}¢AT =L¤∅)Θ, Λ, Ψ ` conUL(v, tS , tT ), Θ1 , Λ1 , Ψ]ρ

[BIND]
adt cnhs∗ i where φ; φI {(ti fi )i:1..p meth∗ } ∈ Pv ∈Θ/Γ(v) = cnhn∗ i@A ρ1 =U([U 7→ S]¢A∈{S, R}¤[])
cn∈C ρ2 =[s7→n0 ]∗ ρ3 =ρ2 ] pi=1 rename(ti , prime(ti ))Γ1 ={vi ::ρ1 ti }pi=1 Γ−{v|A∈{L, U}}∪Γ1 ; C; ∆1 ; Θ ` e :: t, ∆2 , Θ1
∆1 =∆∧(ρ2 φ∧φI )∧noX (Γ1 )∧inv(ΓS1 ) I=∃i∈1..p·vi ∈Θ1∆3 =∆2 ◦{n∗ } ρ3 φ Θ2 =(Θ1S− pi=1 {vi }) ∪{v|I}(¬I∧∆3 )⇒ρ3 φI I⇒(A=U) Y = pi=1 V(ti ) Z=Y ∪prime(Y )Γ; C; ∆; Θ ` bind v of (v1 , . . ., vp ) in e :: t, ∃Z·∆3 , Θ2

[CALL]
t̂0 mn((t̂i v̂i )i:1..p ) where φpr ; φpo · · · ∈ P
t0 = fresh(t̂0 ) Λ0 = ∅ ρ0 = [ ] Γ(vi ) = ti i ∈ 1..p
Θi−1 , Λi−1 , ρi−1 ` conUL(vi , ti , t̂i ), Θi , Λi , ρi i ∈ 1..p
ρ =S
rename(t̂0 , t0 )]ρp ]prime(ρp ) ∆ ≈>ρφSV(Γ) prX= pi=1 V(t̂i ) Y =X∪prime(X) L= pi=1 V(ti )Γ; C; ∆; Θ0 ` mn(v1..p ) :: t0 , ∆ ◦L ∃Y · ρ φpo , Θp
[IF]Γ; C; ∆∧b0 =1; Θ ` e1 :: t1 , ∆1 , Θ1
Γ; C; ∆∧b0 =0; Θ ` e2 :: t2 , ∆2 , Θ2 t=unify(t1 , t2 )Γ(v)=boolhbi@S ρi =rename(ti , t), i = 1, 2
∆3 = (ρ1 ∆1 )∨(ρ2 ∆2 ) Θ3 = Θ1 ∪ Θ2
Γ; C; ∆; Θ ` if v then e1 else e2 :: t, ∆3 , Θ3

[METH]
Γ = {v1 ::t1 , . . . , vp ::tp } ∆=noX (Γ)∧φpr ∧inv(Γ)Γ; C; ∆; ∅ ` e :: t, ∆1 , Θ ` t<:t0 , ρ
S ann(t0 ) 6= L ann(ti ) = Ai , i ∈ 0..p
Y = pi=1 (XN ∪(XT ¢Ai =U¤∅) | ( , XT , XN )=Vfield (ti ))(∃ prime(Y) · ∆1 )⇒ρ φpo ∀i∈1..p · (Ai =L)⇒vi 6∈ ΘC `meth t0 mn((ti vi )i:1..p ) where φpr ; φpo {e}[SUBT]
Vobj (τ hs1 , . . . , sm i) = (SI , ST , )(A3 , A4 )=[R 7→ S](A1 , A2 ) A3 ≤a A4
ρI = [ni 7→ si ]si ∈SI ρT = [ni 7→ si ]si ∈STρ = (ρI ¢A3 = S ∨ A4 = S¤ρI ] ρT )` τ hs1 , . . . , sm i@A1 <: τ hn1 , . . . , nm i@A2 , ρ

Figure 2. Major Size and Alias Type Rules for Safety Verification

5.2 Assignment
The assignment rule [ASSIGN] ensures that the LHS and RHS
are consistent in accordance with (i) alias subtyping (ii) flow of
trackable size properties (iii) imperative update of its LHS. It also
checks that the LHS is neither a parameter variable, nor in R- or
L-mode. To capture imperative update, we link the current size
constraint with a new updated state for the affected size variablesfrom the LHS. Given Γ = {x :: inthai@S}, we have:¬isParam(x) S 6∈ {L, R}
Γ; ∆1 ; Θ ` x + 1 :: inthr1 i@S, ∆2 , Θ∆2 = (∆1 ∧r1 = a0 +1) Γ ` x :: inthr2 i@S, a0 = r2 , {a}` inthr1 i@S <: inthr2 i@S, [r2 7→ r1 ]Γ; C; ∆1 ; Θ ` x = x + 1 :: voidhi@S, ∃r1 ·∆2 ◦{a} a0 = r1 , Θ

its mapping, namely [r2 7→ r1 ]. Some other examples are:` Pairhs1 , s2 , s3 i@U <: Pairhn1 , n2 , n3 i@S, [n2 7→ s2 ]` Pairhs1 , s2 , s3 i@U <: Pairhn1 , n2 , n3 i@U, [ni 7→ si ]3i=1` Pairhs1 , s2 , s3 i@S <: Pairhn1 , n2 , n3 i@U, !FAIL
Another important aspect of assignment is the restoration of theuniqueness for the LHS variable/field. As this is not applicable toshared objects, let us examine another example with ∆2 = noX {d}.
Notice a smaller dead set.
¬isParam(v)U 6∈ {L, R}
Γ; ∆2 ; {v} ` new Int(4) :: Inthr1 i@U, ∆2 ∧r1 = 4, {v}Γ ` v :: Inthr2 i@U, d0 = r2 , {d}` Inthr1 i@U <: Inthr2 i@U, [r2 7→ r1 ]Γ; C; ∆2 ; {v} ` v = new Int(4) :: voidhi@S, d0 = 4, {}5.3 Conditional
If ∆1 = (a0 = a), the final constraint simplifies to a0 =a+1 whichreflects the update. Apart from alias subtyping, the subtype relation [SUBT] also captures the flow of trackable size variables as a
mapping. In the case of the above, when an S-object flows to an
S-location, only the size-immutable size variable is captured via

For conditional, our rule is able to track the size constraint pathsensitively, but the dead set is tracked only flow-sensitively but not
path-sensitively. Given Γ1 = Γ+{x::boolhhi@S,v::Inthji@U} and∆=(h0 =0), we have:0Γ1 ; C; ∆∧h = 1; {}`v::Inthr1 i@U, false, {v}Γ1 ; C; ∆∧h0 = 0; {}`new Int(5)::Inthr2 i@U, ∆∧r2 = 5, {}Γ1 ; C; ∆; {} ` if x then v else (new Int(5)):: Inthr3 i@U, ∆∧r3 = 5, {v}Note that h0 = 1 and h0 = 0 captures path-sensitivity. As a result, the final size constraint is able to ignore an infeasible branch.
A branch is infeasible if its corresponding size constraint yields
false. However, the uniqueness of v is consumed even though it
occurs in the infeasible branch. This is so as the dead set is tracked
only flow-sensitively.

5.4 Method Declaration and Call
For method declaration, our type rule must ensure that eachdecoration at the method header is consistent with its body. The
declared size constraint may be weaker than the analysed size constraint (from the method body), but not vice versa. Note that
non-trackable size variables and mutable size variables of uniqueparameters must be quantified, as we do not track them acrossmethod boundary.
The rule for method call must ensure that U-mode parametersconsume uniqueness, and that L-mode parameters adhere to thelent-once policy. Relation Θ, Λ, Ψ ` conUL(v, tS , tT ), Θ1 , Λ1 , Ψ1
(named [CON−UL]) helps ensure the above. It checks that eachvariable v is neither lent twice, nor has its uniqueness consumed
twice. Note that Λ captures unique variables which are temporarily lent out. The method invocation rule also includes a safety
check on the precondition of the callee. This is performed by thepredicate ≈>X defined as follows:∆ ≈>X φ =df (∆ ⇒ ρφ), whereρ = [s1 7→ s01 , .., sn 7→ s0n ] and Vu (φ) ∩ X = {s1 , .., sn }.
where Vu returns the size variables in unprimed form, for example Vu (x0 =z+1∧y=2) = {x, y, z}. As an example of checking
a method call, givenΓ = {p :: Bufferhr, zi@U, v :: inthmi@S}∆ = (r0 =3 ∧ r=0 ∧ z=10 ∧ m=30 ∧ noX {z, m})
we obtain V(Γ) = {r, z, m} and the following:
t1 = Bufferhr, zi@U t̂1 = Bufferhs, ci@L
p 6∈ Θ ρ1 = [s7→r, c7→z]
Θ, ∅, [ ] ` conUL(p, t1 , t̂1 ), Θ, {p}, ρ1t2 = inthmi@St̂2 = inthni@Sv 6∈ Θ ∪ {p} ρ2 = ρ1 ] [n7→m]∆ ≈>V(Γ) (r < z)Θ, {p}, ρ1 ` conUL(v, t2 , t̂2 ), Θ, {p}, ρ2
Γ; C; ∆; Θ ` add(p, v) :: voidhi@S, ∆2 , ΘNote that uniqueness of p is only lent-out and not consumed.
We also have:∆2 = ∆ ◦{r,z,m} (r0 = r + 1 ∧ noX {z, m})= (r0 =4 ∧ r=0 ∧ z=10 ∧ m=30 ∧ noX {z, m})

5.5 Binding
The bind expression enables us to accurately capture the size
relations among object fields as well as between an object and its

fields. In addition, it can replace the field access construct altogether (for type checking). When an object subjected to a bind operation is marked by either R or S, all its unique fields are remarked
as S using [U7→S] in the scope of bind. On the other hand, the object will lose its uniqueness if any one of its fields loses it. For
instance, given Γ=Γ0 +{v::List2hni@U}, the following derivation demonstrates how v loses its uniqueness when its unique yfield loses it (denoted by I = (y∈Θ1 )):v∈/ Θ Γ0 ∪ Γ1 ; C; ∆1 ; Θ ` y :: t1 , ∆2 , Θ1 Θ1 = Θ∪{y}Γ(v)=t A=ann(t) I=(y∈Θ1 ) I⇒A=U ¬I∧∆3 ⇒n0 ≥0Γ; C; ∆; Θ ` bind v of (x, y) in y :: t1 , ∆4 , Θ1 −{y}∪{v|I}for some values Γ1 , t1 , ∆1 ,∆2 , ∆3 and ∆4 . As a counter-example,
consider bind v of (x, y) in x. Here, v does not lose its uniqueness as the uniqueness of its y field remains intact.
A well-typed bind expression also permits the size invariant φIof the bound object to be temporarily violated in its scope, but
ensures that φI holds whenever the object escapes. This is enforced by the check (¬I∧∆3 )⇒ρ3 φI with I denoting the loss of
one or more unique fields. Our rule also ensures that an object
and its unique fields are never used simultaneously to avoid aliasing. It achieves this by hiding the visibility of variable v throughΓ−{v|A∈{L, U}} when type-checking the body of the bind construct.

5.6 Soundness of Type System
We have proposed a small-step operational semantics instrumented with alias and size notations. We have also formulated
and proved several novel safety properties that our checking system possesses:• Alias Property: (1) All unique references are unaliased during the evaluation; (2) each unique reference can only belent once within each stack frame; and (3) R-mode fields
never change during evaluation.
• Type Preservation: Each well-typed program preserves its
type under reduction with a runtime environment and a store
which are consistent with the compile-time counterparts. The
final size property is consistent with the value obtained ontermination.
• Progress: Well-typed programs can never go wrong. It
guarantees that safety policies are met for well-typed OI MP
programs.
Details on the dynamic semantics, formal descriptions of thesoundness theorems and their proofs can be found in our technicalreport [11]. Detailed correctness proof for size analysis can also
be found in [31] in the context of a first-order functional languagewith primitive resources.

6. Related Work
Sized type was first proposed by Hughes, Pareto and Sabry [23,22] as a formal mechanism for proving the correctness of certain
size-related properties for embedded functional programs. Their
proposal captures an upper or lower bound for each data, depending on whether it is declared as data or co-data. This catered toindependent attribute analysis, rather than relational analysis. Separately, dependent type was proposed by Xi and Pfenning [36, 38]

Programs
bisortem3d
healthmst
power
treeaddtsp
perimetern-bodyVoronoiinsert(AVL)
delete(AVL)bs(array)bufferSize (lines)
Source Annotation
340
7
462
19
562
22
473
31
765
24
195
6
545
10
745
12
1128
31
1000
45
64
1
157
2
41
1
65
6

Safety Checking(seconds)
0.68
0.30
6.08
0.20
1.32
0.12
0.42
8.48
0.37
1.90
1.36
4.79
0.08
0.12

Figure 3. Performance of Verification
to capture size information and has been applied to a variety of
applications. These early works are based on the type checking
framework. Later, Chin and Khoo [10] enriched sized typing bydevising fixed-point methods for safely inferring the size relations
for functional programs. A common feature of these past works isthat they are based primarily on functional languages, and operateover mostly immutable data structures.
Recently, some advance has been achieved in extending dependent types to imperative programming through a language, called
Xanadu [37]. However, Xanadu supports only a limited set oftypes, including read-only lists; but not general objects. This restriction avoided the aliasing problem, as only size-immutable objects are effectively used. With a different research goal, Odersky
et. al. [29] designed a dependent type system for objects andclasses. However, its purpose is to model JAVA’s inner classes,
virtual types and family polymorphism, rather than tracking size
properties.
Sharing objects through aliases is both a powerful feature anda weakness of object-oriented languages [1, 7, 19]. As each object
may be updated via any alias, object being changed may not evenbe aware of it; causing such programs to be harder to understandand reason. To regain control over aliasing, various researchers
have proposed alias annotations to limit the capability of pointervariables so that local reasoning is possible. A wide range of alias
annotations have been proposed, which have been systematicallyorganised into a general capability system[1, 7]. Our work is built
on top of such alias controls. Uniqueness [27] gives unaliased reference, and is closely related to linear type systems [35, 17]. Lent
mechanism allows other annotations to be borrowed temporarily
over a program scope, where they do not escape. It is related toquasi-linearity [24]. Read-only annotation is related to immutability, and can facilitate sharing and invariants. Another well-studied
mechanism is ownership annotation in support of object encapsulation. Here, every object has an owner, whose access is limited
to the ownership tree, such that external objects have only indirectaccesses through the owner’s methods. Ownership encapsulation
has been applied to a number of applications, including regiontypes for real-time Java [4], prevention of data races and deadlocks
in concurrent programs[5, 6], and as aids to program understanding [1]. Our present proposal for sized type for objects rely ona smaller set of alias annotations, but offers a mutually beneficial
synergy. With the portfolio of size-inspired applications, we ex-pect the type system proposed here to further reinforce on the importance of alias control mechanisms; and to continue to benefit
from their advances.
Instead of confining aliasing[19], there have been a number ofattempts at analysing possible aliasing structures. Systems such as
TVLA [33], PALE [28], and Roles [25], enable the shape of local
object graphs to be analysed and captured. Most of these systems
employ heavier machinery to capture state change and to enforce
the expected aliasing structures. For example, Sagiv, Rep and Wilhelm [33] employed three-value logic to capture points-to relation
between objects as well as imperative changes on shape graph.
These proposals are complimentary to our goal of size analysis inrelational form, and may open up new classes of mutable objects
that could be precisely analysed.
In recent years, several approaches have been advocated forverifying software to ensure that it conforms to stated safety policy. One popular approach [20, 2, 12, 8] is based on the concept of model checking in which program states are approximatedthrough boolean predicates. Choosing a suitable predicate abstraction remains one of the main challenges, and various symbolic techniques have been proposed to facilitate this task. Witha different approach, several type based techniques [14, 16, 13]
have also been advocated for checking if user programs conformto some stated safety protocols. The focus has been on designing bounded typestates together with linear typing for supportingstrong updates. As an approach between the above two, Flanagan et.al.[15] use verification-condition generation and automatictheorem-proving techniques in their extended static checking system for Java. However, they incorporate a trade-off between soundness and usefulness. Moreover, most of these proposals are basedon finite state approximation of the program states, and are typically formulated in a path-insensitive manner.
Through the use of relational size analysis (with disjunctive
formulae), our proposal has the potential to give more precise verification. Furthermore, our use of alias controls and size-immutability(often omitted in other works) has provided a clearer path towards
analysing object-based imperative programs.

7. Conclusion
We have proposed an advanced type system to capture size relations for objects. We make use of size-immutability to facilitate sharing, and alias controls to identify unaliased objects. Thismechanism permits size relation in constraint form to be accurately analysed for object-based programs.
Our type system
can be viewed as a sound and decidable lightweight verification
method. We use the ADT mechanism augmented with size invariants together with pre/post conditions on methods, to allow us toexpress a variety of size-inspired safety policies - ranging fromsafe array bounds, data structure invariant to protocol verification.
We have implemented a prototype system which converts annotated Java programs (without concurrency and exceptions) to
our kernel language, before type checking is applied to verify the
specified safety policies (with a prototype system accessible at
http://loris-4.ddns.comp.nus.edu.sg/˜nguyenh2/mi). Our prototype was implemented using the Glasgow Haskell compiler. To
evaluate this prototype, we hand-annotated a set of programs fromthe Java Olden benchmark together with programs described inthis paper, before subjecting them to sized type checking. The
performance statistics (on Red Hat Linux 9.0 for Pentium 2.4 GHz

with 768MB) is summarised in Fig 3. Due to modular type checking, our system verifies each medium-sized program under 10 seconds, despite the use of Presburger constraint solving[32]. Size
and alias annotations are required for the headers of object andmethod declarations which account for less than 5% of the sourcecode. Our recent investigations into automatic inference of size
constraints for an imperative language without objects [39] (forarray bound check elimination) could further reduce the burden ofannotations.

Acknowledgments
The authors would like to thank Florin Craciun, Dana Xu, Stefan
Andrei and Martin Rinard for various pointers, and the referees of
ICSE05 for their insightful comments. This work is supported bySingapore-MIT Alliance and NUS grant R252-000-092-112.

8. REFERENCES[1] J. Aldrich, V. Kostadinov, and C. Chambers. Alias Annotation for
Program Understanding. In ACM OOPSLA, Seattle, Washington,
November 2002.
[2] T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic
Predicate Abstraction of C Programs. In ACM PLDI, June 2001.
[3] F. Benoy and A. King. Inferring argument size relationships with
CLP(R). In Logic Programming Synthesis and Transformation,
Springer-Verlag, August 1997.
[4] G. Bollella, B. Brosgol, P. Dibble, S. Furr, J. Gosling, D. Hardin,
and M. Turnbull. The Real-Time Specification for Java.
Addison-Wesley, 2000.
[5] C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe
programming: Preventing data races and deadlocks. In ACM
OOPSLA, Seattle, Washington, November 2002.
[6] C. Boyapati and M. Rinard. A parameterized type system forrace-free Java programs. In ACM OOPSLA, Tampa Bay, Florida,
October 2001.
[7] J. Boyland, J. Noble, and W. Retert. Capabilities for Sharing: A
Generalization of Uniqueness and Read-Only. In ECOOP,
Budapest, Hungary, June 2001.
[8] S. Chaki, E. M. Clarke, A. Groce, S. Jha, and H. Veith. Modular
Verification of Software Components in C. In Proceedings of theInternational Conference on Software Engineering (ICSE’03),
pages 385–395, 2003.
[9] E. C. Chan, J. Boyland, and W. L. Scherlis. Promises: Limited
Specifications for Analysis and Manipulation. In Proceedings of theInternational Conference on Software Engineering (ICSE’98),
Kyoto, Japan, April 1998.
[10] W.N. Chin and S.C. Khoo. Calculating sized types. In ACM
SIGPLAN PEPM, pages 62–72, Boston, Massachusetts, UnitedStates, January 2000.
[11] W.N. Chin, S.C. Khoo, S.C. Qin, C. Popeea, and H.H. Nguyen.
Verifying Safety Policies with Size Properties and Alias Controls.
Technical report, SoC, Natl Univ. of Singapore, August 2004. avail.
at http://www.comp.nus.edu.sg/∼ qinsc/papers/safety.ps.gz.
[12] J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu,
Robby, and H. Zheng. Bandera: extracting finite-state models fromJava source code. In Proceedings of the International Conference
on Software Engineering (ICSE’00), pages 439–448, Limerick,Ireland, June 2000.
[13] R. DeLine and M. Fahndrich. Typestates for Objects. In ECOOP,
Oslo, Norway, June 2004.
[14] M. Fahndrich and R. DeLine. Adoption and Focus: Practical linear
types for imperative programming. In ACM PLDI, June 2002.

[15] C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe,and R. Stata. Extended Static Checking for Java. In ACM PLDI,
Berlin, Germany, June 2002.
[16] J.S. Foster, T. Terauchi, and A. Aiken. Flow-Sensitive Type
Qualifiers. In ACM PLDI, Berlin, Germany, June 2002.
[17] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102,
1987.
[18] B. Grobauer. Cost Recurrences for DML Programs. In Proceedingsof the International Conference on Functional Programming (ICFP’01), pages 253–277, Florence, Italy, September 2001.
[19] C. Grothoff, J. Palsberg, and J. Vitek. Encapsulating Objects with
Confined Types. In ACM OOPSLA, October 2001.
[20] T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy
Abstraction. In ACM POPL, pages 58–70, Portland, Oregon,
January 2002.
[21] M. Hofmann and S. Jost. Static Prediction of Heap Space Usage forFirst Order Functional Programs. In ACM POPL, New Orleans,Louisiana, January 2003.
[22] J. Hughes and L. Pareto. Recursion and Dynamic Data-Structures inBounded Space: Towards Embedded ML Programming. In
Proceedings of the International Conference on Functional
Programming (ICFP ’99), September 1999.
[23] J. Hughes, L. Pareto, and A. Sabry. Proving the Correctness ofReactive Systems Using Sized Types. In ACM POPL, pages
410–423. ACM Press, January 1996.
[24] N. Kobayashi. Quasi-linear types. In ACM POPL, pages 29–42.
ACM Press, 1999.
[25] V. Kuncak, P. Lam, and M. Rinard. Role analysis. In ACM POPL,
Portland, Oregon, January 2002.
[26] C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change
principle for program termination. In ACM POPL, pages 81–92.
ACM Press, 2001.
[27] N. Minsky. Towards alias-free pointers. In ECOOP, July 1996.
[28] A. Moeller and M. I. Schwartzbach. The Pointer Assertion LogicEngine. In ACM PLDI, June 2001.
[29] M. Odersky, V. Cremet, C. Röckl, and M. Zenger. A Nominal
Theory of Objects with Dependent Types. In ECOOP, Springer
LNCS, July 2003.
[30] B. C. Pierce. Intersection types and bounded polymorphism.
Mathematical Structures in Computer Science, 7(2):129–193, 1997.
[31] C. Popeea and W.N. Chin. A Type System for Resource Protocol
Verification and its Correctness Proof. In ACM SIGPLAN PEPM,
Verona, Italy, August 2004.
[32] W. Pugh. The Omega Test: A fast practical integer programmingalgorithm for dependence analysis. Communications of the ACM,
8:102–114, 1992.
[33] M. Sagiv, T. Reps, and R. Wilhelm. Parametric Shape Analysis via
3-valued Logic. In ACM POPL, January 1999.
[34] K. Sohn and A. Van Gelder. Termination detection in logic
programs using argument sizes (extended abstract). In Proceedingsof the 10th ACM Symposium on Principles of Database Systems,
pages 216–226, 1991.
[35] P. Wadler. Linear types can change the world! In M. Broy and C.
Jones, editors, Programming Concepts and Methods. North
Holland, Amsterdam, April 1990.
[36] H. Xi. Dependent Types in Practical Programming. PhD thesis,
Carnegie Mellon University, 1998.
[37] H. Xi. Imperative Programming with Dependent Types. In
Proceedings of 15th Symposium on Logic in Computer Science(LICS ’00), Santa Barbara, June 2000.
[38] H. Xi and F. Pfenning. Eliminating array bound checking throughdependent types. In ACM PLDI, pages 249–257. ACM Press, June
1998.
[39] D.N. Xu, C. Popeea, S.C. Khoo, and W.N. Chin. Scalable andPrecise Inference for Array Checks Elimination. Technical report,
SoC, Natl Univ. of Singapore, November 2004. avail. at
http://www.comp.nus.edu.sg/∼ chinwn/publ.html.