Discussione sull’integrazione di strumenti di verifica formale nella programmazione quotidiana

Il presente studio propone un uso non convenzionale di Why3, uno strumento di verifica formale. Viene definita una strategia che guida il programmatore all’uso atipico di questo strumento. Il metodo proposto aiuterebbe a trovare un compromesso tra formalità ed efficienza nello sviluppo software. Questo approccio viene analizzato e studiato attraverso casi di studio reali: esercizi su problemi isolati ed un progetto. Queste attività hanno generato una serie di deduzioni e conclusioni, che sostanzialmente compongono l’elaborato.