Section outline
-
- Linguaggio imperativo minimo: sintassi con grammatica BNF
- Stato di un programma
- Semantica delle espressioni
- Significato informale dei comandi
- Asserzioni: soddisfazione di un'asserzione in uno stato
- Definizione di Triple di Hoare: definizione di tripla soddisfatta
- Interpretazione di triple di Hoare: semantica, correttezza, specifica
Dispense: [LdH], fino a pag 20.
- Linguaggio imperativo minimo: sintassi con grammatica BNF