An overview of JML Tools and Applications
description
Transcript of An overview of JML Tools and Applications
Paola Spinazzé, 809506Luca Leonardi, 810086
Linguaggio di specifica Permette di descrivere analiticamente
proprietà di codice Java◦ Descrizione di pre condizioni◦ Descrizione di post condizioni◦ Descrizione di invarianti
Specifica commenti in una particolare forma all’interno dei quali si inseriscono parole chiave e operatori particolari
//@.........../*@..............@*/
2
invariant: identifica l’invariante requires: identifica precondizioni assignable: identifica campi della classe
modificabili dal metodo ensures: identifica postcondizioni signlas: identifica postcondizioni in caso di
eccezione \old(name): riferimento al valore originario
della variabile name \forall …: quantificatore universale \result: valore di ritorno del metodo
3
4
Controllo a run-time◦ jmlc ◦ jmlunit
Controllo statico◦ ESC/Java (ESC/Java2)◦ LOOP◦ JACK
Generazione di specifiche◦ Daikon◦ Houdini
Documentazione◦ jmldoc
5
Si esegue il programma per verificare che le caratteristiche che deve avere siano rispettate.
6
Estensione di javac Compila in bytecode Java con asserzioni JML Preserva il comportamento del programma Peggiora le prestazioni (tempo e spazio) Fornisce informazioni per l’individuazione di
errori Affidabilità
◦ I risultati che fornisce sono corretti, ma alcune asserzioni possono essere ignorate
7
Permettono di verificare unità di programma in modo indipendente
Vengono create classi di test che richiamano le classi in analisi inviando messaggi predefiniti per testarne le funzionalità implementate
8
Permette di automatizzare il processo di testing del codice
Il tool genera le classi di test automaticamente a partire dalle specifiche JML annotate nelle classi in analisi
Si controlla che le violazioni prodotte non siano causate da violazioni delle precondizioni dovute ai dati di test immessi dall’utente
9
Si tenta di stabilire staticamente se le caratteristiche di un determinato codice
vengono rispettate. Non è legato a particolari esecuzioni.
10
Controlla senza eseguire il codice possibili errori a run-time
Supporta un sottoinsieme delle asserzioni definite in JML
Utilizza le annotazioni JML in due modi:◦ elimina alcuni warning del compilatore javac◦ verifica che le precondizioni siano rispettate
Fornisce informazioni sui metodi che possono causare o causano errori/warning
11
Né correttezza né completezza◦ Intenzionale per prestazioni
Trasforma le annotazioni JML in formule logiche valide sse il programma non presenta il tipo di errori che le annotazioni identificano
Utilizza un “theorem prover” per verificare la correttezza delle formule
Esc/Java2 ne estende alcune funzionalità
12
Verifica proprietà specificate in JML Formalizza una semantica denotazionale in
PVS Genera una “proof obligation” per ogni
metodo del codice da verificare Output di difficile interpretazione da
analizzare successivamente con tecniche di analisi PVS
13
ESC/Java: nessuna interazione con l’utente, semplice da usare, determina solo alcuni errori
LOOP: interazione con l’utente
Possono essere utilizzati assieme◦ ESC/Java elimina una parte degli errori◦ LOOP raffina i risultati
14
Utilizzato in progetti in cui lo sforzo sia giustificabile
Librerie JAVA (Vector)
SmartCards (JavaCard API)
15
Implementa un calcolo di weakest precondition automatizzato a partire dalle annotazioni JML
Le weackest precondition vengono dimostrate con dei prover automatici
Permette anche di annotare automaticamente il codice tramite JML
16
Corretto e completo◦ Genera solo quei giudizi la cui formalizzazione è
rispettata dall’applicazione
Due possibilità:◦ controllo dei soli giudizi non provati
automaticamente◦ controllare tutti i giudizi attraverso un theorem
prover interattivo
17
Si tenta di inferire automaticamente le specifiche che un determinato codice deve
avere.
18
Genera specifiche per il codice sorgente in input
Trova invarianti di punti specifici del programma
Osserva i valori calcolati durante dei test e ne controlla l’accuratezza
Accuratezza dipende da qualità e completezza dei test◦ Usa analisi statiche e test statistici per ridurre la
probabilità di errore Non gestisce le clausole signals
19
Deduce annotazioni JML per un dato programma
Algoritmo◦ Genera delle annotazioni JML candidate◦ Esegue ESC/Java più volte per eliminare quelle
non consistenti con il codice (non considera i potenziali errori a runtime)
◦ Nell’ultima esecuzione restituisce l’output di ESC/Java
20
Aiuta i programmatori a comprendere le specifiche JML per un dato progetto.
21
Estende il tool javaDoc col supporto a JML
Analizza il codice per trovare le specifiche per ogni metodo (es. in caso di overrides)
Produce documenti HTML contenenti sia informazioni javaDoc che specifiche JML
22
JML risulta essere facile da imparare a programmatori Java in quanto simile a Java stesso
Non vi è la necessità di specificare un modello formale, in quanto il codice rappresenta il modello stesso (non esistono bug che possono sfuggire al modello)
Notazione standard che permette di usare facilmente qualsiasi tool che la supporti senza necessità di imparare molti linguaggi
23
Runtime checking: aiutano ad identificare possibili errori che possono essere legati a particolari esecuzioni◦ jmlc utile per testare intere applicazioni◦ jmlunit utile per testare singole funzionalità
Static checking: più precisi dei precedenti; la correttezza del programma è assicurata per qualsiasi esecuzione◦ ESC/Java semplice da usare ma identifica solo pochi
errori◦ LOOP e JACK più completi: il primo richiede conoscenze
di PVS, mentre per il secondo non sono necessarie conoscenze di prover
24
Generating Specification: la generazione di specifiche JML può non essere sempre facile, specie se fatta in fase post-development◦ Daikon: genera annotazioni per un programma
non annotato◦ Houdini: annota un programma e fornisce i
warning testati da ESC/Java
25
[1] L.Burdy, Y. Cheon, D. Cok, M. D. Ernst, J. Kinkry, G.T. Leavens, K.R.M Leino, E. Pool, “An Overview of JML Tools and Application”
[2] http://www.cs.iastate.edu/~leavens/JML/
[3] J. Van den Berg, B. Jacobs,“The LOOP compiler for Java and JML”,http://www.cs.kun.nl/~bart/PAPERS/tacas01.ps.Z
[4] C. Flanagan, K. R. M. Leino,“Houdini, an Annotation Assistant for ESC/Java”, http://gatekeeper.research.compaq.com/pub/Compaq/SRC/publications/rustan/krml100.ps
26