Cosa serve per dimostrare che due programmi complicati sono equivalenti?

Question

Supponiamo che volessi dimostrare che due programmi erano equivalenti (o rigorosamente se possibile, o in modo informale altrimenti).Più specificamente, supponiamo di avere qualcosa di relativamente complesso come un server HTTP implementato in C e uno implementato in Node.js/JavaScript.Cosa posso fare per dire "questi due sono effettivamente la stessa cosa"?Quali sono le mie opzioni?Cosa è possibile?Cosa non è possibile?

È passato un po' di tempo dall'ultima volta che ho cercato di dimostrare l'equivalenza dei programmi (sono attualmente collegato a Questo, ma non riesco ancora a leggerlo ahah, e sembra che si concentri su programmi estremamente semplici come controlli di uguaglianza o cicli di base, mentre io sto chiedendo di un robusto server HTTP).

Essenzialmente (immagino) voglio dire "questi due programmi in JS e C fanno la stessa cosa".Quello "fare la stessa cosa" è ovviamente vago, ma allo stesso tempo significa qualcosa di specifico.Qualsiasi risultato osservabile su entrambi i sistemi è generalmente lo stesso, prendere o lasciare.Quindi è come una prova, ma senza essere una perfetto prova.È come se fosse una prova parziale o qualcosa del genere.

Vorrei poter dire dei miei programmi "queste due implementazioni sono equivalenti a tutti gli effetti".Probabilmente inizierei fornendo garanzie misurabili o osservazioni sulle prestazioni e sul comportamento di input/output, quindi scriverei alcuni test e...Non ricordo bene, in qualche modo faccio dichiarazioni sul sistema.O dovrei semplicemente pensare che "un server HTTP funzionante in entrambe le lingue è un ASSIOMA".Ciò lo semplificherebbe :) Supponiamo che faccia la stessa cosa l'uno con l'altro.Ma sembra che questo sia elusivo.

Ti chiedi quali sono le mie opzioni qui?Fino a che punto posso spingermi in teoria?Non mi interessa quanto tempo ci vorrà per implementarlo o definirlo, se ci vorranno anni, bene.Vorrei solo sapere cosa è possibile in termini di rendere l'affermazione "questi due programmi in C e JS sono equivalenti" più rigorosa e precisa.Quali tecniche/teorie/direzioni di ricerca potrei esaminare per renderlo possibile?

In questo momento sono giusto assumendo sono implicitamente uguali, consentendo al mio codice di chiamare la funzione C o la funzione JS sapendo che l'~effetto complessivo~ è lo stesso (nebuloso, lo so, non so come definirlo).Vorrei applicare un po' di matematica, controllo del modello, simulazione del programma o qualcosa del genere in modo da poterlo rendere più solido, se possibile :)

All’altra estremità dello spettro c’è la dimostrazione di ciò 3 > 2 è equivalente sia in C che in JS.Cosa dovrei fare in questo semplice caso?Rendendo tutto leggermente più complesso nel percorso verso un server HTTP completo, copiare una stringa in C è molto diverso rispetto a JavaScript, ma è una cosa relativamente semplice.Da dove comincio a dimostrare quelle "operazioni" equivalenti tra le due lingue?Oppure, se non "provare", allora semplicemente "dichiarare" che sono equivalenti, con qualche prova di supporto o qualcosa del genere, non lo so.

Qui non è molto, ma questo diagramma è ciò che fondamentalmente sto cercando di fare:

A un livello più ampio, il problema sembra essere simile a questo….Diciamo che voglio prendere un medaglione.Posso andare al negozio e comprarne uno oppure posso stamparne uno in 3D.Entrambi gli "algoritmi" (andare al negozio o stampare in 3D) sono molto diversi l'uno dall'altro, ma sono effettivamente gli stessi.Non ci sarebbe un modo semplice per dimostrare passo passo che questi sono equivalenti operativamente (da quello che mi fornisce la fantasia), ma visibilmente il risultato finale è lo stesso.Come lo diresti (anche qui) con rigore?

Answer 1

L'analisi formale oggi viene solitamente eseguita a livello di modulo o unità.Sfortunatamente non sono a conoscenza di una metrica comune che permetta di prevedere se un'analisi formale sarà possibile.Solo i codici strutturalmente molto semplici possono essere analizzati formalmente anche con LOC o complessità ciclomatiche fino a un milione.

Nel tuo caso qui il codice di uno qualsiasi dei due programmi è chiaramente troppo complesso per un'analisi formale completa:

• Il controllo del modello non funzionerà.
• Nemmeno una (bi-)simulazione completa funzionerà.

Quindi la migliore soluzione pratica che conosco è test basati su modelli.Sebbene non sia una prova, è comunque possibile utilizzare metodi formali.Alla fine elimina il disastro della scrittura e del mantenimento di casi di test scritti manualmente.

PS:

Un breve elenco di passaggi che possono essere eseguiti in questo caso:

• Viene creato un modello astratto dei due programmi.Questa è una terza implementazione che ometterà tutti i dettagli non importanti.L'astrazione ha il vantaggio che questo modello è abbastanza semplice da poter essere analizzato formalmente.Il modello può essere implementato in qualsiasi lingua tu voglia se l'analizzatore del modello analizzerà il codice byte.
• Il modello astratto può essere attraversato e ad es.una condizione di copertura viene raggiunta in una suite di test.Questo passaggio viene eseguito utilizzando uno strumento di test basato su modello.
• Infine questi casi di test vengono testati sui due programmi e viene verificato se il modello astratto può simulare le due implementazioni del programma.
• Questa relazione di simulazione ovviamente non è una prova di equivalenza.
• L'astrazione è una specifica molto chiara di ciò che è stato preso in considerazione nei nostri test e di ciò che è stato omesso.
• Due strumenti di test basati su modelli che possono essere consigliati:Microsoft Spec Explorer, Conformiq Designer

Answer 2

Si potrebbe scrivere un intero libro esaminando le tecniche per dimostrare l'equivalenza dei programmi.Questa risposta è solo un punto di partenza molto breve:

In teoria, se pensate ai vostri programmi come a Macchine di Turing, allora ogni speranza è perduta: dimostrare che due TM hanno lo stesso linguaggio (cioè sono semanticamente equivalente) è indecidibile (infatti non è in RE$ azza$ nucleo).

Ancora in teoria, se pensi ai tuoi programmi come macchine a stati finiti, includendo gli stati della memoria come parte della macchina, l'equivalenza del programma per i DFA è molto semplice (risolvibile in NL) e per gli NFA è PSPACE completo.Il problema con questo approccio è che lo spazio degli stati sarebbe enorme (ad esempio, se hai solo 100 bit di memoria, il tuo spazio degli stati ha almeno $2^{100}$ membri), quindi ciò è irragionevole.

Ora che abbiamo superato i limiti teorici, esiste un immenso lavoro che affronta questi argomenti, compresi i modi per definire la semantica operativa.

Fondamentalmente, questo è il campo di Verifica formale, e solo alcune parole chiave che possono aiutarti a iniziare:

• Controllo del modello
• Bisimulazione
• Astrazione - Raffinatezza
• Dimostratori di teoremi (ad esempio, Coq)

Tieni presente che in pratica molte aziende stanno verificando formalmente il proprio codice.Per l'hardware, questa è una pratica comune e rappresenta una fase importante nello sviluppo.Per il software, l'enorme complessità significa che solo piccoli frammenti di codice vengono dimostrati formalmente, mai interi programmi (non ancora, almeno).