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

Gary T. Leavens, Joseph R. Kiniry, Erik Poll

Sujets

• Union des communistes de France marxiste-léniniste
• RW
• Spécification (informatique)
• Spectres
• Gender studies
• Lightweight Third Party Authentication

Informations

• Publié par: Cheyn
• Nombre de lectures: 122
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

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