Apresentacao JML

Flickr em JML

Pedro Pereira Ulisses Costa

Metodos Formais em Engenharia de Software

18 de Dezembro de 2008

Pedro Pereira, Ulisses Costa Flickr em JML

Sumario

1 JMLO que e?Direitos e DeveresIsolamento e ajuda no debuggingLinguagem formal e abstracta

2 ESC/Java2

3 JMLUnit

4 Alloy Revisitado

5 De Alloy para JAVA e JML


Sumario


2 ESC/Java2

3 JMLUnit

4 Alloy Revisitado



Java


Java + JML


Sumario


2 ESC/Java2

3 JMLUnit

4 Alloy Revisitado



Design by contract

Contracto entre classe e clientes

Classe explicıta os direitos e deveres

Cliente cumpre os deveres

Classe atribui direitos


JML melhora o codigo

JML sao anotacoes verificadas no programa

Anotacoes sao puras

Pode ajudar no debugging

Isola os erros evitando propagacao


Especificacao em JML

O JML e melhor que JAVAdoc (linguagem natural vslinguagem formal)

JML e mais abstracto que codigo

Nao e necessario dar o algoritmo detalhado

Racioncınio modular

Compreensao mais rapida dos metodosNo pior caso basta ler os contractos dependentes do metodoO cliente nao pode concluir mais nada para alem doscontractos


Sumario


2 ESC/Java2

3 JMLUnit

4 Alloy Revisitado



Estados do JML

76 5401 23normal post state

76 5401 23pre state

normal behaviour 44

throwing de excepcao

%%

76 5401 23exceptional post state

/. -,() *+excepcao

exceptional behaviour

33

java.lang .Error

''/. -,() *+fora do alcance


Isolamento e ajuda no debugging

...

/*@

@ public normal_behaviour

@ requires unameA != null && unameB != null;

@ requires m_users.containsKey(unameA) && m_users.containsKey(unameB);

@ requires m_users.get(unameA) instanceof User;

@ ensures ((User) m_users.get(unameA)).getContacts ().contains(unameB);

@ assignable m_users;

@ also

@ public exceptional_behaviour

@ requires unameA == null || unameB == null;

@ signals_only NullPointerException;

@ signals (NullPointerException) true;

@ assignable \nothing;

@*/

public void add_contact(String unameA , String unameB)

throws NullPointerException {

User u = (User) users.get(unameA );

Vector contacts = u.getContacts ();

if( !contacts.contains(unameB) ) {

contacts.add(unameB );

u.setContacts(contacts );

users.put(unameA , u);

}

}

...


Quando a pre-condicao falha

Exception in thread main org.jmlspecs.jmlrac.runtime.JMLInternalPreconditionError: by method Flickr.add contact

Flickr.java

...

/*@


@ requires unameA != null;

@ requires unameB != null;

@ requires m_users.containsKey(unameA);

@ requires m_users.containsKey(unameB);

@ requires m_users.get(unameA) instanceof User;

@ ...

@*/

public void add_contact

(String unameA , String unameB)


User u = (User) users.get(unameA );

...

}

...

Main.java (Culpado)

...

Flick f = new Flickr ();

...

f.add_contact("Pedro","Ulisses");

...

Utilizadores nao estao registados no Flickr

O objecto com esse nome nao e instancia de User

NOTA: verificacao com instanceof nao seria necessaria em JAVA5Pedro Pereira, Ulisses Costa Flickr em JML

Quando a pos-condicao falha

Exception in thread ”main” org.jmlspecs.jmlrac.runtime.JMLInternalNormalPostconditionError: by method

Flickr.add contact

Flickr.java (Culpado)

...

/*@


@ ...

@ ensures ((User) m_users.get(unameA))

@ .getContacts ()

@ .contains(unameB);


@*/

public void add_contact

(String unameA , String unameB)


...

}

...

Main.java

...

Flick f = new Flickr ();

...

f.add_contact("Pedro","Ulisses");

...

Metodo add contact ou nos metodos que este usa


Quando a pos-condicao falha

Quando o erro e de outros metodos

Exception in thread "main" org.jmlspecs.jmlrac.runtime.

JMLInternalNormalPostconditionError: by method User.setContacts

...

at Flickr.internal$add_contact(Flickr.java :246)

...

at Main.internal$main(Main.java :17)

...

Flickr.java

...

/*@


@ ...

@ ensures m_files.containsKey(mname);

@ (*^linha 246*)

@ ...

@*/

public void add_media

(String uname , String mname)


...

}

...

O JML aqui tenta ser preciso em vao.

User.java (Culpado)

...

/*@ public normal_behaviour

@ requires contacts != null;

@ ensures m_contacts.equals(contacts);

@ assignable m_contacts;

@ also


@ requires contacts == null;




@*/

public void setContacts(Vector contacts) {

this.contacts = new Vector ();

}

...


Sumario


2 ESC/Java2

3 JMLUnit

4 Alloy Revisitado



Linguagem natural vs Linguagem formal


Mais abstracto que codigo

Especificacao do metodo del user


@ requires uname != null;

@ requires m_users.containsKey(uname);

@ ensures !m_users.containsKey(uname);

@ assignable m_users , m_files , m_groups;

@ also


@ requires uname == null;




@*/

Nao e necessario dar o algoritmo detalhado

O contracto mantem-se, o cliente nunca e afectado

O contracto e muitas das vezes mais pequeno que o codigo


Linguagem formal e abstracta

