Lösungsvorschlag Formal Methods and Functional Programming FS07

Aus VISki
Wechseln zu: Navigation, Suche

Assignment 1 (Set Theory)

1.1)




1.2)

1.3)

Assignment 2 (Model of an Access Control System)

2.1)

inv0_2:

2.2)

2.3)

enter/inv0_2/INV:









2.4)

enter/inv0_2/INV









FUN

FUN Branch 1:








MON






HYP

FUN Branch 2:








MON






HYP

2.5)

Aufgabe 2.5 entspricht Exercise 14.5. Die Lösung dazu ist jetzt online.


DLF








XST_L, XST_R, CASE

CASE Branch 1:

MON








OR_R1






HYP

CASE Branch 2:

MON, Rewriting








OR_R2







CASE

CASE Branch 1:








AND_L, OR_R1






HYP

CASE Branch 2:








Rewriting , AND_L, OR_R2






XST_R with r=H, HYP

Assignment 3 (Refinement of Access Control System)

Bin mir nicht ganz sicher: Vorsicht!

3.1)

Ich glaube eine einfachere Lösung wäre: Ist symmetrisch. (Slide 168 in math)

3.2)


3.3)


3.4)

Work in progress.png

Diese Aufgabe wurde noch von niemandem gelöst und wartet noch immer auf einen Musterlöser.
Hast du dieses Fach bereits besucht? Hilf mit, die Qualität dieser Seite zu verbessern, indem du eine plausible Lösung für diese Frage notierst!

Assignment 4 (Euclid's Algorithm)

4.1)

4.2)

m>n

4.3)

m<n

4.4)

n:= n-m

4.5)

Genau gleich wie exercise 13, Third Refinement. M_IF, M_WHILE, M_INIT