Verification of
object-oriented programs
with invariants
by M. Barnett, R. DeLine, M. Fähndrich, K.R.M. Leino, W. Schulte
Bordignon Claudio
Zampieron Elisa
Introduzione

Scopo: fornire una metodologia di
programmazione che sfrutta gli invarianti

La metodologia




utilizza il design-by-contract
determina in quale stato un oggetto può essere
modificato;
permette l’object-composition e il subclassing;
estesa per permette il multithreading;
Introduzione: Design-By-Contract

Il Design By Contract (DBC) è una metodologia inventato da Betrand
Meyer e integrata in Eiffel

Consiste nel considerare un'interfaccia (insieme dei metodi esposti da una
classe) come un contratto fra chi la invoca (client) e chi la implementa
(classe)

Vengono quindi definiti i termini del contratto utilizzando 4 elementi:

Pre-condizioni: i requisiti minimi che devono essere soddisfatti dal
cliente affinché il metodo possa andare a buon fine

Post-condizioni: i requisiti per cui l’esecuzione del metodo si può
ritenere corretta e che il metodo si impegna quindi a rispettare

Clausule di modifica: una lista dei campi della classe che vengono
modificati dall’implementazione del metodo

Invarianti: condizioni che devono essere sempre valide.
I termini del contratto


Le pre e post-condizioni riguardano quindi un metodo:
 le pre-condizioni vincolano il chiamante
 le post-condizioni vincolano il metodo
Gli invarianti sono invece un vincolo a livello dell’intera classe:
 devono valere



prima che una qualunque invocazione di metodo avvenga
e alla fine dell’esecuzione del metodo stesso
possono non essere validi temporaneamente durante
l’esecuzione di un metodo
Esempio
class SquareRootable feature
value: Real;
sqrt is
require
value
do
value
ensure
value
value
end;
>= 0;
:= ....;
>= 0;
<= old value;
invariant
value >= 0;
end ;
Pre-condizione: un'espressione boolean
valutata prima del codice di un metodo;
è introdotta a mezzo della parola chiave
require e può comporsi di una o più
espressioni boolean separate da ‘;’
Post-condizione: un'espressione boolean
valutata al termine di un metodo;
è introdotta a mezzo della parola chiave
ensure
Invariante di classe: è una condizione che,
ogni volta che viene valutata, deve valere
true;
è introdotta a mezzo della parola chiave
invariant
Invarianti…
Spesso vengono usati come sostitutivi di pre e post-condizioni:

class C{
private int x, y;
invariant 0  x < y;
public C(){
x = 0; y = 1;
}
public void M()
modifies x, y {
assert y – x  0;
L’invariante è soddisfatto prima dell’incremento di x
Stato dell’oggetto CONSISTENTE
L’invariante potrebbe non valere
Stato dell’oggetto INCONSISTENTE
x = x + 3;
y = 4 * y;
}
L’invariante è ristabilito dopo l’assegnamento di y
Torniamo ad uno stato CONSISTENTE
}

Quindi non sono necessarie pre e post-condizioni ?
E se il metodo invoca P()?
class C{
private int x, y;
invariant 0  x < y;
public C(){
x = 0; y = 1;
}
public void M()
modifies x, y {
assert y – x  0;
x = x + 3;
P();
L’invariante deve essere soddisfatta
all’uscita del costrutture
Si assume che l’invariante sia soddisfatta
all’entrata del metodo
Qui l’invariante potrebbe non valere
temporaneamente
Cosa succede se P() esegue
una chiamata ricorsiva?
y = 4 * y;
}
public P() {
/*…*/;
M();
}
}
L’invariante è qui ripristinata
L’invariante deve essere valida
all’uscita dal metodo
Specifichiamo i dettagli del
contratto
class C{
private int x, y;
invariant 0  x < y;
Il metodo P() invoca M(), quindi
deve garantire le precondizioni.
public C()
ensures 0  x < y; {
x = 0; y = 1;
}
public M()
requires 0  x < y;
modifies x, y
ensures 0  x < y {
assert y – x  0;
x = x + 3;
P();
Y = 4 * y;
}
public P() {
/*…*/
M();
}
}
Esprimere l’invariante
come pre e post condizione
viola l’information-hiding
La metodologia quindi dovrà:


specificare SE L’INVARIANTE E’
SODDISFATTO
RISPETTARE L’INFORMATION
HIDING
Validità dell’invariante 1/2

Introduciamo un campo speciale st:{Invalid, Valid}




compare solo nelle pre e post-condizioni;
non può essere modificato nel corpo dei metodi ma
solo dai comandi pack e unpack;
Definiamo il predicato InvT(o)  l’oggetto o di tipo
T soddisfa gli invarianti della classe T
Vogliamo che, in ogni punto del programma, valga:
 ( o : T | o.st = Invalid  InvT(o))
Validità dell’invariante 2/2

o.st = Invalid  l’oggetto o è invalido




l’invariante potrebbe non essere soddisfatto
i campi dell’oggetto possono essere modificati
un oggetto viene allocato inizialmente nello stato invalid
o.st = Valid  l’oggetto o è valido


l’invariante è soddisfatto
l’oggetto non è modificabile
pack o 
assert o  null
assert InvT(o);
o.st := Valid;

assert o.st = Invalid;
unpack o 
assert o  null  assert o.st = Valid;
o.st := Invalid;
Esempio
class C{
private int x, y;
invariant 0  x < y;
public C()
ensures st = Valid; {
x = 0; y = 1;
pack this;
}
public M()
requires st = Valid;
modifies x, y;
{
assert y – x  0;
unpack this;
x = x + 3;
Y = 4 * y;
pack this;
}
}
All’uscita dal costruttore l’oggetto deve
essere valido, questo è garantito dal
comando pack
La pre-condizione indica che
l’oggetto deve essere valido a
tempo di invocazione.
Il comando pack mi garantisce la
validità in uscita
Estensione object-composition

Problema
 l’invariante potrebbe dipendere dai componenti
quindi l’aggiornamento dei campi può portare a
invalidità
 information hiding

Introduciamo un modificatore rep

Nuovo range {Valid, Invalid, Committed} per st

Ridefiniamo le operazioni pack e unpack

Istanziamo nuovi oggetti con stato invalid
Object-composition: Pack / Unpack

pack

controlla l’invariante e imposta il campo st dei componenti allo
stato committed e varia o.st allo stato di valid
pack o  assert o  null  assert o.st = Invalid;
assert InvT(o);
foreach p є CompT(o) { assert(p = null  p.st = Valid)};
foreach p є CompT(o) { if(p
o.st := Valid;


null) p.st := Committed};
unpack

modifica il campo o.st dell’oggetto e delle sue componenti
rispettivamente allo stato invalid e valid
unpack o 
assert o  null  assert o.st = Valid;
o.st := Invalid;
foreach p є CompT(o) { if(p

null) {p.st := Valid}};
Object-composition

Se T ha due campi rep, per esempio, x e y e o è di tipo T, allora:
pack o 
assert o  null
assert InvT(o);

assert (o.x = null
if(o.x


o.st = Invalid;

o.x.st = Valid)

(o.y = null

o.y.st = Valid);
null) { o.x.st := Committed };
if(o.y
null) { o.y.st := Committed };
o.st := Valid;

Vogliamo che, in ogni punto del programma, valga:

