Unità didattica
Course full name
Concurrent Models
Course ID number
2223-1-F1801Q132-F1801Q132M
Lezione del 17 ottobre
Completion requirements
15:30-17:30, aula U4-02
Riassunto
- Programmi come trasformatori di stato; computazione come cammino in un grafo
- Schema generale di una dimostrazione di correttezza
- La logica di Hoare nella pratica: design by contract, Eiffel, Java Modeling language
- La logica di Hoare come fondamento di una semantica dei programmi
- Esercizi
Attenzione: nel diagramma a pagina 7 del file mdc-finale.pdf la regione associata alla formula "s" dovrebbe contenere tutti gli stati nell'intersezione di "i" e "non B".