Dijkstras wp-Funktion als Formeltransformer und ihre Verbindung zur denotationellen Semantik

In diesem Artikel wird der von R. Back stammende Ansatz, schwächste Vorbedingungen durch infitären Formeln zu axiomatisieren, verfeinert, um auch Variablensubstitution in der gewohnten Weise handhabbar zu machen. Als Hauptresultat wird die Korrektheit einer rein syntaktischen wp-Funktion bezüglich des mittels denotationeller Semantik definierten Begriffs einer schwächsten Vorbedingung für totale Korrektheit bewiesen.

Vorschau

Logo BII

BII

Zitieren

Zitierform:
Zitierform konnte nicht geladen werden.

Rechte

Nutzung und Vervielfältigung:Keine Creative-Commons-Lizenz - Es gelten die Bestimmungen des dt. Urheberrechts (UrhG)Bitte beachten Sie, dass einzelne Bestandteile der Publikation anderweitigen Lizenz- bzw. urheberrechtlichen Bedingungen unterliegen können.