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 isrequire

value >= 0;do

value := ....;ensure

value >= 0;value <= old value;

end;

invariantvalue >= 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:

Quindi non sono necessarie 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;

x = x + 3;

y = 4 * y; }}

L’invariante è soddisfatto prima dell’incremento di xStato dell’oggetto CONSISTENTE

L’invariante potrebbe non valereStato dell’oggetto INCONSISTENTE

L’invariante è ristabilito dopo l’assegnamento di y Torniamo ad uno stato CONSISTENTE

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();

y = 4 * y; }

public P() {/*…*/;M();

}}

Si assume che l’invariante sia soddisfattaall’entrata del metodo

Qui l’invariante potrebbe non valeretemporaneamente

L’invariante deve essere validaall’uscita dal metodo

Cosa succede se P() esegue una chiamata ricorsiva?

L’invariante deve essere soddisfatta all’uscita del costrutture

L’invariante è qui ripristinata

Specifichiamo i dettagli del contratto

class C{ private int x, y; invariant 0 x < y;

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(); }}

Il metodo P() invoca M(), quindi deve garantire le precondizioni.

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 o.st = Invalid;assert InvT(o);o.st := Valid;

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

unpack modifica il campo o.st dell’oggetto e delle sue

componenti rispettivamente allo stato invalid e 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 null) p.st := Committed}; o.st := 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:

Vogliamo che, in ogni punto del programma, valga: ( o : T |

o.st = Invalid InvT(o) ( p є CompT(o) p = null p.st =

Committed))

pack o assert o null o.st = Invalid; assert InvT(o);

assert (o.x = null o.x.st = Valid) (o.y = null o.y.st = Valid); if(o.x null) { o.x.st := Committed };

if(o.y null) { o.y.st := Committed }; o.st := Valid;

Esempio 1/3

class C {method m0(k)

requires k.st=Valid …{

unpack k ;k.d.m1() ;k.s.m2() ;pack k;

}

class E {method m2(s) requires s.st=Valid …

sd

Ck

E

D

Valid

Committed

Committed

Committed

CommittedCommitted

Esempio 2/3

class C {method m0(k)

requires k.st=Valid …{

unpack k ;k.d.m1() ;k.s.m2() ;pack k;

}

class E {method m2(s) requires s.st=Valid …

sd

Ck

E

D

Invalid

Valid

Valid

Committed

CommittedCommitted

Esempio 3/3

class C {method m0(k)

requires k.st=Valid …{

unpack k ;k.d.m1() ;k.s.m2() ;pack k;

}

class E {method m2(s) requires s.st=Valid …

sd

Ck

E

D

Valid

Committed

Committed

Committed

CommittedCommitted

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

Object

U

Y

T

K

W

Dato un oggetto o:W

o puo’ essere invalido per K e W

L’oggetto o puo’ essere valido per T

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

class C extends By:Y

invariant u, v, x, y

class B extends Ax:X

invariant u, v, x

class A extends objectu:U, v:V

invariant u, v

object

Il tipo dinamico C ha 4 class frames

Aggiorniamo il campo c.y:

/* inv == C */unpack c from B/* inv == B */

c.y = 5;pack this as C

/* inv == C */

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

Correttezza

La correttezza della metodologia è dimostrata dalle seguenti condizioni che valgono in tutto il programma

1. ( o,T • o.committed o.inv = type(o) )

2. ( o,T • o.inv <: T InvT (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’ ))

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

(1) ( o,T • o.committed o.inv = type(o) )(2) ( o,T • o.inv <: T InvT (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’ ))

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;

Ogni componente (in cui modifichiamo lo stato) è valida quindi viene soddisfatta la (1)

(1) ( o,T • o.committed o.inv = type(o) )

Sia T<:S. l’asserzione precedente alla verifica degli invarianti garantisce che portando o.inv da T a S venga soddisfatta la (2)

(2) ( o,T • o.inv <: S InvS (o) )

Porre allo stato committed solo gli oggetti non nulli soddisfa la (3)

(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’ ))

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

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

(1) ( o,T • o.committed o.inv = type(o) )(2) ( o,T • o.inv <: T InvT (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’ ))

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};

La (4) è soddisfatta perché il comando indebolisce il predicato

Correttezza nell’aggiornamento dei campi

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

(1) ( o,T • o.committed o.inv = type(o) )

(2) ( o,T • o.inv <: T InvT (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’ ))

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;

}

Account act = …;int b0 = act.balance;act.balance += 50;int b1 = act.balance;

L’interleavings tra due treadconcorrenti possono portare

violazioni dell’invariante

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 C; ]] o = new C;o.owner = t;o.inv = 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;

il thread t crea l’oggetto o

modificato dal thread t

Ciclo di vita di un oggetto

o.Owned = “thread”

o è mutable

o.Owned = “thread”

o è consistente

o.Owned = “null”o è free e

consistente

o.Owned = “object”

o è consistente e “sigillato”

thread t esegue pack o

acquire dal tread t

release dal thread t

thread t esegue unpack o

thread t esegue unpack owner p

thread t esegue pack object p e p.f = o e f è

un campo rep

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

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;

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

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

K. Rustan M. Leino

Mike Barnett

Robert DeLine

Manuel Fähndrich

Wolfram Schulte