DbC Automation JML

50 %
50 %
Information about DbC Automation JML
Education

Published on February 5, 2008

Author: Bruno

Source: authorstream.com

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

Add a comment

Related presentations

Related pages

DbC Automation JML, SlideSearchEngine.com

DbC Automation JML Education presentation by Bruno ... Published on February 5, 2008. Author: Bruno. Source: authorstream.com
Read more

Outline Java Modeling Language (JML) - Soda Hall

Java Modeling Language (JML) ... – Automation ... 10/27/2004 JML and ESC/Java 2 8 Design by Contract (DBC) A way of recording:
Read more

Design by contract - Wikipedia, the free encyclopedia

Design by contract (DbC), also known as contract programming, ... Java Modeling Language (JML) Bean Validation (only pre- and postconditions) valid4j;
Read more

Design by contract with JML (PDF Download Available)

Official Full-Text Publication: Design by contract with JML on ResearchGate, the professional network for scientists.
Read more

Verificarea şi Validarea Sistemelor Soft - cs.ubbcluj.ro

Verificarea şi Validarea Sistemelor Soft Informatică – Română 2014-2015/ II Java Modeling Language (JML)
Read more

KeY Project: Integrated Deductive Software Design

KeY 2 differs significantly from the previous KeY 1.6 ... Further Enhancend JML Support ... KeY can optionally use SMT solvers to improve automation: CVC3;
Read more

A Library-Based Approach to Translating OCL Constraints to ...

A Library-Based Approach to Translating OCL Constraints to JML Assertions for Runtime Checking Carmen Avila, Guillermo Flores, Jr., and Yoonsik Cheon
Read more

A good Design-by-Contract library for Java? - Stack Overflow

... I did a survey of DbC packages for Java, ... A good Design-by-Contract library for Java? ... Manual testing is better than Automation testing.
Read more

On the Effectiveness of Contracts as Test Oracles in the ...

Design by contract (DbC) is a software development methodology that focuses on clearly defining the interfaces between components to produce better quality ...
Read more

Dynamic Dispatch for Method Contracts through Abstract ...

Dynamic Dispatch for Method Contracts through Abstract Predicates Wojciech Mostowski Formal Methods and Tools, University of Twente The Netherlands
Read more