Lingue delle specifiche vs test automatizzati

Naviga le tue risposte
2

Recentemente ho ascoltato un episodio di Software Engineering Radio in cui è stato intervistato Leslie Lamport . Una cosa che ha discusso è stata la sua lingua delle specifiche, TLA + .

Essenzialmente, sembrava sostenere che, per i programmi in cui la correttezza è molto importante, dobbiamo riflettere attentamente e specificare attentamente prima di scrivere il codice, e TLA + è pensato per essere uno strumento per farlo. Ha detto che un team di Amazon ha recentemente avuto successo nell'utilizzarlo.

Personalmente, scrivo test eseguibili per il mio codice. Vedo i test come una specifica, che ha l'enorme vantaggio di dimostrare se il codice è conforme ad esso.

Suppongo che Mr. Laport, essendo un brillante e compiuto informatico, lo conosca da molto tempo e veda ancora il bisogno del suo linguaggio. Ma perché?

I linguaggi delle specifiche formali e i test automatizzati sono approcci complementari o in disaccordo? Si prestano a diversi tipi di codice?

    
posta Nathan Long 20.05.2014 - 14:47
fonte

2 risposte

2

I tuoi test possono mostrare che il sistema reagisce correttamente a quegli input che i test effettivamente esercitano. Questo è molto prezioso, ma è quasi impossibile esercitare gli tutti input che un programma potrebbe ricevere.

Una prova formale o un documento linguistico di specifica scelta può dimostrare matematicamente che il tuo programma risponderà correttamente a tutti input che potrebbe ricevere, anche se questo è un insieme infinito . Questo è certamente meglio, anche se lo sforzo extra vale il miglioramento dell'affidabilità varia da caso a caso.

    
risposta data 20.05.2014 - 14:51
fonte
0

Mr. Lamport, ... still sees a need for his language. But why?

Con un linguaggio di specifica formale, puoi eseguire un verificatore, che prova matematicamente il progetto / algoritmo. Questo non è lo stesso di un insieme di test unit / integration / bdd.

Are formal specification languages and automated tests complementary approaches, or at odds?

Questi sono complementari, certamente. Niente ti impedisce di utilizzarli entrambi, se necessario.

    
risposta data 20.05.2014 - 14:52
fonte

Leggi altre domande sui tag

Con quale velocità un chip dedicato può eseguire le operazioni di modulo di squadratura sequenziale per interrompere una capsula crittografica temporizzata? Come evitare un sovraccarico mentre si implementa ancora un modello di oggetto nullo?