A JML Tutorial - Modular Specification and Verification of Functional Behavior for Java

Intro.ObjectivesAJMLTutorial You’ll be able to:ModularSpecificationandVerificationExplain JML’s goals.ofFunctionalBehaviorforJavaRead and write JML specifications.Use JML tools.1 2 3Gary T. Leavens Joseph R. Kiniry Erik Poll Explain basic JML semantics.Know where to go for help.1Department of Computer ScienceIowa State University (moving to University of Central Florida)2School of Computer Science and InformaticsUniversity College Dublin3Computing Science DepartmentRadboud University NijmegenJuly 3, 2007 / CAV 2007 Tutorial / jmlspecs.orgGaryT.Leavens (ISU→UCF) JMLTutorial CAV2007 1/225 GaryT.Leavens (ISU→UCF) JMLTutorial CAV2007 2/225Intro. Intro.TutorialOutline IntroduceYourself,PleaseQuestion1 JMLOverviewWho you are?2 ReadingandWritingJMLSpecificationsQuestionHow much do you already know about JML?3 AbstractioninSpecificationQuestion4 SubtypingandInheritanceWhat do you want to learn about JML?5 ESC/Java26 ConclusionsGaryT.Leavens (ISU→UCF) JMLTutorial CAV2007 3/225 GaryT.Leavens (ISU→UCF) JMLTutorial CAV2007 4/225Overview Basics Overview BasicsJavaModelingLanguage JML’sGoalsPractical, effective for detailed designs.Existing code.Currently: Workingon:Wide range of tools.Formal. Detailed Semantics.Sequential Java. Multithreading.Functional behavior of APIs. Temporal Logic.Java 1.4. Java 1.5 (generics).GaryT.Leavens (ISU→UCF) JMLTutorial CAV2007 6/225 GaryT.Leavens (ISU→UCF) JMLTutorial CAV2007 7/225Overview Basics Overview ...