DbC Automation JML

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

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