Lösungsvorschlag Software Architecture FS08: Unterschied zwischen den Versionen

Aus VISki
Wechseln zu: Navigation, Suche
Zeile 129: Zeile 129:
 
'''Prove that balance(c) >= 0:'''
 
'''Prove that balance(c) >= 0:'''
  
Base case: <math> balance(c_0) = 0 </math> using A2, <math> c_0 = </math> new_card(l)
+
'''Base case:''' <math> balance(c_0) = 0 </math> using A2, <math> c_0 = </math> new_card(l)
  
Induction assumption: <math> c_n </math> is a correct expression of type CREDIT_CARD of length <math>n</math>, i.e. <math> balance(c_n) \geq 0 </math>
+
'''Induction assumption:''' <math> c_n </math> is a correct expression of type CREDIT_CARD of length <math>n</math>, i.e. <math> balance(c_n) \geq 0 </math>
  
Induction step:  
+
'''Induction step: '''
  
 
<math> balance(settle(c_n)) = 0 </math> using A4
 
<math> balance(settle(c_n)) = 0 </math> using A4
Zeile 142: Zeile 142:
 
'''Prove that <math> balance(c) \leq limit(c) </math>'''
 
'''Prove that <math> balance(c) \leq limit(c) </math>'''
  
Base case:  
+
'''Base case: '''
  
 
<math> c_0 = </math> new_card(l: INTEGER)
 
<math> c_0 = </math> new_card(l: INTEGER)
Zeile 152: Zeile 152:
 
Hence: <math> balance(c_0) = 0 \leq limit(c_0) = l > 0 </math> using P1 for the last inequality
 
Hence: <math> balance(c_0) = 0 \leq limit(c_0) = l > 0 </math> using P1 for the last inequality
  
Induction assumption:  
+
'''Induction assumption: '''
  
 
<math> c_n </math> is a correct expression of type CREDIT_CARD and length <math> n </math>, that is:
 
<math> c_n </math> is a correct expression of type CREDIT_CARD and length <math> n </math>, that is:
Zeile 158: Zeile 158:
 
<math> balance(c_n) \leq limit(c_n) </math> and <math> limit(c_n) > 0 </math>
 
<math> balance(c_n) \leq limit(c_n) </math> and <math> limit(c_n) > 0 </math>
  
Induction step (reuse inequalities found for balance above):
+
'''Induction step (reuse inequalities found for balance above):'''
  
 
<math> balance(settle(c_n)) = 0</math> (see above) and <math> limit(settle(c_n)) = limit(c_n) > 0 </math> using A3 and induction assumption, hence  
 
<math> balance(settle(c_n)) = 0</math> (see above) and <math> limit(settle(c_n)) = limit(c_n) > 0 </math> using A3 and induction assumption, hence  

Version vom 21. Mai 2009, 22:14 Uhr

Modularity, ADT, Designy by Contract and Concurrency (8 points)

b

d

f: true, since the visitor needs to know implementation details of the objects it visits

b: true because class invariants are 'and'-ed, hence stronger assertions can be introduced

c

Design by Contract (12 points)

<eiffel> class

 BANK_ACCOUNT

feature withdraw(v: INTEGER) is

 require TRUE

do end

feature balance: INTEGER

end

class STUDENT_ACCOUNT inherit BANK_ACCOUNT redefine withdraw end

feature withdraw(v: INTEGER) is require else balance >= v do

 balance := balance - v

ensure

 balance_altered: balance = balance - v

end

end

class B_A_NORMAL inherit BANK_ACCOUNT redefine withdraw end

feature withdraw(v: INTEGER) is require else balance - fee >= v do

 balance := balance -v

ensure

 balance_altered: balance = balance - v

end

feature

 fee: INTEGER

end

class B_A_BUSINESS inherit BANK_ACCOUNT redefine withdraw end

feature withdraw(v: INTEGER) is require else balance + credit >= v do

 balance := balance -v

ensure

 balance_altered: balance = balance - v

end

feature

 credit: INTEGER

end </eiffel>

Abstract Data Types (16 points)

Writing and ADT for CREDIT_CARD (7 points)

TYPES

CREDIT_CARD

FUNCTIONS

Creators:

new_card: INTEGER x INTEGER --|--> CREDIT_CARD

Queries:

limit: CREDIT_CARD ----> INTEGER

balance: CREDIT_CARD ----> INTEGER

Commands:

settle: CREDIT_CARD ----> CREDIT_CARD

charge: CREDIT_CARD x INTEGER --|--> CREDIT_CARD

PRECONDITIONS

P1 new_card (limit: INTEGER) require limit > 0

P2 charge (c: CREDIT_CARD; amount: INTEGER) require amount + balance(c) <= limit(c) and amount > 0

AXIOMS

A1 limit(new_card(l: INTEGER)) = l

A2 balance(new_card(l: INTEGER)) = 0

A3 limit(settle(c: CREDIT_CARD)) = limit(c)

A4 balance(settle(c: CREDIT_CARD)) = 0

A5 limit(charge(c: CREDIT_CARD; a: INTEGER)) = limit(c: CREDIT_CARD)

A6 balance(charge(c: CREDIT_CARD; a: INTEGER)) = balance(c: CREDIT_CARD) + a

Proof of balance properties (6 points)

Prove that balance(c) >= 0:

Base case: using A2, new_card(l)

Induction assumption: is a correct expression of type CREDIT_CARD of length , i.e.

Induction step:

using A4

using A6, induction assumption for , and P2 for


Prove that

Base case:

new_card(l: INTEGER)

using A2

using A1

Hence: using P1 for the last inequality

Induction assumption:

is a correct expression of type CREDIT_CARD and length , that is:

and

Induction step (reuse inequalities found for balance above):

(see above) and using A3 and induction assumption, hence


using P2

using A5

since above we could show that a stronger statement was true