Logica di Hoare applicata su un linguaggio procedurale: implementazione Matita

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.