Centrale nei metodi formali è il cosiddetto Teorema della Correttezza che mette in relazione una specifica con le sue corrette Implementazioni. Questo teorema è l'obiettivo del test tradizionale del programma e, più recentemente, della verifica del programma (in cui il teorema deve essere dimostrato). Le dimostrazioni sono difficili, anche se si utilizzano potenti dimostratori di teoremi. Questo volume spiega e illustra un metodo alternativo, che consente la costruzione di algoritmi (necessariamente corretti) a partire da una specifica utilizzando trasformazioni algebriche e tecniche di raffinamento che impediscono l'introduzione di errori. Basandosi su materiale didattico ampiamente utilizzato presso l'Università di Loughborough, John Cooke introduce le nozioni di base, utilizzando semplici esempi e molti lavori dettagliati (che spesso possono essere riutilizzati). Constructing Correct Software fornirà letture preziose per studenti e professionisti di informatica e ingegneria del software per i quali la correttezza del software è di primaria importanza.
caricamento...
