I metodi formali possono essere utilizzati per specificare, provare e generare codice per un'applicazione. Questo è meno incline agli errori, quindi utilizzato principalmente nei programmi di sicurezza / critici.
Perché non lo usiamo più spesso per la programmazione quotidiana, o nelle applicazioni web, ecc ...?
Riferimenti:
Un ingegnere è una persona che può fare con un dollaro quello che qualsiasi idiota può fare con 10.
Limitazioni alle risorse, vincoli di budget, vincoli di tempo, sono tutti importanti.
Lo sviluppo di software utilizzando metodi formali è in genere significativamente più costoso e richiede molto più tempo del dovuto. Inoltre, per molti progetti, la parte più difficile è capire i requisiti aziendali. Tutto ciò che utilizza metodi formali ti compra in quel caso è la prova che il tuo codice corrisponde al 100% alla tua comprensione incompleta e errata dei requisiti aziendali.
Per questo motivo, l'uso di metodi formali, prove, verifica del programma e tecniche simili è tipicamente limitato a "cose che contano", cioè software avionico, sistemi di controllo per apparecchiature mediche, centrali elettriche, ecc.
Per risolvere un problema con un prodotto software, dopo aver compreso i requisiti, è possibile scrivere un programma utilizzando i linguaggi di programmazione OPPURE specificare il programma utilizzando un linguaggio formale e utilizzare gli strumenti di generazione del codice. Quest'ultimo aggiunge solo un livello di astrazione.
L'approccio formale ti dà una prova che il tuo software funziona secondo le specifiche. Quindi il tuo prodotto fa le cose per bene. Ma fa le cose giuste?
I requisiti su cui stai lavorando potrebbero essere incompleti o ambigui. Potrebbero persino essere bacati. Nel peggiore dei casi, i reali bisogni non sono nemmeno espressi. Ma un'immagine vale più di mille: solo immagini google per "Cosa vuole il cliente" (ad esempio picture here ).
In un mondo perfetto, avresti requisiti completamente dettagliati e perfetti sin dall'inizio. Potresti quindi specificare completamente il tuo software. Se andassi in modo formale, il tuo codice verrebbe generato automaticamente in modo da renderti più produttivo. I guadagni di produttività compenserebbero il costo degli strumenti formali. E tutti ora userebbero metodi formali. Quindi perché non è vero?
In pratica, questa è raramente realtà! Questo è il motivo per cui così tanti progetti waterfall non sono riusciti e perché iterativo (agile, RAD, ecc.) hanno preso il comando: possono gestire requisiti, progetti e implementazioni incompleti e imperfetti e perfezionarli finché non sono a posto.
E qui arriva il punto. Con i metodi formali, ogni iterazione richiede di avere una specifica formale completamente coerente. Ciò richiede un pensiero attento e un lavoro supplementare, perché la logica formale non è indulgente e non ama i pensieri incompleti. Semplici esperimenti throw-away diventano costosi sotto questo limite. E così ogni iterazione che porterebbe al backtracking (ad esempio un'idea che non ha funzionato, o un requisito che è stato frainteso).
Se non sei obbligato a utilizzare metodi formali per ragioni legali o contrattuali, puoi anche ottenere una qualità molto elevata senza sistemi formali, ad esempio utilizzando programmazione a contratto e altre buone pratiche (ad es. revisione del codice, TDD , ecc ...) . Non sarai in grado di dimostrare che il tuo software funziona, ma i tuoi utenti apprezzeranno presto il software di lavoro.
Nel numero di ottobre 2018 di Comunicazioni dell'ACM c'è un'interessante articolo su Software verificato formalmente nel mondo reale con alcune stime dello sforzo.
È interessante notare che (sulla base dello sviluppo del sistema operativo per le apparecchiature militari), sembra che la produzione di un software formalmente provato richieda 3,3 volte più sforzo rispetto alle tecniche di ingegneria tradizionali. Quindi è davvero costoso.
Dall'altro lato, richiede 2,3 volte meno sforzi per ottenere un software di sicurezza elevata in questo modo rispetto al software tradizionale se si aggiunge lo sforzo per rendere tale software certificato ad alto livello di sicurezza (EAL 7). Quindi, se si dispone di alta affidabilità o requisiti di sicurezza, esiste definitivamente un caso aziendale per diventare formali.
Ogni programma in qualsiasi lingua può essere pensato come una specifica formale (equivalente ad alcuni tornitori). Qualsiasi altro livello "specifica formale" da utilizzare per dimostrare la correttezza formale è anche - solo un altro programma. Ma è (tipicamente) un programma cattivo, incompleto, vago, insufficientemente pensato. E non a caso, in genere scritti da persone che non sanno come programmare (di solito sono esperti di dominio).
E così dimostrando che un programma è compatibile (produce le stesse risposte o comunque lo si caratterizza) con i suoi requisiti formali di livello più alto, invariabile dipende da come si risolvono le ambiguità nella specifica formale di livello superiore. Non esiste un buon modo per farlo in generale.
Questa mappatura dei requisiti di alto livello ai dettagli di livello inferiore è l'essenza di ciò che riguarda la programmazione reale. Non dovrebbe sorprendere il fatto che il lavoro di base svolto da un programmatore che legge e interpreta le specifiche non può essere sostituito da ondeggiamento a mano e dicendo "ora basta vedere se questa specifica di alto livello è soddisfatta da questo programma di esempio".
Anche nei primi tempi della programmazione logica, dove questo concetto sembrava inizialmente così promettente (perché sia la specifica di alto livello che i programmi reali sottostanti potevano essere scritti nella stessa lingua), questo problema centrale si dimostrò intrattabile.
Leggi altre domande sui tag code-quality development-process formal-methods