Introduzione alla verifica del software con il linguaggio Dafny: Dimostrare la correttezza dei programmi

Recensioni dei lettori

Attualmente non ci sono recensioni dei lettori. La valutazione si basa su 2 voti.

Titolo originale:

Introducing Software Verification with Dafny Language: Proving Program Correctness

Contenuto del libro:

Introducetevi alla verifica del software e alla dimostrazione della correttezza utilizzando il linguaggio di programmazione Dafny, sostenuto da Microsoft Research. Mentre altri libri su questo argomento sono piuttosto rigorosi dal punto di vista matematico, questo libro utilizzerà il minor numero possibile di simboli matematici e di rigore, spiegando ogni concetto con un linguaggio semplice. È il primo passo perfetto per i programmatori e gli sviluppatori di software con competenze in C# e altri linguaggi di programmazione.

Scrivere software corretto può essere difficile, quindi imparerete il concetto di calcolo e di verifica del software. Quindi, applicherete questi concetti e queste tecniche per scrivere con sicurezza codice privo di bug e facile da capire. Il codice sorgente sarà disponibile in tutto il libro e liberamente consultabile su GitHub.

Dopo aver letto e utilizzato questo libro, sarete in grado di scrivere codice sorgente di software libero corretto e di grandi dimensioni, applicabile indipendentemente dalla piattaforma e dal linguaggio di programmazione utilizzati.

Cosa imparerete

⬤ Scoprire il linguaggio di programmazione Dafny, sostenuto da Microsoft Research.

⬤ Esplorare la logica di Hoare, i programmi imperativi e funzionali.

⬤ Lavorare con pre e postcondizioni.

⬤ Utilizzare tipi di dati, pattern matching e classi.

⬤ Tuffarsi in esempi di verifica per un potenziale riutilizzo nei propri progetti.

Per chi è questo libro?

Sviluppatori e programmatori di software con almeno una precedente esperienza di programmazione di base. Non è necessario un linguaggio specifico. È anche per coloro che hanno un'esperienza matematica di base (funzioni, variabili).