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

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

-

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

Description

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

Subjects

Informations

Published by
Reads 27
Language English
Report a problem
A JML Tutorial Modular Specification and Verification of Functional Behavior for Java Gary T. Leavens1Joseph R. Kiniry2Erik Poll3 1Department of Computer Science Iowa State University (moving to University of Central Florida) 2School of Computer Science and Informatics University College Dublin 3Computing Science Department Radboud University Nijmegen July 3, 2007 / CAV 2007 Tutorial / jmlspecs.org Gary T. Leavens (ISU TutorialUCF) JML
Intro. Tutorial Outline 1JML Overview 2Reading and Writing JML Specifications 3Abstraction in Specification 4Subtyping and Specification Inheritance 5ESC/Java2 6Conclusions
Gary T. Leavens (ISU TutorialUCF) JML
CAV 2007 1 / 225
CAV 2007 3 / 225
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.
Gary T. Leavens (ISU TutorialUCF) JML
Intro. Introduce Yourself, Please Question Who you are? Question How much do you already know about JML? Question What do you want to learn about JML?
Gary T. Leavens (ISUUCF) JML Tutorial
CAV 2007 2 / 225
CAV 2007 4 / 225
Overview Basics Java Modeling Language Currently: Working on: Formal. Detailed Semantics. Sequential Java. Multithreading. Functional behavior of APIs. Temporal Logic. Java 1.4. Java 1.5 (generics).
Gary T. Leavens (ISU TutorialUCF) JML
CAV 2007 6 / 225
Overview Basics Detailed Design Specification Handles: Doesn’t handle: Inter-module interfaces. User interface. Classes and interfaces. Architecture, packages. Data (fields) Dataflow. Methods. Design patterns.
Gary T. Leavens (ISU Tutorial CAVUCF) JML / 225 2007 8
Overview Basics JML’s Goals Practical, effective for detailed designs. Existing code. Wide range of tools.
Gary T. Leavens (ISU TutorialUCF) JML
Overview Flavor Basic Approach “Eiffel + Larch for Java” Hoare-style (Contracts). Method pre- and postconditions. Invariants.
Gary T. Leavens (ISUUCF) JML Tutorial
CAV 2007 7 / 225
CAV 2007 9 / 225
Overview Flavor A First JML Specification
public classArrayOps { private/*@spec_public@*/ Object[] a; //@publicinvariant0 < a.length; /*@requires0 < arr.length; @ensuresthis.a == arr; @*/ public voidinit(Object[] arr) { this.a = arr; }
Gary T. Leavens (ISUUCF) JML Tutorial
Overview Flavor Object Invariant
public classArrayOps { private/*@spec_public@*/ Object[] a; //@publicinvariant0 < a.length; /*@requires0 < arr.length; @ensures this.a == arr; @*/ public voidinit(Object[] arr) { this.a = arr; }
Gary T. Leavens (ISUUCF) JML Tutorial
CAV 2007 10 / 225
CAV 2007 12 / 225
Overview Flavor Field Specification withspec_public
public classArrayOps { private/*@spec_public@*/ Object[] a; //@public invariant0 < a.length; /*@requires0 < arr.length; @ensures this.a == arr; @*/ public voidinit(Object[] arr) { this.a = arr; }
Gary T. Leavens (ISU 11 / 225 CAV 2007UCF) JML Tutorial
Overview Flavor Method Specification withrequires,ensures
public classArrayOps { private/*@spec_public@*/ Object[] a; //@public invariant0 < a.length; /*@requires0 < arr.length; @ensuresthis.a == arr; @*/ public voidinit(Object[] arr) { this.a = arr; }
Gary T. Leavens (ISU / 225UCF) JML Tutorial CAV 2007 13
Overview Flavor Interface Specification
Gary T. Leavens (ISUUCF) JML Tutorial
Overview Flavor Like. . .But for Java and. . . VDM, but OO features Eiffel, but Features for formal verification Spec#, but Different invariant methodology More features for formal verification
Gary T. Leavens (ISUUCF) JML Tutorial
CAV 2007 14 / 225
CAV 2007 16 / 225
Overview Flavor Interface Specification
Gary T. Leavens (ISUUCF) JML Tutorial
Overview Flavor Unlike OCL and Z More Java-like syntax. Tailored to Java semantics.
Gary T. Leavens (ISU TutorialUCF) JML
CAV 2007 15 / 225
CAV 2007 17 / 225
Overview Flavor Many Tools, One Language
Gary T. Leavens (ISU TutorialUCF) JML
Overview Interest Interest in JML Many tools. State of the art language. Large and open research community: 23 groups, worldwide. Over 135 papers. See jmlspecs.org
Gary T. Leavens (ISUUCF) JML Tutorial
CAV 2007 18 / 225
CAV 2007 20 / 225
Overview Flavor How Tools Complement Each Other Different strengths: Runtime checking — real errors. Static checking — better coverage. Verification — guarantees. Usual ordering: 1Runtime checker (jmlc and jmlunit). 2Extended Static Checking (ESC/Java2). 3Verification tool (e.g., KeY, JACK, Jive).
Gary T. Leavens (ISUUCF) JML Tutorial
Overview Interest Advantages of Working with JML Reuse language design. Ease communication with researchers. Share customers. Join us!
Gary T. Leavens (ISUUCF) JML Tutorial
CAV 2007 19 / 225
CAV 2007 21 / 225
Overview Interest Opportunities in Working with JML Or: What Needs Work Tool development, maintenance. Extensible tool architecture. Unification of tools.
Gary T. Leavens (ISU TutorialUCF) JML
CAV 2007 22 / 225
R/W Lightweight JML Annotations Comments6=Java Annotations JML annotation comments: Line starting with//@ Between/*@and@*/, ignoring@’s starting lines. First character must be@
Gary T. Leavens (ISU 25 / 225UCF) JML Tutorial CAV 2007
Overview Finding More Where to Find More: jmlspecs.org Documents: “Design by Contract with JML” “An overview of JML tools and applications” “Preliminary Design of JML” “JML’s Rich, Inherited Specifications for Behavioral Subtypes” “JML Reference Manual” Also: Examples, teaching material. Downloads, sourceforge project. Links to papers, etc.
Gary T. Leavens (ISU CAV 2007UCF) JML Tutorial 23 / 225
R/W Lightweight JML Annotations Comments6=Java Annotations Question What’s wrong with the following? // @requires 0 < arr.length; // @ensures this.a == arr; public voidinit(Object[] arr)
Gary T. Leavens (ISU TutorialUCF) JML
CAV 2007 26 / 225
R/W Lightweight Most Important JML Keywords Top-level in classes and interfaces: invariant spec_public nullable For methods and constructors: requires ensures assignable pure
Gary T. Leavens (ISUUCF) JML Tutorial
R/W Lightweight BoundedStack’s Data and Invariant public classBoundedStack { private/*@spec_public nullable@*/ Object[] elems; private/*@spec_public@*/intsize = 0; //@publicinvariant0 <= size; /*@publicinvariantelems !=null @ && (\forall inti; @ size <= i && i < elems.length; @ elems[i] ==null); @*/
CAV 2007 27 / 225
Gary T. Leavens (ISU / 225 29 2007 CAV TutorialUCF) JML
R/W Lightweight Example: BoundedStack Example Specify bounded stacks of objects.
Gary T. Leavens (ISUUCF) JML Tutorial
R/W Lightweight BoundedStack’s Constructor /*@requires0 < n; @assignableelems; @ensureselems.length == n; @*/ publicBoundedStack(intn) { elems =newObject[n]; }
Gary T. Leavens (ISUUCF) JML Tutorial
CAV 2007 28 / 225
CAV 2007 30 / 225
R/W Lightweight BoundedStack’s push Method /*@requiressize < elems.length1; @assignableelems[size], size; @ensuressize == \old(size+1); @ensureselems[size1] == x; @lyntdanuder_serusne @ (\forall inti; 0 <= i && i < size1; @ elems[i] == \old(elems[i])); @*/ public voidpush(Object x) { elems[size] = x; size++; }
Gary T. Leavens (ISU TutorialUCF) JML
R/W Lightweight BoundedStack’s top Method /*@requires0 < size; @assignable\nothing; @ensures\result== elems[size1]; @*/ public/*@pure@*/ Object top() { returnelems[size1]; } }
Gary T. Leavens (ISU TutorialUCF) JML
CAV 2007 31 / 225
CAV 2007 33 / 225
R/W Lightweight BoundedStack’s pop Method /*@requires0 < size; @assignablesize, elems[size1]; @ensuressize == \old(size1); @dnudltnaeruser_seny @ elems[size] ==null @ && (\forall inti; 0 <= i && i < size1; @ elems[i] == \old(elems[i])); @*/ public voidpop() { size; elems[size] =null; }
Gary T. Leavens (ISUUCF) JML Tutorial
R/W Lightweight spec_public, nullable, and invariant spec_public Public visibility. Only public for specification purposes. nullable field (and array elements) may be null. Default isnon_null. invariantmust be: True at end of constructor. Preserved by each method.
Gary T. Leavens (ISU TutorialUCF) JML
CAV 2007 32 / 225
CAV 2007 34 / 225
R/W Lightweight requires and ensures requiresclause: Precondition. Obligation on callers, after parameter passing. Assumed by implementor. ensuresclause: Postcondition. Obligation on implementor, at return. Assumed by caller.
Gary T. Leavens (ISU TutorialUCF) JML
R/W Lightweight Semantics of Requires and Ensures
Gary T. Leavens (ISU TutorialUCF) JML
CAV 2007 35 / 225
CAV 2007 37 / 225
R/W Lightweight Semantics of Requires and Ensures
Gary T. Leavens (ISUUCF)
JML Tutorial
R/W Lightweight Semantics of Requires and Ensures
Gary T. Leavens (ISUUCF) JML Tutorial
CAV 2007 36 / 225
CAV 2007 38 / 225
R/W Lightweight assignable and pure assignable Frame axiom. Locations (fields) in pre-state. New object fields not covered. Mostly checked statically. Synonyms:modifies,modifiable pure No side effects. Impliesassignable\nothing Allows method’s use in specifications.
Gary T. Leavens (ISUUCF) JML Tutorial
R/W Lightweight Redundant Clauses E.g.,neeruser_sdundantly Alerts reader. States something to prove. Must be implied by: ensuresclauses, assignableclause, invariant, and JML semantics. Alsoruieqdnnaltyer_serud, etc.
Gary T. Leavens (ISU TutorialUCF) JML
CAV 2007 39 / 225
CAV 2007 41 / 225
R/W Lightweight Assignable is a Shorthand assignablegender; ensuresgender.equals(g); means ensures\only_assigned(gender) && gender.equals(g);
Gary T. Leavens (ISU TutorialUCF) JML
R/W Lightweight
CAV 2007 40 / 225
Multiple Clauses Semantics: requiresP; requiresQ; is equivalent to: requiresP&&Q; Similarly forensures,invariant. Note: runtime checker gives better errors with multiple clauses.
Gary T. Leavens (ISU / 225 42 TutorialUCF) JML 2007 CAV
R/W Lightweight Defaults for Omitted Clauses invarianttrue; requirestrue; assignable\everything; ensurestrue;
Gary T. Leavens (ISUUCF) JML Tutorial
CAV 2007 43 / 225
R/W Exercise Steps for Specifying a Type for Public Clients 1Specify data (spec_publicfields). 2Specify apublicinvariant. 3Specify each public method using: 1sreruieq. 2ssaangielb(orpure). 3ensures.
Gary T. Leavens (ISU TutorialUCF) JML
CAV 2007 45 / 225
R/W Lightweight Expression Keywords \result= method’s return value. \old(E) value of= pre-stateE. (\forallT x;P;Q)=V{Q|xTP} (\existsT x;P;Q)=W{Q|xTP} (\minT x;P;E)= min{E|xTP} (\sumT x;P;E)=P{E|xTP} (\num_ofT x;P;Q)=P{1|xTPQ}   
Gary T. Leavens (ISU Tutorial CAV 2007 44UCF) JML / 225
R/W Exercise Exercise: Specify BagOfInt (7 minutes) Exercise Specify the following: public classBagOfInt { /** Initialize to contain input’s elements. */ publicBagOfInt(int[] input); /** Return the multiplicity of i. */ public intoccurrences(inti); /** Return and delete the minimum element. */ public intextractMin(); }
Gary T. Leavens (ISU / 225 2007 46 Tutorial CAVUCF) JML