Prima di tutto, questo è possibile solo su algoritmi che non hanno effetti collaterali?Verifica formale della correttezza di un algoritmo
In secondo luogo, dove potrei venire a conoscenza di questo processo, di buoni libri, articoli, ecc.?
COQ è un assistente di prova che produce un'uscita ocaml corretta. È piuttosto complicato però. Non sono mai riuscito a guardarlo, ma il mio collega ha iniziato e poi ha smesso di usarlo dopo due mesi. Era soprattutto perché voleva fare le cose più velocemente, ma se hai bisogno di verificare un algoritmo, questa potrebbe essere una buona idea.
Here is a course che utilizza COQ e parla degli algoritmi di prova.
E here is a tutorial sulla scrittura di articoli accademici in COQ.
anche qui, http://www.lix.polytechnique.fr/coq/getting-started – nlucaroni
Di solito le prove di correttezza sono molto specifiche dell'algoritmo in questione.
Tuttavia, ci sono diversi trucchi ben noti che vengono utilizzati e riutilizzati di nuovo. Ad esempio, con gli algoritmi ricorsivi è possibile utilizzare loop invariants.
Un altro trucco comune è la riduzione del problema originale a un problema per il quale è più semplice mostrare la dimostrazione di correttezza dell'algoritmo, quindi generalizzando il problema più facile o mostrando che il problema più semplice può essere tradotto in una soluzione al problema originale. Here è una descrizione.
Se si ha in mente un particolare algoritmo, si può fare meglio chiedendo come costruire una dimostrazione per quell'algoritmo piuttosto che una risposta generale.
Riduzione dell'algoritmo (specialmente descritto come nel link che offri) è uno strumento teorico per dimostrare che un problema è almeno altrettanto difficile di un altro. Queste prove, spesso fatte nel modello di calcolo della macchina di Turing, sono affari a mano e non hanno nulla a che vedere con prove formali (controllabili dalla macchina). Spesso sono fatti per problemi difficili da essere utili nella pratica (l'esempio nel tuo link è per il problema di Halting, mostrare un problema è NP-hard riducendo un noto problema NP-hard è anche popolare). In breve, non sono sicuro che la riduzione dei problemi, in quanto collegata, abbia qualcosa a che fare con la correttezza formale. –
Hmm forse la riduzione non è il termine corretto che dovrei usare qui. Quando dico riduzione intendevo qualcosa sulla falsariga del seguente esempio. Supponiamo che tu abbia un algoritmo che calcola l'intersezione di N rettangoli, che sai essere corretta. Supponiamo di avere un altro problema per il quale esiste una traduzione non banale di quel problema al problema di calcolare l'intersezione di N rettangoli. Quindi si utilizza il primo algoritmo per calcolare la soluzione a quest'ultimo problema.Tutto ciò che rimane è dimostrare che la traduzione è corretta. – ldog
Ma posso vedere che questo è confuso, è un trucco che si basa sul fatto che si fa uso di un algoritmo noto che è noto per essere corretto (in questo caso quello per calcolare l'intersezione di N rettangoli.) Posso vedere dove arriva la confusione se questo è un metodo per dimostrare o fornire un algoritmo corretto. – ldog
Penso che la verifica della correttezza di un algoritmo sarebbe la convalida della sua conformità con una specifica. C'è una branca di Informatica teorica chiamata Formal Methods che potrebbe essere ciò che stai cercando se hai bisogno di avvicinarti il più possibile alle prove. Da wikipedia,
metodi formali sono un particolare tipo di tecniche matematicamente basate per la specifica, lo sviluppo e verifica di software e hardware sistemi
Sarete in grado di trovare molti di apprendimento risorse e strumenti dalla moltitudine di link sulla pagina di Wikipedia collegata e dallo Formal Methods wiki.
comprare questi libri: http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800
Il libro Gries, programmazione scientifica è roba grande. Paziente, completo, completo.
E se ti piace Z, sii sicuro che troverai gli strumenti per incorporarlo nel processo di scrittura di un algoritmo formalmente corretto: http : //www.bmethod.com/php/methode-b-en.php –
Logic in Computer Science, di Huth e Ryan, offre una panoramica ragionevolmente leggibile dei sistemi moderni per la verifica dei sistemi.C'era una volta che la gente parlava di provare i programmi corretti - con linguaggi di programmazione che possono o meno avere effetti collaterali. L'impressione che ottengo da questo libro e da altre parti è che le applicazioni reali sono diverse, ad esempio dimostrando che un protocollo è corretto o che l'unità in virgola mobile di un chip può dividere correttamente o che una routine di blocco per manipolare le liste collegate è corretta.
ACM Computing Surveys Vol 41 Numero 4 (ottobre 2009) è un numero speciale sulla verifica del software. Sembra che puoi ottenere almeno uno dei documenti senza un account ACM cercando "Metodi formali: pratica ed esperienza".
"I metodi formali" racchiudono tutti gli obiettivi citati. Sono nel sottocampo di "provare i programmi corretti" e devo ammettere che fino ad ora i grandi successi industriali provenivano dagli altri sotto-campi (basta aspettare fino al prossimo anno!). Una conferenza come FMWEEK è piuttosto sconcertante perché riunisce persone con tutti questi approcci e obiettivi diversi, ma abbiamo molto in comune e molto scambio. –
Lo strumento Frama-C, per il quale Elazar suggerisce un video dimostrativo nei commenti, fornisce un linguaggio delle specifiche, ACSL, per scrivere contratti di funzione e vari analizzatori per verificare che una funzione C soddisfi il suo contratto e le proprietà di sicurezza come l'assenza degli errori di runtime.
Un'esercitazione estesa, ACSL by example, mostra esempi di algoritmi C effettivi specificati e verificati e separa le funzioni senza effetti collaterali da quelle efficaci (quelle senza effetti collaterali sono considerate più semplici e vengono prima nel tutorial). Questo documento è anche interessante in quanto non è stato scritto dai progettisti degli strumenti che descrive, quindi dà un aspetto più fresco e più didattico a queste tecniche.
Se si ha familiarità con LISP allora si dovrebbe verificare ACL2: http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html
di Dijkstra Disciplina della Programmazione e dei suoi EWDS gettare le basi per la verifica formale come una scienza in programmazione. Un'opera più semplice è la programmazione sistematica di Wirth, che inizia con il semplice approccio all'utilizzo della verifica. Wirth utilizza pre-ISO Pascal per la lingua; Dijkstra usa un formalismo simile ad Algol 68 chiamato Guarded (GCL). La verifica formale è maturata da Dijkstra e Hoare, ma questi testi più vecchi possono ancora essere un buon punto di partenza.
Lo strumento PVS sviluppato da Stanford è un sistema di specifica e verifica. Ci ho lavorato e l'ho trovato molto utile per Theoram Proving.
WRT (1), sarà probabilmente necessario creare un modello dell'algoritmo in modo da "catturare" gli effetti collaterali dell'algoritmo in una variabile di programma intesa a modellare tali effetti collaterali basati sullo stato.
Non sono sicuro di cosa intendi sugli effetti collaterali. – ldog
Vedi questo: http://en.wikipedia.org/wiki/Side_effect_%28computer_science%29 – joemoe
Vedi http://stackoverflow.com/questions/476959/why-cant-programs-be-proven che ha alcune buone risposte. –