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

• Published on
05-Jan-2016

• View
30

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