A JML Tutorial - Modular Specification and Verification of ...

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 ...