Full textReport1997UrhG

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.

Preview

Logo BII

BII

Cite

Citation style:
Could not load citation form.

Rights

Use and reproduction:No Creative Commons license - The provisions of the German Copyright Act (UrhG) apply.Please note that individual components of the publication may be subject to other licensing or copyright conditions.