עיצוב בעזרת חוזים Design by Contract

  • Published on
    05-Jan-2016

  • View
    30

  • Download
    5

Embed Size (px)

DESCRIPTION

Design by Contract. . 2009. . 1 . . . - PowerPoint PPT Presentation

Transcript

  • Design by Contract 2009

  • 1

    *

  • . : (separation of concern), . , ( ), .*

  • *API , , : , , , ' javadoc, html API (Application Programming Interface) : *

  • , () , , .: ( ): : ? : API ?: + ?*

  • , " , , , : divide :

    public static int divide(int numerator, int denominator) {...} , 6 - 2

    *

  • ? 7 - 2 ? ? ? ? ? ? ? ? ? ? ? ? ? , ? ?*

  • ... divide : ( , ') , , '...*

  • (design by contract) , (Bertrand Meyer) Hoare Floyd Java, , , : : , *

  • * (design by contract) : (precondition) ( , postcondition) , ( ) ( ): *

  • - divide/** * @pre denominator != 0 , * Cant divide by zero" * * @post Math.abs($ret * denominator)
  • - divide/** * @pre (denominator != 0) || (numerator != 0) , * "you can't divide zero by zero" * * @post (denominator == 0) && ((numerator > 0)) * $implies $ret == Integer.MAX_VALUE * "Dividing positive by zero yields infinity (MAX_INT)" * * @post (denominator == 0) && ((numerator < 0)) $implies * $ret == Integer.MIN_VALUE * "Dividing negative by zero yields minus infinity (MIN_INT)" * * @post Math.abs($ret * denominator)
  • ( ) : MyStack pop . ( )*

  • *

    /** @inv (top >= 0 && top < max)*/class MyStack { private Object[] elems; private int top, max; /** @pre (sz > 0) @post (max == sz && elems != null) */ public MyStack(int sz) { max = sz; elems = new Object[sz]; }

    *

  • * /** @pre !isFull() @post (top == $prev (top) + 1) && elems[top-1] == obj */ public void push(Object obj) { elems[top++] = obj; } /** @pre !isEmpty() @post (top == $prev (top) - 1) */ public void pop() { top--; } /** @pre !isEmpty() @post $ret == elems[top] */ public Object top() { return elems[top]; }

    *

  • *public boolean isFull() { return top == max; } /** @post ($ret == (top == 0)) */ public boolean isEmpty() { return top == 0; }}

    *

  • *

    /** @inv (top >= 0 && top < max)*/class MyStack { private T[] elems; private int top, max; /** @pre (sz > 0) @post (max == sz && elems != null) */ public MyStack(int sz) { max = sz; elems = (T[]) new Object[sz]; }

    *

  • * /** @pre !isFull() @post (top == $prev (top) + 1) && elems[top-1] == obj */ public void push(T obj) { elems[top++] = obj; } /** @pre !isEmpty() @post (top == $prev (top) - 1) */ public void pop() { top--; } /** @pre !isEmpty() @post $ret == elems[top] */ public T top() { return elems[top]; }

    *

  • *public boolean isFull() { return top == max; } /** @post ($ret == (top == 0)) */ public boolean isEmpty() { return top == 0; }}

    *

  • " " ,

    "" (business logic) " " " (defensive programming) *

  • ? !

    , : ( )

    . ? ...*

  • /** * @param a An array sorted in ascending order * @param x a number to be searched in a * @return the first occurrence of x in a, or -1 if * it x does not occur in a * * @pre "a is sorted in ascending order" */public static int searchSorted(int [] a, int x)

    ? , , ? 1- ? ? ? searchSorted . ...

    *

  • , ;

    ,

    ; ( )

    , 2/ *

  • , (, invariant) , (!) ,

    *

  • , " " " " " , , ( , ) ( )

    *

  • (representation invariant, Implementation invariant) (private), /** @inv (top >= 0 && top < max) @inv (elems != null) @inv top() == elems[top]*/class MyStack { private T[] elems; private int top, max; .....} " , *

  • , : /** @pre !isEmpty() @post (top == $prev (top) - 1) */ public void pop() { top--; } ?

    *

  • ?

    , , ( !) *

  • ? assert assert " true false (exception), . assert / / $prev assert ( )

  • : -2 int,

    *

  • -

  • * " , . . C A, : - C A C A / B A C A

  • * B ., .

  • * A f ( ) C a.f(..) a A , a BC A.f(..) B.f(..) C A.f(..) B.f(..)

  • public class MATRIX {.../** inverse of current with precision epsilon * @pre epsilon >= 10 ^(-6) * @post (this.mult($prev(this)) ONE).norm

  • public class ACCURATE_MATRIX extends MATRIX {.../** inverse of current with precision epsilon * @pre epsilon >= 10^(-20) * @post (this.mult($prev(this)) ONE).norm

  • , , Java

    ( [], [] ) [ ]

    [] []*

  • , ' , :

    [] , .

    ( 5) [] , []. ( -)*

  • - Pre Post , $prev(Pre) implies Post , "" ( ). x x . x , 0 x . ,

    *

  • " , *

  • " () : : require , : ensure : invariant ( and ), . old Result " ( ), : require else ensure then -- ( )*

  • class STACK [T] creation makefeature -- Initialization make(n: INTEGER) is -- Allocate stack for maximum of n elements, require positive_capacity: n >= 0 do capacity:=n !!representation(1,capacity) ensure capacity_set: capacity = n array_allocated: representation /= Void stack_empty: empty end - *

  • feature -- Access capacity: INTEGER -- The maximum number of stack elements count: INTEGER -- Number of stack elements top: T is -- Top element require not_empty: not empty -- i.e. count > 0 do Result:=representation @ count end *

  • feature -- Status report empty: BOOLEAN is -- Is stack empty? do Result:=(count = 0) ensure empty_definition: Result=(count = 0) end full: BOOLEAN is -- Is stack full? do Result:=(count = capacity) ensure full_definition: Result=(count=capacity) end *

  • feature -- Element change push(x: T) is -- Add x on top require not_full: not full do count:=count+1 representation.put(count,x) ensure not_empty: not empty added_to_top: top = x one_more_item: count = old count+1 in_top_array_entry: representation @ count =x end *

  • pop is -- Remove top element require not_empty: not empty do count:=count-1 ensure not_full: not full one_fewer: count = old count-1 endfeature {NONE}-- Implementation representation: ARRAY[T] -- The array used to hold elements *

  • Invariant -- of STACK count_non_negative: 0
  • check assert check assertion1; assertion2; .. end . : x:=a*a + b*b check x >=0 end push : if full then error:=Overflow else check representation /= Void end representation.push(x) error:=0 end*

  • from initialization_instructions -- optionalinvariant invariant -- optional variant variant -- optional until exit_condition loop loop_instructions end , . , . *

  • gcd(a,b: INTEGER): INTEGER is -- Greatest common divisor of a and b require a>0; b>0 local x, y : INTEGER do . -- see next slide ensure -- Result is the gcd of a and b end: GCD*

  • from x:=a; y:=b invariant x>0;y>0 --(x,y) have same GCD as (a,b) variant x.max(y) until x=y loop if x>y then x:=x-y else y:=y-x end end GCD *

  • short . . ( ). do ... , .' -- Javadoc , [ ' 5 (annotations) ]*

  • , . . exception : . ( ). *

  • - production . . . % 50 .

    *

  • - . : . (, ) : : , push , :

    *

  • : ( ) ( ) ? . : .*

  • , , ( ', #C) UML , OCL (Object Constraint Language)

  • " ' #C " '. : iContract2, Contract4J, jContractor JMSAssert" # C Code Contracts JMSAssert . , ( ).*

  • JML - The Java Modeling Language ' , , , null, (\forall Student s; juniors.contains(s); s.getAdvisor ( ) != null) juniors " , assignable x , y **

  • JML pure / ,

    **

  • public class Person{ /*@ normal_behavior @ requires kgs >= 0; @ assignable weight; @ ensures weight == \old(weight) + kgs; @ also @ exceptional_behavior @ requires kgs < 0; @ assignable \nothing; @ signals (Exception e) (e instanceof IllegalArgumentException); @*/public void addKgs(int kgs) { if (kgs >= 0) { weight += kgs; } else { throw new IllegalArgumentException(); } }}

  • JML ( ), ESC/Java , null **

  • Spec# API " JML , ' #C JML , ( )**

  • Spec# ArchitectureSource-LevelAnalysisByteCodeGenerationInvariant inferenceVerificationConditiongenerationTheoremprovingSpec#Source codeIntermediateLanguageBoogiePLBoogiePL withInvariantsFirst-OrderFormulaBoogieBoogieByteCodeTranslationSpec# Compilercorrect or list of errors

  • Non-Null Types back to exampleclass MyNonNullLibrary {public static void Clear(int[]! xs) { for (int i = 0; i < xs.Length; i++) { xs[i] = 0; }} } class ClientCode { static void Main() { int[] xs = null; MyNonNullLibrary.Clear(xs); } }WasInt[]

  • , ......

  • () / () ,

    HWe will get this Warning from the compiler

    Think why it is only a warning ? Expansion of C# - backward compatible