Design by Contract Automation:JML: Design by Contract Automation: JML dan wilkin bit.stream@alum.com SevaJug 16 October 2007


Overview: Overview 2


Design by Contract: Design by Contract 3


Design by Contract (Briefly): Design by Contract (Briefly) 4


Design by Contract (Briefly): Design by Contract (Briefly) 5


LOGIC MECHANICS: LOGIC MECHANICS A Surface Exposure to 6


Logic: Logic Defined: reasoning within a domain of observations to establish premises that yield a deduction Involves: differentiating facts from assumptions proving deductions, eliminating failed deductions Formal Logic Defined: expressions about a domain based on explicitly stated observations and propositions from which additional expressions are drawn results in a knowledge base identifies axioms as basis of expressions axiom: a self-evident principle or rule that is accepted without proof as the basis for argument, a postulate - American Heritage Dictionary 7 JML most resembles First-Order Logic


First-Order Logic: Quantifiers - Universal (“for all [x]”) - Existential (“there exists [some x in]”) predicate: a statement describing the property or relationship of a subject quantifier: an operator on a subject in order that predicates may be created over collections of subjects having the same type First-Order Logic Defined: a descriptive formal logic adding subjects, predicates, and quantifiers to form expressions yielding deductions Syntax: ident - some variable/subject, e.g. x, y name(…) - some predicate operating on some subject 8 enhances Propositional Logic (which in turn enhances Boolean Logic) enhanced by Second-Order Logic as with the other logics, a formal syntax to describe propositions (state what we know or want to prove from observations) as with the other logics, all deductions are subject to proofs


Slide9: Satisfiablility An expression is satisfiable IFF there is at least one set of values that makes the expression true. All self-contradictory expressions are unsatisfiable by definition e.g. “There is a podium in front of me and there is not a podium in front of me.” Deductions truth of an expression = the interpretation and observations of the world e.g. Siblings(Tim, Tam) - what do we know about the family of Tim and Tam for this predicate to be true? 9


Logic Mechanics: Examples: Logic Mechanics: Examples “One’s father is one’s male parent” f, c Father(f, c) Male(f) Parent(f, c) “It is a crime for an American to sell weapons to hostile nations.” x, y, z American(x) Weapon(y) Nation(z) Hostile(z) Sells(x, z, y)  Criminal(x) f, c Father(c) = f Male(f) Parent(f, c) 10


Logic Mechanics: Examples: x, y, i0 Interval(Engaged(x, y), i0)  i1 (Meet(i0, i1) After(i1, i0)) Interval(Marry(x, y) BreakEngagement(x, y), i1) Logic Mechanics: Examples i, j Meet(i, j) Time(End(i)) = Time(Start(j)) i, j After(j, i) Time(End(i)) > Time(Start(j)) 11


JAVA MODELING LANGUAGE: JAVA MODELING LANGUAGE jmlspecs.org 12


Purpose & Benefits: Purpose & Benefits 13


Purpose & Benefits: Purpose & Benefits 14


Background: Background Possible XP-style JML integration 15


Language Features: The default expressions for the heavyweight specifications are moderately complex; in short, they operate in an apparent stricter fashion, demanding more from the spec writer Language Features 16


Language Features: Language Features instance and/or static fields instance and/or static methods overriding methods: superclass method specifications defined with code are not inherited to subclasses (similar to final keyword) overriding methods will inherit superclass specifications; compiler error w/o keyword also Exception: private methods declared with helper JML modifier are not subject to the invariants defined in the class 17 methods with no specification take the default lightweight behavior: assignable \everything, requires \nothing, etc. class body level specifications can be invariants and history constraints. History constraints define how object state is expected to change over the life of the instance. Model programming affords model only methods, fields, and JML code. Model programs can also be embedded within Java methods, e.g. //@ assert


Language Features: Language Features 18


Language Features: Language Features 19


Language Features: Language Features 20


Language Features: Language Features 21


Language Features: Language Features Contains JML specifications only with Java method signatures - even for concrete classes, e.g. in java.util.LinkedList: public String toString(); Follow-up refinements to “tighten” specification or e.g. add specs to less visible methods. Negotiate and define with interface-participant Engineering staff to obtain the best interface between systems. Implement specification Modifiable (owned) Java class with embedded JML specifications. Additional refinements can be applied over time. Or, the Java class may not contain any specifications and this refinement file provides them. 22


Tools: Tools 23


Tools: Tools 24


Tools: Tools 25


Tools: Tools 26


Install/Configuration: Install/Configuration 27


Install/Configuration: Install/Configuration 28 jmlenv.bat


Examples: Examples 29


Summary: Summary 30


Examples: Examples Person.java 31


Examples: Examples Queue.java Queue.java (continued) 32


Examples: Examples Queue.java (continued) 33


Examples: Examples Queue.java (continued) 34


Examples: Examples Store.java Store.java (continued) 35


Examples: Examples Store.java (continued) EmptyQueueException.java 36