La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
Télécharger Lire

Tutorial [] The KeY Approach to Deductive Verification of Object -Oriented Programs

De
72 pages
TutorialThe KeY Approach to Deductive Veri cationof Object-Oriented ProgramsWolfgang Ahrendt, Bernhard Beckert, Reiner Hahnle,Philipp Rummer, Peter H. Schmittwww.key-project.org5th International Symposium onFormal Methods for Components and ObjectsAmsterdam, NLNovember 9, 2006Deductive Veri cation of OO Programs: FMCO 2006 1 / 57What is this Tutorial all About?It is about an approach and tool for theDesignFormal specicationDeductive veri cationofOO softwareThe approach, tool, and project is namedin the following: ’KeY’Deductive Veri cation of OO Programs: Introduction FMCO 2006 2 / 57KeY Project PartnersChalmers UTUniversity of University ofG oteborgKarlsruhe (TH) Koblenz-LandauReiner HahnlePeter H. Schmitt Bernhard BeckertWolfgang AhrendtRichard Bubel Gerd BeusterDaniel LarssonSte en Schlager Christoph GladischPhilipp RummerIsabel Tonin Vladimir KlebanovAngela WallenburgDeductive Veri cation of OO Programs: Introduction FMCO 2006 3 / 57Some Buzzwords Early OnJava as target languageDynamic logic as program logicVeri cation = symbolic execution + inductionSequent style calculus + meta variables + incremental closureProver is interactive + automatedIntegration with two standard SWE tools:TogetherCC, a commercial CASE toolEclipse, an open extensible IDESpeci cation languagesJMLOCL/UMLSmart cards as main target applicationDeductive Veri cation of OO Programs: Introduction FMCO 2006 4 / 57Part IOverview of the KeY ...
Voir plus Voir moins
eD
Tutorial The KeY Approach to Deductive Verification of Object-Oriented Programs
ductiveV
WolfgangAhrendt,BernhardBeckert,ReinerHa¨hnle, PhilippRu¨mmer,PeterH.Schmitt
ericati
www.key-project.org
5th International Symposium on Formal Methods for Components and Objects
nofoOOrPorgma:s
Amsterdam, NL November 9, 2006
MFCO20061/57
ront:ImsnFioctdu26002OCM
It is about anapproachandtoolfor the Design Formal specification Deductive verification
in the following: KeY’
Theapproach,tool, andprojectis named
What is this Tutorial all About?
75/ductDeeriiveVnofoacitgoarOOrP
of
OO software
oducIntrams:rogrOfPOoionctaeVirvetiucedD
Bernhard Beckert Gerd Beuster Christoph Gladisch Vladimir Klebanov
University of Koblenz-Landau
KeY Project Partners
Chalmers UT G¨oteborg
ReinerH¨ahnle Wolfgang Ahrendt Daniel Larsson PhilippR¨ummer Angela Wallenburg
University of Karlsruhe (TH)
Peter H. Schmitt Richard Bubel Steffen Schlager Isabel Tonin
600275/3noitOCMF
ontiOOofogPrmsraudeDvitcreVeaciO20064/57
Some Buzzwords Early On
Javaas target language Dynamic logicas program logic Verification =symbolic execution+induction Sequent stylecalculus + meta variables + incremental closure Prover isinteractive+automated Integration with two standard SWE tools: TogetherCC, a commercial CASE tool Eclipse, an open extensible IDE Specification languages JML OCL/UML Smart cardsas main target application
I:tnorudtcoiFnCM
Deductive
Verification
Overview
of
OO
Programs:
Part
of
the
I
KeY
system
FMCO
2006
5
/
57
First
Demo
Deductive
Verification
of
OO
Programs:
First
Demo
FMCO
2006
6
/
57
067/57
Supported Specification Languages: OCL
ObjectConstraintLanguage
Part of the OMG standard UML
Scope: Add formal constraints to UML (class) diagrams
F:ritseDomMFOC02ontiOOofogPrmsraudeDvitcreVeaci
edDtiucVevecriioatOfonorPOmargiF:srstDemoFMCO200685/7
JavaModelingLanguage Behavioral interface specification language for Java
Supported Specification Languages: JML
Comes with assertion and runtime checkers
International community effort lead by Gary T. Leavens, Iowa State building on the Larch approach
criVevetiucedD
differences OCL model oriented: attached to class diagrams ‘talks’ UML JML implementation oriented: attached to Java programs ‘talks’ Java specifies exceptional behaviour also JML only: restricting scope of side effects
both specify method behaviour: pre/post conditions specify admissible states: class invariants essentially full first order support inter-object navigation
OCL and JML
960075/emoFMCO2s:FirstDPOorrgmataoionOf
JML example /*@public normal_behavior @requiresa !=null; @ensures(\forall intj; j >= 0 && j < a.length; @\result>= a[j]); @ensuresa.length > 0 ==> @(\exists intj; j >= 0 && j < a.length; @\result== a[j]); @*/ public static/*@pure@*/intmax(int[] a) { if( a.length == 0 )return0; intmax = a[0], i = 1; while( i < a.length ) { if( a[i] > max ) max = a[i]; ++i; } returnmax; } Deductive Verification of OO Programs: First Demo FMCO 2006 10 / 57
KeY
Architecture
Deductive
Verification
of
OO
Programs:
First
Demo
FMCO
2006
11
/
57