Altadonna, Fabio
(2024)
Logica di Hoare applicata su un
linguaggio procedurale:
implementazione Matita.
[Laurea], Università di Bologna, Corso di Studio in
Informatica [L-DM270]
Documenti full-text disponibili:
![[img]](http://amslaurea.unibo.it/style/images/fileicons/application_pdf.png) |
Documento PDF (Thesis)
Disponibile con Licenza: Salvo eventuali più ampie autorizzazioni dell'autore, la tesi può essere liberamente consultata e può essere effettuato il salvataggio e la stampa di una copia per fini strettamente personali di studio, di ricerca e di insegnamento, con espresso divieto di qualunque utilizzo direttamente o indirettamente commerciale. Ogni altro diritto sul materiale è riservato
Download (583kB)
|
Abstract
Nell’ambito dello sviluppo del software, garantire la correttezza dei
programmi scritti ´e cruciale per fornire affidabilit´a e sicurezza. La logica di
Hoare[2], introdotta da Tony Hoare nel 1969, fornisce un approccio formale
per la specifica e la verifica della correttezza dei programmi. Tale approccio
si basa sull’idea di specificare le precondizioni e le postcondizioni per
ciascun frammento di programma, definendo la nozione di tripla di Hoare,
la quale consente di dimostrare logicamente che un determinato programma
soddisfa determinate propriet´a. Lo scopo del progetto presentato nel
documento ´e quello di utilizzare il software Matita[1], per definire la sintassi
e la semantica di un linguaggio imperativo con memoria statica (stack),
memoria dinamica (heap) e parallelismo. Dopo aver creato il linguaggio,
implementare, dimostrandone la validit´a attraverso la funzionalit´a di Proof
Assistant di Matita, le regole di inferenza sulle triple di Hoare, per
consentire in ultimo di effettuare dimostrazioni rigorose su programmi
scritti nello stesso linguaggio. Il presente documento riepiloga in primis i
concetti fondamentali riguardanti la teoria che sta alla base del sistema di
inferenze di Hoare e di come quest’ultimo dipenda dal linguaggio di
programmazione su cui si adopera. In seguito viene invece relazionato il
processo di lavoro svolto su Matita per la relativa implementazione pratica.
Abstract
Nell’ambito dello sviluppo del software, garantire la correttezza dei
programmi scritti ´e cruciale per fornire affidabilit´a e sicurezza. La logica di
Hoare[2], introdotta da Tony Hoare nel 1969, fornisce un approccio formale
per la specifica e la verifica della correttezza dei programmi. Tale approccio
si basa sull’idea di specificare le precondizioni e le postcondizioni per
ciascun frammento di programma, definendo la nozione di tripla di Hoare,
la quale consente di dimostrare logicamente che un determinato programma
soddisfa determinate propriet´a. Lo scopo del progetto presentato nel
documento ´e quello di utilizzare il software Matita[1], per definire la sintassi
e la semantica di un linguaggio imperativo con memoria statica (stack),
memoria dinamica (heap) e parallelismo. Dopo aver creato il linguaggio,
implementare, dimostrandone la validit´a attraverso la funzionalit´a di Proof
Assistant di Matita, le regole di inferenza sulle triple di Hoare, per
consentire in ultimo di effettuare dimostrazioni rigorose su programmi
scritti nello stesso linguaggio. Il presente documento riepiloga in primis i
concetti fondamentali riguardanti la teoria che sta alla base del sistema di
inferenze di Hoare e di come quest’ultimo dipenda dal linguaggio di
programmazione su cui si adopera. In seguito viene invece relazionato il
processo di lavoro svolto su Matita per la relativa implementazione pratica.
Tipologia del documento
Tesi di laurea
(Laurea)
Autore della tesi
Altadonna, Fabio
Relatore della tesi
Scuola
Corso di studio
Ordinamento Cds
DM270
Parole chiave
Hoare,Separation Logic,Matita,coq,Proof assistant,automazione prove,correttezza,Logica,Dimostrazioni
Data di discussione della Tesi
13 Marzo 2024
URI
Altri metadati
Tipologia del documento
Tesi di laurea
(NON SPECIFICATO)
Autore della tesi
Altadonna, Fabio
Relatore della tesi
Scuola
Corso di studio
Ordinamento Cds
DM270
Parole chiave
Hoare,Separation Logic,Matita,coq,Proof assistant,automazione prove,correttezza,Logica,Dimostrazioni
Data di discussione della Tesi
13 Marzo 2024
URI
Statistica sui download
Gestione del documento: