advertisement

Apresentacao JML

50 %
50 %
advertisement
Information about Apresentacao JML
Technology

Published on January 5, 2009

Author: UlissesCosta

Source: slideshare.net

advertisement

Flickr em JML Pedro Pereira Ulisses Costa M´todos Formais em Engenharia de Software e 18 de Dezembro de 2008 Pedro Pereira, Ulisses Costa Flickr em JML

Sum´rio a 1 JML O que ´? e Direitos e Deveres Isolamento e ajuda no debugging Linguagem formal e abstracta 2 ESC/Java2 3 JMLUnit 4 Alloy Revisitado 5 De Alloy para JAVA e JML Pedro Pereira, Ulisses Costa Flickr em JML

Sum´rio a 1 JML O que ´? e Direitos e Deveres Isolamento e ajuda no debugging Linguagem formal e abstracta 2 ESC/Java2 3 JMLUnit 4 Alloy Revisitado 5 De Alloy para JAVA e JML Pedro Pereira, Ulisses Costa Flickr em JML

Java Pedro Pereira, Ulisses Costa Flickr em JML

Java + JML Pedro Pereira, Ulisses Costa Flickr em JML

Sum´rio a 1 JML O que ´? e Direitos e Deveres Isolamento e ajuda no debugging Linguagem formal e abstracta 2 ESC/Java2 3 JMLUnit 4 Alloy Revisitado 5 De Alloy para JAVA e JML Pedro Pereira, Ulisses Costa Flickr em JML

Design by contract Contracto entre classe e clientes Classe explic´ os direitos e deveres ıta Cliente cumpre os deveres Classe atribui direitos Pedro Pereira, Ulisses Costa Flickr em JML

JML melhora o c´digo o JML s˜o anota¸˜es verificadas no programa a co Anota¸˜es s˜o puras co a Pode ajudar no debugging Isola os erros evitando propaga¸˜o ca Pedro Pereira, Ulisses Costa Flickr em JML

Especifica¸˜o em JML ca O JML ´ melhor que JAVAdoc (linguagem natural vs e linguagem formal) JML ´ mais abstracto que c´digo e o N˜o ´ necess´rio dar o algoritmo detalhado ae a Racionc´ modular ınio Compreens˜o mais r´pida dos m´todos a a e No pior caso basta ler os contractos dependentes do m´todo e O cliente n˜o pode concluir mais nada para al´m dos a e contractos Pedro Pereira, Ulisses Costa Flickr em JML

Sum´rio a 1 JML O que ´? e Direitos e Deveres Isolamento e ajuda no debugging Linguagem formal e abstracta 2 ESC/Java2 3 JMLUnit 4 Alloy Revisitado 5 De Alloy para JAVA e JML Pedro Pereira, Ulisses Costa Flickr em JML

Estados do JML 76 54 01 23 normal post state normal behaviour 4 76 54 76 54 01 state 23 01 23 pre exceptional post state 3 throwing de excepcao /. -, () *+ exceptional behaviour % excepcao java.lang .Error /. -, () *+ ' fora do alcance Pedro Pereira, Ulisses Costa Flickr em JML

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 e x c e p t i o n a l _ b e h a v i o u r @ requires unameA == null || unameB == null ; @ signals_only N u l l P o i n t e r E x c e p t i o n ; @ signals ( N u l l P o i n t e r E x c e p t i o n ) true ; @ assignable nothing ; @ */ public void add_contact ( String unameA , String unameB ) throws N u l l P o i n t e r E x c e p t i o n { User u = ( User ) users . get ( unameA ); Vector contacts = u . getContacts (); if ( ! contacts . contains ( unameB ) ) { contacts . add ( unameB ); u . setContacts ( contacts ); users . put ( unameA , u ); } } ... Pedro Pereira, Ulisses Costa Flickr em JML

