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

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

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

Informations

• Publié par: Sosul
• Nombre de lectures: 16
• Langue: English

Extrait

A JML Tutorial Modular Specification and Verification of Functional Behavior for Java Gary T. Leavens1Joseph R. Kiniry2Erik Poll3 1 Department of Computer Science Iowa State University (moving to University of Central Florida) 2 School of Computer Science and Informatics University College Dublin 3 Computing Science Department Radboud University Nijmegen July 3, 2007 / CAV 2007 Tutorial / jmlspecs.org Gary T. Leavens (ISU→ TutorialUCF) JML

Intro. Tutorial Outline 1 JML Overview 2 Reading and Writing JML Specifications 3 Abstraction in Specification 4 Subtyping and Specification Inheritance 5 ESC/Java2 6 Conclusions

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 (ISU→UCF) 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 (ISU→UCF) 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 (ISU→UCF) 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 (ISU→UCF) 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 (ISU→UCF) 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 (ISU→UCF) JML Tutorial

CAV 2007 14 / 225

CAV 2007 16 / 225

Overview Flavor Interface Specification

Gary T. Leavens (ISU→UCF) 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 (ISU→UCF) 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: 1 Runtime checker (jmlc and jmlunit). 2 Extended Static Checking (ESC/Java2). 3 Verification tool (e.g., KeY, JACK, Jive).

Gary T. Leavens (ISU→UCF) JML Tutorial

Overview Interest Advantages of Working with JML Reuse language design. Ease communication with researchers. Share customers. Join us!

Gary T. Leavens (ISU→UCF) 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 (ISU→UCF) 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 (ISU→UCF) JML Tutorial

R/W Lightweight BoundedStack’s Constructor /*@requires0 < n; @assignableelems; @ensureselems.length == n; @*/ publicBoundedStack(intn) { elems =newObject[n]; }

Gary T. Leavens (ISU→UCF) 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 (ISU→UCF) 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 is non_null . invariant must 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 requires clause: Precondition. Obligation on callers, after parameter passing. Assumed by implementor. ensures clause: 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 (ISU→UCF)

JML Tutorial

R/W Lightweight Semantics of Requires and Ensures

Gary T. Leavens (ISU→UCF) 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. Implies assignable\nothing Allows method’s use in specifications.

Gary T. Leavens (ISU→UCF) JML Tutorial

R/W Lightweight Redundant Clauses E.g., neeruser_sdundantly Alerts reader. States something to prove. Must be implied by: ensures clauses, assignable clause, invariant , and JML semantics. Also ruieqdnnaltyer_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: requires P ; requires Q ; is equivalent to: requires P && Q ; Similarly for ensures , 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 (ISU→UCF) JML Tutorial

CAV 2007 43 / 225

R/W Exercise Steps for Specifying a Type for Public Clients 1 Specify data ( spec_public fields). 2 Specify a publicinvariant . 3 Specify each public method using: 1 sreruieq . 2 ssaangielb (or pure ). 3 ensures .

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|x∈T∧P} (\existsT x; P ; Q ) = W {Q|x∈T∧P} (\minT x; P ; E ) = min{E|x∈T∧P} (\sumT x; P ; E ) = P {E|x∈T∧P} (\num_ofT x; P ; Q ) = P {1|x∈T∧P∧Q}   

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