Lösungsvorschlag Software Architecture Endterm 2006

Aus VISki
Wechseln zu: Navigation, Suche

Exercise 3

1.

read is a partial function because it has a precondition.

2.

(a)

Correct and holds. Application of A4.

(b)

Correct and holds.

read(n,write(m,d2,write(n,d1,f))) = read(n, write(n,d1,write(m,d2,f))) [Axiom 5]
read(n,write(n,d1,f)) = read (n,write(n,d1,write(m,d2,f))) [Axiom 4]
d1 = d1

c)

Correct, but does not hold. Left hand side:

read (n,write (n,d2,write (n,d1,f))) = (A4)
d2 

Right hand side:

read (n,write (n,d1,write (n,d2,f)) = (A4)
d1

d)

Not correct.

read (n,write (m,d1,format_disk)) = (A5)
read (n, format_disk) <-- violates P1 because A1

3.

We prove sufficient completeness by structural Induction over the terms.

Let d: DATA; n,m: NAME with n != m; f: FILE_SYSTEM).

Base case: file_exists(n, format_disk) = false (A1)

read can not be executed for arbitrary n on format_disk because P1.

Step case: Induction hypothesis: Sufficient completness holds for being a subterm of T.


file_exists(n,write(n,d,f)) = true (A2)

file_exists(m,write(n,d,f)) = file_exists(m,f) (A3)


read(n,write(n,d,f)) = d (A4)

read(m,write(n,d,f)) = read(m,f) (A5)


Q.E.D.

4.

delete: NAME x FILE_SYSTEM -/-> FILE_SYSTEM


let n,m : NAME

delete(n,f) requires file_exists(n,f)


A6: file_exists(n, delete(m,f)) = false


Since we only would need to adapt the step case of the proof, and read(n, delete(n,f)) is not possible (P1), read(m, delete(n,f)) = read(m,f) because it does not affect m, and can be easily adapted similiar, the ADT is still sufficiently complete specified.