Quando a pr´-condi¸˜o falha e ca Exception in thread main org.jmlspecs.jmlrac.runtime.JMLInternalPreconditionError: by method Flickr.add contact Flickr.java ... /* @ @ public n o r m a l_behaviour @ requires unameA != null ; Main.java (Culpado) @ requires unameB != null ; @ requires m_users . containsKey ( unameA ) ; @ requires m_users . containsKey ( unameB ) ; ... @ requires m_users . get ( unameA ) instanceof User ; Flick f = new Flickr (); @ ... ... @ */ f . add_contact ( quot; Pedro quot; ,quot; Ulisses quot; ); ... public void add_contact ( String unameA , String unameB ) throws N u l l P o i n t e r E x c e p t i o n { User u = ( User ) users . get ( unameA ); ... } ... Utilizadores n˜o est˜o registados no Flickr a a O objecto com esse nome n˜o ´ instˆncia de User ae a NOTA: verifica¸˜o com instanceof n˜o seria necess´ria em JAVA5 ca a a Pedro Pereira, Ulisses Costa Flickr em JML

Quando a p´s-condi¸˜o falha o ca Exception in thread ”main” org.jmlspecs.jmlrac.runtime.JMLInternalNormalPostconditionError: by method Flickr.add contact Flickr.java (Culpado) ... /* @ @ public n o r m a l_behaviour Main.java @ ... @ ensures (( User ) m_users . get ( unameA ) ) @ . getContacts () ... @ . contains ( unameB ) ; Flick f = new Flickr (); @ assignable m_users ; ... @ */ f . add_contact ( quot; Pedro quot; ,quot; Ulisses quot; ); ... public void add_contact ( String unameA , String unameB ) throws N u l l P o i n t e r E x c e p t i o n { ... } ... M´todo add contact ou nos m´todos que este usa e e Pedro Pereira, Ulisses Costa Flickr em JML

Quando a p´s-condi¸˜o falha o ca Quando o erro ´ de outros m´todos e e Exception in thread quot; main quot; org . jmlspecs . jmlrac . runtime . J M L I n t e r n a l N o r m a l P o s t c o n d i t i o n E r r o r : by method User . setContacts ... at Flickr . i n t e r n a l $ a d d _ c o n t a c t ( Flickr . java :246) ... at Main . internal$main ( Main . java :17) ... User.java (Culpado) Flickr.java ... ... /* @ public normal_behaviour /* @ @ requires contacts != null ; @ public n o r mal_behaviour @ ensures m_contacts . equals ( contacts ) ; @ ... @ assignable m_contacts ; @ ensures m_files . containsKey ( mname ) ; @ also @ (* ^ linha 246 *) @ public e x c e p t i o n a l _ b e h a v i o u r @ ... @ requires contacts == null ; @ */ @ signals_only N u l l P o i n t e r E x c e p t i o n ; @ signals ( N u l l P o i n t e r E x c e p t i o n ) true ; public void add_media @ assignable nothing ; ( String uname , String mname ) @ */ throws N u l l P o i n t e r E x c e p t i o n { ... public void setContacts ( Vector contacts ) { } this . contacts = new Vector (); ... } ... O JML aqui tenta ser preciso em v˜o. a Pedro Pereira, Ulisses Costa Flickr em JML

Sum´rio a 1 JML O que ´? e Direitos e Deveres Isolamento e ajuda no debugging Linguagem formal e abstracta 2 ESC/Java2 3 JMLUnit 4 Alloy Revisitado 5 De Alloy para JAVA e JML Pedro Pereira, Ulisses Costa Flickr em JML

Linguagem natural vs Linguagem formal Pedro Pereira, Ulisses Costa Flickr em JML

Mais abstracto que c´digo o Especifica¸˜o do m´todo del user ca e /* @ public normal_behaviour @ requires uname != null ; @ requires m_users . containsKey ( uname ) ; @ ensures ! m_users . containsKey ( uname ) ; @ assignable m_users , m_files , m_groups ; @ also @ public e x c e p t i o n a l _ b e h a v i o u r @ requires uname == null ; @ signals_only N u l l P o i n t e r E x c e p t i o n ; @ signals ( N u l l P o i n t e r E x c e p t i o n ) true ; @ assignable nothing ; @ */ N˜o ´ necess´rio dar o algoritmo detalhado ae a O contracto mantem-se, o cliente nunca ´ afectado e O contracto ´ muitas das vezes mais pequeno que o c´digo e o Pedro Pereira, Ulisses Costa Flickr em JML

