A JML Tutorial - Modular Specification and Verification of ...
232
pages
English
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
232
pages
English
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
AJMLTutorial
ModularSpecificationandVerification
ofFunctionalBehaviorforJava
1 2 3Gary T. Leavens Joseph R. Kiniry Erik Poll
1School of Electrical Engineering and Computer Science
University of Central Florida
2School of Computer Science and Informatics
University College Dublin
3Computing Science Department
Radboud University Nijmegen
Aug 27, 2007 / JML Tutorial / jmlspecs.org
GaryT.Leavens (UCF) JMLTutorial Fall2007 1/332 Intro.
Objectives
You’ll be able to:
Explain JML’s goals.
Read and write JML specifications.
Use JML tools.
Explain basic JML semantics.
Know where to go for help.
GaryT.Leavens (UCF) JMLTutorial Fall2007 2/332 Intro.
TutorialOutline
1 JMLOverview
2 ReadingandWritingJMLSpecifications
3 AbstractioninSpecification
4 SubtypingandInheritance
5 ESC/Java2
6 Conclusions
GaryT.Leavens (UCF) JMLTutorial Fall2007 3/332 Intro.
IntroduceYourself,Please
Question
Who you are?
Question
How much do you already know about JML?
Question
What do you want to learn about JML?
GaryT.Leavens (UCF) JMLTutorial Fall2007 4/332 Overview
Outline
1 JMLOverview
2 Reading and Writing JML Specifications
3 Abstraction in Specification
4 Subtyping and Inheritance
5 ESC/Java2
6 Conclusions
GaryT.Leavens (UCF) JMLTutorial Fall2007 5/332 Overview Basics
JavaModelingLanguage
Currently: Workingon:
Formal. Detailed Semantics.
Sequential Java. Multithreading.
Functional behavior of APIs. Temporal Logic.
Java 1.4. Java 1.5 (generics).
GaryT.Leavens (UCF) JMLTutorial Fall2007 6/332 Overview ...
Voir
ModularSpecificationandVerification
ofFunctionalBehaviorforJava
1 2 3Gary T. Leavens Joseph R. Kiniry Erik Poll
1School of Electrical Engineering and Computer Science
University of Central Florida
2School of Computer Science and Informatics
University College Dublin
3Computing Science Department
Radboud University Nijmegen
Aug 27, 2007 / JML Tutorial / jmlspecs.org
GaryT.Leavens (UCF) JMLTutorial Fall2007 1/332 Intro.
Objectives
You’ll be able to:
Explain JML’s goals.
Read and write JML specifications.
Use JML tools.
Explain basic JML semantics.
Know where to go for help.
GaryT.Leavens (UCF) JMLTutorial Fall2007 2/332 Intro.
TutorialOutline
1 JMLOverview
2 ReadingandWritingJMLSpecifications
3 AbstractioninSpecification
4 SubtypingandInheritance
5 ESC/Java2
6 Conclusions
GaryT.Leavens (UCF) JMLTutorial Fall2007 3/332 Intro.
IntroduceYourself,Please
Question
Who you are?
Question
How much do you already know about JML?
Question
What do you want to learn about JML?
GaryT.Leavens (UCF) JMLTutorial Fall2007 4/332 Overview
Outline
1 JMLOverview
2 Reading and Writing JML Specifications
3 Abstraction in Specification
4 Subtyping and Inheritance
5 ESC/Java2
6 Conclusions
GaryT.Leavens (UCF) JMLTutorial Fall2007 5/332 Overview Basics
JavaModelingLanguage
Currently: Workingon:
Formal. Detailed Semantics.
Sequential Java. Multithreading.
Functional behavior of APIs. Temporal Logic.
Java 1.4. Java 1.5 (generics).
GaryT.Leavens (UCF) JMLTutorial Fall2007 6/332 Overview ...
AJMLTutorial
ModularSpecificationandVerification
ofFunctionalBehaviorforJava
1 2 3Gary T. Leavens Joseph R. Kiniry Erik Poll
1School of Electrical Engineering and Computer Science
University of Central Florida
2School of Computer Science and Informatics
University College Dublin
3Computing Science Department
Radboud University Nijmegen
Aug 27, 2007 / JML Tutorial / jmlspecs.org
GaryT.Leavens (UCF) JMLTutorial Fall2007 1/332 Intro.
Objectives
You’ll be able to:
Explain JML’s goals.
Read and write JML specifications.
Use JML tools.
Explain basic JML semantics.
Know where to go for help.
GaryT.Leavens (UCF) JMLTutorial Fall2007 2/332 Intro.
TutorialOutline
1 JMLOverview
2 ReadingandWritingJMLSpecifications
3 AbstractioninSpecification
4 SubtypingandInheritance
5 ESC/Java2
6 Conclusions
GaryT.Leavens (UCF) JMLTutorial Fall2007 3/332 Intro.
IntroduceYourself,Please
Question
Who you are?
Question
How much do you already know about JML?
Question
What do you want to learn about JML?
GaryT.Leavens (UCF) JMLTutorial Fall2007 4/332 Overview
Outline
1 JMLOverview
2 Reading and Writing JML Specifications
3 Abstraction in Specification
4 Subtyping and Inheritance
5 ESC/Java2
6 Conclusions
GaryT.Leavens (UCF) JMLTutorial Fall2007 5/332 Overview Basics
JavaModelingLanguage
Currently: Workingon:
Formal. Detailed Semantics.
Sequential Java. Multithreading.
Functional behavior of APIs. Temporal Logic.
Java 1.4. Java 1.5 (generics).
GaryT.Leavens (UCF) JMLTutorial Fall2007 6/332 Overview Basics
JavaModelingLanguage
Currently: Workingon:
Formal. Detailed Semantics.
Sequential Java. Multithreading.
Functional behavior of APIs. Temporal Logic.
Java 1.4. Java 1.5 (generics).
GaryT.Leavens (UCF) JMLTutorial Fall2007 6/332 Overview Basics
JML’sGoals
Practical, effective for detailed designs.
Existing code.
Wide range of tools.
GaryT.Leavens (UCF) JMLTutorial Fall2007 7/332 Overview Basics
DetailedDesignSpecification
Handles: Doesn’thandle:
Inter module interfaces. User interface.
Classes and interfaces. Architecture, packages.
Data (fields) Dataflow.
Methods. Design patterns.
GaryT.Leavens (UCF) JMLTutorial Fall2007 8/332 Overview Basics
DetailedDesignSpecification
Handles: Doesn’thandle:
Inter module interfaces. User interface.
Classes and interfaces. Architecture, packages.
Data (fields) Dataflow.
Methods. Design patterns.
GaryT.Leavens (UCF) JMLTutorial Fall2007 8/332
