Operationale Semantik und Fairness

Zusammenfassung

Durch Fairnessvorgaben sollen Ausführungen ausgeschlossen werden, in denen eine atomare Aktion anderen gegenüber benachteiligt wird. Im Rahmen einer operationalen Semantik kann der Fairnessbegriff bereits für sequentielle Programme mit atomaren Aktionen sinnvoll formalisiert werden. Wir definieren in diesem Kapitel daher zunächst die Syntax und dann die Operationale Semantik einer sequentiellen Programmiernotation mit atomaren Aktionen, genannt APROG . Die Fairnessdefinitionen werden auf dieser Semantik aufgebaut. Die Sprache APROG ist eine Erweiterung der sequentiellen nichtdeterministischen Notation USEQPROG des Kapitels 3. Noch lassen wir jedoch keine parallelen Sprachkonstrukte zu. Die neue Sprache kann alternativ auch als eine Version der Sprache der sequentiellen Kontrollprogramme aufgefaßt werden, worin die Elemente von A konkretisiert sind, d.h. Zuweisungen und andere Anweisungen enthalten dürfen.