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

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

-

English
232 Pages
Read
Download
Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

Description

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

Subjects

Informations

Published by
Reads 122
Language English
Document size 2 MB
Report a problem
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