public void del_user(String uname) throws NullPointerException {

User u = (User) users.get(uname );

for( Iterator i = users.values (). iterator (); i.hasNext (); ) {

User u_temp = (User) i.next ();

Vector contacts = u_temp.getContacts ();

Vector favourites = u_temp.getFavourites ();

if( contacts.remove(uname) || favourites.removeAll(u_temp.getPStream ()) ) {

u_temp.setContacts(contacts );

u_temp.setFavourites(favourites );

users.put(u_temp.getUname(), u_temp );

}

}

for( Iterator i = u.getPStream (). iterator (); i.hasNext (); )

files.remove(i.next ());

for( Iterator i = groups.values (). iterator (); i.hasNext (); ) {

Group g_temp = (Group) i.next ();

Vector members = g_temp.getMembers ();

Vector pool = g_temp.getPool ();

if( members.remove(uname) || pool.removeAll(u.getPublics ()) ) {

g_temp.setMembers(members );

g_temp.setPool(pool);

groups.put(g_temp.getGname(), g_temp );

}

}

users.remove(uname);

}


Sumario


2 ESC/Java2

3 JMLUnit

4 Alloy Revisitado



ESC/Java2

Validacao dos tipos de dados e sıntax

Detecta:

referencias para apontadores nuloscasts ilegaisindexacao de arrays fora dos limites


ESC/Java2

Nao suporta todas as especificacoes JML

Pode indicar falsos negativos/positivos


Sumario


2 ESC/Java2

3 JMLUnit

4 Alloy Revisitado



JMLUnit

Gera Test Cases para metodos

Usa pre-condicoes para filtar input

Usa invariantes/pos-condicoes para capturar as falhas dostestes


JMLUnit

Apenas tinhamos excepcoes NullPointerException

...

return new java.lang.String [] {

"ulisses", "pedro", ...

}

...

switch(n) {

case 0: return new User("pedro");

case 1: return new User("ulisses");

...

}

...


Sumario


2 ESC/Java2

3 JMLUnit

4 Alloy Revisitado



Propriedades de uma HashTable?

all u : f.users[Uname] | lone f.users.u

all n : f.users.User | lone f.users[n]


O que e uma HashTable?

cada objecto esta associado a uma imagem e vice-versa;

nao existem objectos ou imagens repetidas.


Injectividade e Simplicidade

injectividade a mesma imagem nao pode relacionar dois objectosdiferentes

simplicidade o mesmo objecto nao pode relacionar duas imagensdiferentes


Sobrejectividade e Totalidade

sobrejectividade cada imagem esta relacionada com pelo menosum objecto

totalidade cada objecto esta relacionado com pelo menos umaimagem


Refinamento

// media associado ao pstream tem de existir

all u : f.users[Uname] | u.pstream in f.files.Media

// nao ha media "solto"

f.files.Media in f.users[Uname ]. pstream

// media associado ao user e unico

all u : f.users.User | no f.users[u]. pstream & f.users[Uname - u]. pstream


Relacao comments

pred comments_inj_sur_ent [ f : Flickr ] {

// comments injectiva

all x, y : f.users.User , z : f.files[Mname]. comments[Uname] {

z in f.files[Mname]. comments[x] && z in f.files[Mname ]. comments[y]

=> x=y

}

// comments sobrejectiva

all x : f.files[Mname ]. comments[Uname] | one y : f.files[Mname ]. comments.

Comment {

y in f.files[Mname]. comments.x

}

// comments inteira (total)

all x : f.files[Mname ]. comments.Comment | some y : f.files[Mname]. comments[

Uname] {

y in f.files[Mname]. comments[x]

}

}


Relacao comments


Invariante global

pred inv_Flickr [ f : Flickr ] {

users_bijection[f]

files_bijection[f]

groups_bijection[f]

comments_inj_sur_ent[f]

inv_User[f]

inv_Media[f]

inv_Group[f]

}


Sumario


2 ESC/Java2

3 JMLUnit

4 Alloy Revisitado



create user

pred create_user [ f, f’ : Flickr , n :

Uname ] {

n !in f.users.User

one u : User {

u !in f.users[Uname]

no u.pstream

no u.public

no u.contacts

no u.favourites

f’. users = f.users + n->u

}

f’. files = f.files

f’. groups = f.groups

}


@ requires uname != null;

@ ensures m_users.containsKey(uname);


@ also


@ requires uname == null;




@*/

public void create_user(String uname)


if( !users.containsKey(uname) ) {

User u = new User(uname);

users.put(uname , u);

}

}


Invariantes

// apenas podem ser tornadas publicas fotos do resp. photostream

all u : f.users[Uname] | u.public in u.pstream

// media do pstream tem de estar registado

f.users[Uname ]. pstream in f.files.Media

// um user nao pode ser o seu proprio contacto

all n : f.users.User | n !in f.users[n]. contacts

// apenas podem ser tornadas publicas media do resp. photostream

//@ public invariant (\ forall User u; m_users.values ().contains(u); u.

getPStream ().containsAll(u.getPublics ()));

// media de um photostream tem de estar registado

//@ public invariant (\ forall User u; m_users.values ().contains(u); m_files.

keySet ().containsAll(u.getPStream ()));

// um utilizador nao pode ser o seu proprio contacto

//@ public invariant (\ forall User u; m_users.values ().contains(u); !(u.

getContacts ().contains(u.getUname ())));


Technology

Apresentacao JML