Unità didattica
Titolo del corso
Modelli della Concorrenza
Codice identificativo del corso
2223-1-F1801Q132-F1801Q132M
Lezione del 17 ottobre
Aggregazione dei criteri
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".