Informationen zur \Uuml;bung 4

Informationen zur Übung 4

Aufgabe 1:
Nehmen wir als Beispiel die 1. Teilaufgabe: Wir wollen also sehen ob assignment x:= x-4 (das ist a) mit Vorbedingung x => 4 (das ist pre(a)) mit den assertions von {x => 0} <x := x +5;> {x => 5} interferiert.
Es genügt für die Aufgabe für das Beispiel: {x => 0 and x => 4} x:= x-4 {x => 0} und {x => 5 and x => 4} x:= x-4 {x => 5} zu überprüfen.
Zu Aufgabe 3: Ja, es dürfen Atomarizitätsklammern benutzt werden, jedoch sollen möglichst wenige benutzt werden und es soll möglichst wenig Code darin enthalten sein.
Bei den Aufgaben 2 und 3 sind die Punkte vertauscht: Für Aufgabe 2 gibt es 4 Punkte und fuer Aufgabe 3 gibt es 6 Punkte.
Auch der Pseudocode fuer Aufgabe 3 soll bitte kommentiert werden.
Zu <await B>: Es dient nur zur Synchronisation mit einer Bedingung (siehe auch Seite 55 im Buch).
Zu Aufgabe 2 schaut nochmal im Buch die Seiten 64/65. Noninterference wie in 2.5 definiert ist eine weitere Möglichkeiten um zwei oder mehr sequentielle statements mit der Co Statement Rule (Seite 63) zusammenfassen zu können. Eine andere Möglichkeit ist zum Beispiel die At-Most-Once Property(2.2 Seite 52). Gilt diese nicht versucht man es eben mit Noninterference(2.5).
Ein Beispiel für eine proof outline ist im Buch auf Seite 71 angegeben. Falls ihr das noch genauer nachlesen wollt, das Paper An axiomatic proof technique for parallel programs I von Susan Owicki und David Gries könnt ihr hier bei Springer herunterladen. Ihr müsst das aber aus dem Netz der Uni machen damit ihr die Lizenz der Unibibliotek verwendet.