( o : T |
o.st = Invalid  InvT(o) 
( p є CompT(o)  p = null  p.st = Committed))
Esempio 1/3
class E {
method m2(s)
requires s.st=Valid …
class C {
Committed
method m0(k)
requires k.st=Valid …
{
Committed
D
unpack k ;
Committed
Committed
k.d.m1() ;
k.s.m2() ;
pack k;
E
s
d
Committed
}
k
C
Valid
Esempio 2/3
class E {
method m2(s)
requires s.st=Valid …
class C {
method m0(k)
requires k.st=Valid …
{
unpack k ;
k.d.m1() ;
k.s.m2() ;
pack k;
s
d
}
k
C
Invalid
Committed
Committed
Committed
D
Valid
E
Valid
Esempio 3/3
class E {
method m2(s)
requires s.st=Valid …
class C {
Committed
method m0(k)
requires k.st=Valid …
{
Committed
D
unpack k ;
Committed
Committed
k.d.m1() ;
k.s.m2() ;
pack k;
E
s
d
Committed
}
k
C
Valid
Estensione per Subclasses 1/2



I campi sono ereditati dai vari class frames
Ciascun frame contiene nuovi campi
L’oggetto può essere valid/invalid per ciascun class frame
Dato un oggetto o:W
W
o puo’ essere invalido per K e W
K
T
L’oggetto o puo’ essere valido per T
Y
U
Object
Se o è valido per T non puo’ essere
invalido per Y!!!
Estensione per Subclasses 2/2

Ridefiniamo st con due campi speciali
 inv (l’ultima classe per la quale sono soddisfatti gli invarianti)
 committed (boolean: indica se l’oggetto è committed;
true se inv = tipo dinamico dell’oggetto)

Ridefiniamo i comandi pack e unpack:
pack o as T 
assert o  null  o.inv = Superclasse(T);
assert InvT(o);
foreach p є CompT(o){assert(p = null  p.inv = type(p)  p.committed)}
foreach p є CompT(o) { if(p != null) p.committed := true};
o.inv := T;
unpack o from T 
assert o  null  o.inv = T  o.committed;
o.inv := Superclasse(T);
foreach p є CompT(o) { if(p != null) p.committed := false};
Esempio Class Frames

Il tipo dinamico C ha 4 class frames

Aggiorniamo il campo c.y:

pack o as C
 controlla l’invariante
 per ciascun componente p,
setta p.committed = true
 setta o.inv = C

unpack o from C
 setta o.inv = B
 per ciascun componente p,
setta p.commited = false
class C extends B
y:Y
invariant u, v, x, y
class B extends A
x:X
invariant u, v, x
class A extends object
u:U, v:V
invariant u, v
object
/* inv == C */
unpack c from B
/* inv == B */
c.y = 5;
pack this as C
/* inv == C */
Correttezza
La correttezza della metodologia è dimostrata dalle seguenti
condizioni che valgono in tutto il programma

1.
2.
3.
4.
( o,T • o.committed  o.inv = type(o) )
( o,T • o.inv <: T  InvT (o) )
( o,T • o.inv <: T )  ( p  CompT (o) • p = null  p.committed ))
( o,T, o’,T’, q • ( p  CompT (o), p’  CompT’(o’) • o.inv <: T  o’.inv <:
T’  q.committed  p = p’ = q  o = o’  T = T’ ))
Dimostriamo che questi 4 condizioni sono mantenute da ogni
comandi che possono modificare i valori dei campi





Costruttore
Comando pack
Comando unpack
Aggiornamento dei campi
Correttezza del costruttore
(3) ( o,T • o.inv <: T )  ( p  CompT (o) • p = null  p.committed ))
(4) ( o,T, o’,T’, q(1)
• ((
p o,T

Comp

Comp
• o.inv) <: T  o’.inv <: T’
(2)
(
o,T
••o.committed
o.inv
<: p’
T
Inv
o.inv
=) type(o)
T (o),
T’(o’)
T (o)
 q.committed  p = p’ = q  o = o’  T = T’ ))
La (1) è soddisfatta perché per definizione il costruttore setta il campo
committed a false per ogni nuovo oggetto allocato



Il costruttore setta o.inv a object e questo dimostra la (2)
La (3) e la (4) sono verificate in quanto il tipo object non ha rep-fields
Correttezza del comando pack
pack o as T 
assert o  null  o.inv = Superclasse(T);
assert InvT(o);
foreach p є CompT(o){assert(p = null  p.inv = type(p)  p.committed)}
foreach p є CompT(o) { if(p != null) p.committed := true};
o.inv := T;
(4) ( o,T, o’,T’, q • ( p  CompT (o), p’  CompT’(o’) • o.inv <: T  o’.inv <: T’  q.committed
(3) ( o,T • o.inv <:
T(

(
po.inv
 Comp
(o)
• p (o)
==
null
 p.committed
))
(2)
()
o,T
••o.committed
<: S T
Inv
o.inv
) type(o)
)
S
 p = p’ = q  o = o’  T(1)
= T’
))o,T
Ogni componente (in cui modifichiamo lo stato) è valida quindi viene
soddisfatta la (1)

Sia T<:S. l’asserzione precedente alla verifica degli invarianti garantisce
che portando o.inv da T a S venga soddisfatta la (2)


Porre allo stato committed solo gli oggetti non nulli soddisfa la (3)

Possiamo dimostrare che pack rispetta la (4) analizzando i due casi
 q.committed è false la premessa è falsa => implicazione vera
 se la premessa è verificata, per come è definito il comando pack o e
o’ sono lo stesso oggetto
Correttezza del comando unpack
unpack o from T 
assert o  null  o.inv = T  o.committed;
o.inv := Superclasse(T);
foreach p є CompT(o) { if(p != null) p.committed := false};
(4) (3)
((o,T,
o’,T’,
q(1)
• <:
((
p o,T
p’
T
Comp
(o’)
• o.inv
 o,T
• o.inv
(2)
(T
)
o,T
Comp
•(•o.committed
o.inv
pT(o),
<:
Comp
T
(o)
Inv
o.inv
•T p(o)
=)null
type(o)
 p.committed
) <: T  o’.inv
)) <: T’
T’=
 q.committed  p = p’ = q  o = o’  T = T’ ))
La (1) è soddisfatta perché il comando cambia solo il valore di oggetti
non committed


La (2) è soddisfatta perché il comando indebolisce il predicato
La (3) è soddisfatta perché il foreach modifica solo le componenti di p e
l’assegnamento a o.inv antecedente il ciclo falsifica le premesse del
predicato => l’implicazione è vera


La (4) è soddisfatta perché il comando indebolisce il predicato
Correttezza nell’aggiornamento
dei campi
(2) ( o,T • o.inv <: T  InvT (o) )
(1) ( o,T • o.committed  o.inv = type(o) )
(3) ( o,T • o.inv <: T )  ( p  CompT (o) • p = null  p.committed ))
(4) ( o,T, o’,T’, q • ( p  CompT (o), p’  CompT’(o’) • o.inv <: T  o’.inv <: T’
 q.committed  p = p’ = q  o = o’  T = T’ ))
I comandi di aggiornamento non possono modificare i valori di inv e
committed, questo mantiene la (1)

Le precondizioni per l’aggiornamento dei campi (dato x:T implica che
(x.inv <: T) ) fanno fallire le premesse di (2) (3) e (4), per la semantica
dell’implicazione quindi queste sono verificate

Estensione per il Multithreaded

Lo scopo è sviluppare una tecnica per la
verifica della consistenza degli oggetti su un
programma OO multithreaded.

Formalizziamo lo stato consistente di un
oggetto attraverso l’uso degli invarianti.

In un linguaggio Multithreaded l’interleaving
può causare la violazione degli invarianti e
quindi inconsistenza.
Esempio
class Account {
int balance;
}
L’interleavings tra due tread
concorrenti possono portare
violazioni dell’invariante
Account act = …;
int b0 = act.balance;
act.balance += 50;
int b1 = act.balance;
Non è garantito che
b1 == b0 + 50

Introduce
 Mutua esclusione
 Aggregate objects
 Object invariants
Mutua esclusione

In ciascun oggetto, si introduce un campo owner che può essere



Null se l’oggetto o non è componente di nessun altro oggetto
Object se l’oggetto o è una componente
Thread se l’oggetto o è posseduto da un thread

Prima che il thread t acceda al campo o.f, si controlla che o.owner == t

Quando il thread t crea un oggetto o, setta o.owner = t;

Il campo owner può essere modificato solo dai comandi:

acquire o;
attende finchè o.owner == null e poi setta o.owner = t;

release o;
controlla che o.owner == t e poi setta o.owner = null;
Esempio
class Account { int balance; }
Account act = new Account();
act.balance = 5;
release act;
…
acquire act;
act.balance++;
release act;
Aggregate objects





Gli aggregate objects vengono trattati come se fossero una unica
entità
Manteniamo modificatore rep
Un thread può modificare un aggregate object tramite comando
unpack
Il comando pack trasferisce le proprietà ritornandole
all’aggregate object
Introduciamo in ciascun oggetto un campo boolean inv che indica
quando l’oggetto è stato modificato
 il campo inv è settato dal comando pack e ripristinato dal
comando unpack
 finchè !inv, i modificatori rep sono vuoti
Aggregate objects
[[ o = new
o = new
o.owner
o.inv =
C; ]] 
C;
= t;
false;
[[ x = o.f; ]] 
assert o.owner == t;
x = o.f;
[[ o.f = x; ]] 
assert o.owner == t;
assert !o.inv;
o.f = x;
[[ acquire o; ]] 
lock (o) {
while (o.owner != null)
Monitor.Wait(o);
o.owner = t;
}
[[ release o; ]] 
assert o.owner == t;
assert o.inv;
lock (o) {
o.owner = null;
Monitor.Pulse(o); //(*)
}
Aggregate objects
[[ pack o; ]] 
assert o.owner == t;
assert !o.inv;
for each rep field o.f:
if (o.f != null) {
assert o.f.owner == t;
assert o.f.inv;
}
for each rep field o.f:
if (o.f != null)
o.f.owner = o;
o.inv = true;
[[ unpack o; ]] 
assert o.owner == t;
assert o.inv;
for each rep field o.f:
if (o.f != null)
o.f.owner = t;
o.inv = false;
Ciclo di vita di un oggetto
il thread t crea
l’oggetto o
modificato dal
thread t
o.Owned = “null”
o è free e
o.Owned = “thread”
o è mutable
consistente
thread t esegue
pack o
thread t esegue
unpack o
o.Owned = “object”
o è consistente e
thread t esegue pack
object p e p.f = o e f è
un campo rep
“sigillato”
thread t esegue
unpack owner p
acquire dal
tread t
o.Owned = “thread”
o è consistente
release dal
thread t
Esempio 1/7
Thread 1
class Agg { rep Rep f; }
class Rep {}
Agg a = new Agg;
Rep r = new Rep;
pack r;
a.f = r;
pack a;
release a;
Esempio 2/7
Thread 1
a
class Agg { rep Rep f; }
class Rep {}
Agg a = new Agg;
Rep r = new Rep;
pack r;
a.f = r;
pack a;
release a;
Esempio 3/7
Thread 1
a
r
class Agg { rep Rep f; }
class Rep {}
Agg a = new Agg;
Rep r = new Rep;
pack r;
a.f = r;
pack a;
release a;
Esempio 4/7
Thread 1
a
r
class Agg { rep Rep f; }
class Rep {}
Agg a = new Agg;
Rep r = new Rep;
pack r;
a.f = r;
pack a;
release a;
Esempio 5/7
Thread 1
a
r
class Agg { rep Rep f; }
class Rep {}
Agg a = new Agg;
Rep r = new Rep;
pack r;
a.f = r;
pack a;
release a;
Esempio 6/7
Thread 1
a
r
class Agg { rep Rep f; }
class Rep {}
Agg a = new Agg;
Rep r = new Rep;
pack r;
a.f = r;
pack a;
release a;
Esempio 7/7
Thread 1
class Agg { rep Rep f; }
class Rep {}
a
r
Agg a = new Agg;
Rep r = new Rep;
pack r;
a.f = r;
pack a;
release a;
Object Invariants




Ciascuna classe può dichiarare un invariante
L’invariante può menzionare solo campi this.f1.f2.….fn.g
dove f1, f2, …, fn sono campi rep
Il comando pack controlla l’invariante:
di conseguenza, l’invariante vale quando inv è true
Il comando release controlla inv
di conseguenza, aggregates liberi soddisfano i loro
invarianti
Related Work



idiomi valid in ESC/Modula-3
dichiarazione di invariant in ESC/Java e JML
Spec# assicura che l’accesso dei campi avviene
tramite operazioni thread-local




supporta aggregate objects
gli invarianti sono rispettati
applicazione completamente dinamica
utilizza operazioni acquire e release
Conclusioni







Invarianti differenti dalle pre/post-conditions
Program invariants mantenuti in ogni punto di
programma
Uso di comandi pack / unpack
I campi possono essere liberamente letti
(vincoli solo per aggiornamento di campi)
Estensione per il multhitreaded
Supporto per aggregate objects
Correttezza
Riferimenti
Wolfram Schulte
Mike Barnett
Robert DeLine
Manuel Fähndrich
K. Rustan M. Leino

Verification of object-oriented programs with invariants
Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino,
Wolfram Schulte
Microsoft Research, Redmond, WA, USA

Journal of Object Technology (http://www.jot.fm)

Verification of multithreaded object-oriented programs with
invariants
Bart Jacobs (Dept. of Computer Science Katholieke Universiteit Leuven),
K. Rustan M. Leino, Wolfram Schulte (Microsoft Research, Redmond, WA,
USA)
 Modular verification of global module invariants in OO programs
K. Rustan M. Leino and Peter Müller
Technical Report 459, ETH Zürich, 2004