Linguagem formal e abstracta public void del_user ( String uname ) throws N u l l P o i n t e r E x c e p t i o n { 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 ); } Pedro Pereira, Ulisses Costa Flickr em JML

Sum´rio a 1 JML O que ´? e Direitos e Deveres Isolamento e ajuda no debugging Linguagem formal e abstracta 2 ESC/Java2 3 JMLUnit 4 Alloy Revisitado 5 De Alloy para JAVA e JML Pedro Pereira, Ulisses Costa Flickr em JML

ESC/Java2 Valida¸˜o dos tipos de dados e s´ ca ıntax Detecta: referˆncias para apontadores nulos e casts ilegais indexa¸˜o de arrays fora dos limites ca Pedro Pereira, Ulisses Costa Flickr em JML

ESC/Java2 N˜o suporta todas as especifica¸˜es JML a co Pode indicar falsos negativos/positivos Pedro Pereira, Ulisses Costa Flickr em JML

Sum´rio a 1 JML O que ´? e Direitos e Deveres Isolamento e ajuda no debugging Linguagem formal e abstracta 2 ESC/Java2 3 JMLUnit 4 Alloy Revisitado 5 De Alloy para JAVA e JML Pedro Pereira, Ulisses Costa Flickr em JML

JMLUnit Gera Test Cases para m´todos e Usa pr´-condi¸˜es para filtar input e co Usa invariantes/p´s-condi¸˜es para capturar as falhas dos o co testes Pedro Pereira, Ulisses Costa Flickr em JML

JMLUnit Apenas tinhamos excep¸˜es NullPointerException co ... return new java . lang . String [] { quot; ulisses quot; , quot; pedro quot; , ... } ... switch ( n ) { case 0: return new User ( quot; pedro quot; ); case 1: return new User ( quot; ulisses quot; ); ... } ... Pedro Pereira, Ulisses Costa Flickr em JML

Sum´rio a 1 JML O que ´? e Direitos e Deveres Isolamento e ajuda no debugging Linguagem formal e abstracta 2 ESC/Java2 3 JMLUnit 4 Alloy Revisitado 5 De Alloy para JAVA e JML Pedro Pereira, Ulisses Costa Flickr em JML

Propriedades de uma HashTable? all u : f . users [ Uname ] | lone f . users . u all n : f . users . User | lone f . users [ n ] Pedro Pereira, Ulisses Costa Flickr em JML

O que ´ uma HashTable? e cada objecto est´ associado a uma imagem e vice-versa; a n˜o existem objectos ou imagens repetidas. a Pedro Pereira, Ulisses Costa Flickr em JML

Injectividade e Simplicidade injectividade a mesma imagem n˜o pode relacionar dois objectos a diferentes simplicidade o mesmo objecto n˜o pode relacionar duas imagens a diferentes Pedro Pereira, Ulisses Costa Flickr em JML

Sobrejectividade e Totalidade sobrejectividade cada imagem est´ relacionada com pelo menos a um objecto totalidade cada objecto est´ relacionado com pelo menos uma a imagem Pedro Pereira, Ulisses Costa Flickr em JML

Refinamento // media associado ao pstream tem de existir all u : f . users [ Uname ] | u . pstream in f . files . Media // nao ha media quot; solto quot; 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 Pedro Pereira, Ulisses Costa Flickr em JML

Rela¸˜o comments ca pred c o m m e n t s _ i n j _ s u r _ e n t [ 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 ] } } Pedro Pereira, Ulisses Costa Flickr em JML

Rela¸˜o comments ca Pedro Pereira, Ulisses Costa Flickr em JML

