Section outline
-
Triple di Hoare
- Regole di inferenza pre e post.
- Assiomi per skip, assegnamento semplice e assegnamento multiplo
- Espressioni definite e non
- Regole per assegnamento e per sequenza di comandi
- Variabili di specifica
- Regola per comando condizionale
- Esempi di verifica di Triple di Hoare.
Dispense: [LdH], fino a pag 23.
- Regole di inferenza pre e post.