Verification Conditions – Metodi formali

In questa lezione analizzeremo le Verification Conditions (vc) e la funzione pre, che, sfruttando la Weakest Liberal Precondition (wlp) introdotta nella lezione precedente, consentono di trasformare i comandi della grammatica annotata in formule logiche caratterizzate da una precondizione e una postcondizione determinate dagli invarianti di ciclo. Concluderemo dimostrando il teorema di correttezza delle Verification Conditions, che garantisce la correttezza del programma quando tutte le condizioni generate risultano valide. Fonti principali: – H. R. Nielson, F. Nielson — Semantics with Applications: A Formal Introduction – Glynn Winskel — The Formal Semantics of Programming Languages – Tobias Nipkow, Gerwin Klein — Concrete Semantics