Invariante global pred inv_Flickr [ f : Flickr ] { u se rs _bijection [ f ] f il es _bijection [ f ] g r o u p s _bijection [ f ] comments_inj_sur_ent [f] inv_User [ f ] inv_Media [ f ] inv_Group [ f ] } Pedro Pereira, Ulisses Costa Flickr em JML

Sum´rio a 1 JML O que ´? e Direitos e Deveres Isolamento e ajuda no debugging Linguagem formal e abstracta 2 ESC/Java2 3 JMLUnit 4 Alloy Revisitado 5 De Alloy para JAVA e JML Pedro Pereira, Ulisses Costa Flickr em JML

create user /* @ public normal_behaviour pred create_user [ f , f ’ : Flickr , n : @ requires uname != null ; Uname ] { @ ensures m_users . containsKey ( uname ) ; n ! in f . users . User @ assignable m_users ; @ also one u : User { @ public e x c e p t i o n a l _ b e h a v i o u r u ! in f . users [ Uname ] @ requires uname == null ; @ signals_only N u l l P o i n t e r E x c e p t i o n ; no u . pstream @ signals ( N u l l P o i n t e r E x c e p t i o n ) true ; no u . public @ assignable nothing ; no u . contacts @ */ no u . favourites public void create_user ( String uname ) f ’. users = f . users + n - > u throws N u l l P o i n t e r E x c e p t i o n { } if ( ! users . containsKey ( uname ) ) { User u = new User ( uname ); f ’. files = f . files users . put ( uname , u ); f ’. groups = f . groups } } } Pedro Pereira, Ulisses Costa Flickr em JML

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 () ) ) ) ; Pedro Pereira, Ulisses Costa Flickr em JML

Add a comment

Related presentations

Presentación que realice en el Evento Nacional de Gobierno Abierto, realizado los ...

In this presentation we will describe our experience developing with a highly dyna...

Presentation to the LITA Forum 7th November 2014 Albuquerque, NM

Un recorrido por los cambios que nos generará el wearabletech en el futuro

Um paralelo entre as novidades & mercado em Wearable Computing e Tecnologias Assis...

Microsoft finally joins the smartwatch and fitness tracker game by introducing the...

Related pages

Apresentação EAD JML - YouTube

O Ensino à Distância da JML consiste em vídeos aula com estudo dirigido, permitindo acesso fácil, rápido e eficiente, segundo a ...
Read more

Minha apresentação de slides - YouTube

Fiz este vídeo com o Criador de slides do YouTube (http://www.youtube.com/upload)
Read more

EAD JML - Ensino a Distância - Curso de Licitação a ...

EAD JML - Ensino a Distância. Curso de FORMAÇÃO E CAPACITAÇÃO DE PREGOEIRO NO ÂMBITO DO SISTEMA
Read more

Apresentação "JML - ESDAH 2009/2010 1 Criação de ...

JML - ESDAH 2009/2010 1 Criação de páginas Web Módulo 3 Criação de páginas Web Joaquim Lopes Escola secundário Dão Afonso Henriques Vila das Aves ...
Read more

SEMINÁRIO NACIONAL DE GESTÃO POR COMPETÊNCIA - A ...

Materiais didáticos que levam a marca da JML, empresa especializada em promover cursos de alta qualidade; Profissionalismo, pontualidade, ...
Read more

SANÇÕES NAS CONTRATAÇÕES PÚBLICAS E A ...

Sites JML: Capacitação e Aperfeiçoamento. Central de Inscrições; Educação Corporativa Incompany; Fotos das Capacitações; Próximas ...
Read more

Apresentação do PowerPoint

Ipv Sbn Pfm Jml Jtb Mng Esp Esp Ipe Jqt Jnp Arc Jqt Musculação Campo de Areia * * Title: Apresentação do PowerPoint Author: STF Last modified by ...
Read more

PsicologiaB - JML: ATENÇÃO: PPT DA MEMÓRIA E ESQUECIMENTO

PsicologiaB - JML. Este sitio destina-se a apoiar o trabalho dos alunos da disciplina de Psicologia B da Escola Secundária Dr. Jaime Magalhães Lima, ...
Read more