Nove regole per validare formalmente gli algoritmi Rust con Dafny (Parte 2)

Nove regole per la validazione formale degli algoritmi Rust con Dafny (Parte 2)

Lezioni da Verificare la Crate range-set-blaze

Di Carl M. Kadie e Divyanshu Ranjan

Questo è il Parte 2 di un articolo che verifica formalmente un algoritmo Rust utilizzando Dafny. Esaminiamo le regole dalla 7 alla 9:

• 7. Porta il tuo Algoritmo Reale a Dafny.
• 8. Convalida la Versione di Dafny del Tuo Algoritmo.
• 9. Riorganizza la Convalida per Affidabilità.

Vedi Parte 1 per le regole dalla 1 alla 6:

• I ricercatori della CMU introducono MultiModal Graph Learning (MMGL) un nuovo framework di intelligenza artificiale per catturare informazioni da molteplici vicini multimodali con strutture relazionali tra di loro.
• 5 Idee per promuovere l’impegno dei data scientist/analisti senza soffocare in riunioni
• CountVectorizer per estrarre le caratteristiche dai testi in Python, in dettaglio

1. Non Imparare Dafny.
2. Impara Dafny.
3. Definisci i Concetti di Base del tuo Algoritmo.
4. Specifica il Tuo Algoritmo.
5. Ottieni Aiuto dalla Comunità di Dafny.
6. Convalida un Algoritmo Diverso, più Semplice.

Le regole sono basate sulla nostra esperienza nella convalida di un algoritmo da range-set-blaze, una crate Rust per la manipolazione di insiemi di numeri interi “aggrumati”.

Ricordiamo che la Regola 6, da Parte 1, mostra che possiamo verificare un algoritmo per InternalAdd, ma non è l’algoritmo utilizzato nella crate Rust. Ci rivolgiamo a quell’algoritmo successivamente.

Regola 7: Porta il tuo Algoritmo Reale a Dafny.

Ecco la funzione Rust di interesse con del codice escluso per ora:

// https://stackoverflow.com/questions/49599833/how-to-find-next-smaller-key-in-btreemap-btreeset// https://stackoverflow.com/questions/35663342/how-to-modify-partially-remove-a-range-from-a-btreemapfn internal_add(&mut self, range: RangeInclusive<T>) {    let (start, end) = range.clone().into_inner();    assert!(        end <= T::safe_max_value(),        "end must be <= T::safe_max_value()"    );    if end < start {        return;    }    //... il codice continua ...}

Ecco l’inizio della portabilità in Dafny:

method InternalAdd(xs: seq<NeIntRange>, range: IntRange) returns (r: seq<NeIntRange>)  requires ValidSeq(xs)  ensures ValidSeq(r)  ensures SeqToSet(r) == SeqToSet(xs) + RangeToSet(range){  var (start, end) := range;  if end < start {    r := xs;    return;  } //... il codice continua ...}

Alcuni punti di possibile interesse:

• Il codice Rust utilizza self e l’incapsulamento simile a quello orientato agli oggetti. Dafny supporta questo stile di programmazione, ma – per semplicità – in questo caso non lo utilizzo. In particolare, il codice Rust modifica self. Ho scelto di scrivere il codice Dafny in modo più funzionale: prende una sequenza immutabile e restituisce una nuova sequenza immutabile.
• Il codice Rust gestisce la memoria con il borrow checker. Ciò porta a espressioni come range.clone(). Dafny gestisce la memoria con un garbage collector. In entrambi i casi, la sicurezza della memoria sarà gestita. Pertanto, la ignoriamo in questa convalida.
• Il codice Rust è generico su T che definisco altrove per includere tutti i tipi di interi standard Rust, ad esempio, u8, isize, i128. Il codice Dafny è definito su int, un singolo tipo che rappresenta interi di dimensioni arbitrarie. Questo significa che questa porta di Dafny non deve controllare gli overflow di interi. [Vedi un articolo precedente per la dimostrazione formale della sicurezza degli overflow con il verificatore Kani Rust.]
• Il codice Rust include un assert a tempo di esecuzione che è necessario in Rust per vietare un caso speciale: l’inserimento di u128::max_value in un RangeSetBlaze<u128>. Poiché Dafny utilizza int di dimensione arbitraria, ignora questo caso speciale.

Nota: Qual è la lunghezza dell’intervallo Rust inclusivo 0..=u128::max_value? La risposta è u128::max_value+1, un valore troppo grande da rappresentare con qualsiasi tipo di intero Rust standard. La libreria range-set-blaze limita gli intervalli a 0..=u128::max_value-1, in modo che le lunghezze possano essere rappresentate con un u128.

Consideriamo ora il resto dell’algoritmo internal_add. Ricordiamo che abbiamo una lista di intervalli disgiunti ordinati e un nuovo intervallo non vuoto che vogliamo inserire. Ad esempio

L’algoritmo ci fa trovare quale (se presente) intervallo esistente si trova prima (o al) dell’inizio del nuovo intervallo. Chiamiamo questo intervallo “prima”. Consideriamo quindi quattro casi:

• Caso 1: Il nuovo intervallo non tocca il suo intervallo precedente, quindi inseriamo il nuovo intervallo controllando se tocca altri intervalli.
• Caso 2: Il nuovo intervallo tocca l’intervallo precedente ed si estende oltre di esso, quindi estendiamo la fine dell’intervallo precedente controllando se tocca altri intervalli. (Quando non vengono toccati altri intervalli, questo sarà molto veloce.)

• Caso 3: Il nuovo intervallo tocca l’intervallo precedente ma non si estende oltre di esso, quindi non facciamo nulla. (Questo sarà sempre molto, molto veloce.)

• Caso 4: Il nuovo intervallo inizia prima di qualsiasi intervallo, quindi lo aggiungiamo controllando se tocca altri intervalli.

Ecco l’algoritmo in Rust:

// codice continuato ...// FUTURO: sarebbe bello avere una funzione partition_point in BTreeMap che restituisca due iteratori    let mut before = self.btree_map.range_mut(..=start).rev();    if let Some((start_before, end_before)) = before.next() {        // Bisogna controllare questo in due parti per evitare l'overflow        if match (*end_before).checked_add(&T::one()) {            Some(end_before_succ) => end_before_succ < start,            None => false,        } {            self.internal_add2(&range);        } else if *end_before < end {            self.len += T::safe_len(&(*end_before..=end - T::one()));            *end_before = end;            let start_before = *start_before;            self.delete_extra(&(start_before..=end));        } else {            // completamente contenuto, quindi non fare nulla        }    } else {        self.internal_add2(&range);    }}

Ecco invece in Dafny:

// codice continuato ...  var beforeHi := IndexAtOrBeforePlusOne(xs, start);  if beforeHi > 0 { // non va all'inizio    var (startBefore, endBefore) := xs[beforeHi-1];    if endBefore+1 < start {      r := InternalAdd2(xs, range);    } else if endBefore < end {      r := xs[..beforeHi-1] + [(startBefore, end)] + xs[beforeHi..];      assume exists i: nat :: i < |r| && r[i] == (startBefore,end) && ValidSeq(r[..i+1]) && ValidSeq(r[i+1..]);      r := DeleteExtra(r, (startBefore,end));    } else{      r := xs;    }  }  else // va all'inizio  {    r := InternalAdd2(xs, range);  }}

Alcuni punti di possibile interesse:

• Il codice Rust manipola una BTreeMap tramite chiavi e valori. Il codice Dafny manipola una seq ordinata con indici (accesso casuale). Ho fatto in modo che le operazioni Dafny riflettano le operazioni Rust, anche se questo rende il codice Dafny meno naturale.
• Il codice Rust aggiorna anche self.len, il numero di interi individuali nel RangeSetBlaze. Il codice Dafny ignora questo. (L’aggiornamento di len è una funzionalità che potrebbe essere aggiunta al codice Dafny in futuro.)
• Come prima, la versione Rust include del codice per evitare l’overflow che Dafny ignora.

Ho proseguito la porting scrivendo una versione Dafny del internal_add2 e delete_extra, le due funzioni che internal_add chiama. Ho completato il porting scrivendo i metodi che queste due funzioni chiamano, ecc. Il porting completo è di circa 185 righe di codice. Puoi vederlo qui.

Non valida. Lavoreremo sulla validazione successiva.

Regola 8: Valida la versione Dafny del tuo algoritmo.

In questo passaggio, aggiungerai suggerimenti di validazione al tuo codice, ad esempio sotto forma di istruzioni assert. Dafny utilizza questi suggerimenti per cercare di convalidare il tuo codice. Come principiante di Dafny, ho trovato più difficile aggiungere suggerimenti che scrivere il codice. In parte perché non sapevo quando (o se) Dafny sarebbe stato soddisfatto e avrei potuto fermarmi.

Tuttavia, ho imparato come dovrei iniziare. Ad esempio, il codice sopra per InternalAdd produce due errori di verifica. Prima, il verificatore di Dafny segnala che uno dei ensures potrebbe non essere verificato:

Questa postcondizione potrebbe non essere verificata: SeqToSet(r) == SeqToSet(xs) + RangeToSet(range)

N.B.: “Postcondizione” corrisponde a ensures. “Precondizione” corrisponde a requires.

In secondo luogo, il verificatore di Dafny si lamenta che una precondizione (cioè uno dei requires) per DeleteExtra non può essere dimostrata.

Prima ci concentreremo sul primo problema aggiungendo un assert alla fine del metodo. Lo scriviamo in modo da riflettere l’ ensures.

// ... aggiungendo questo come l'ultima riga in InternalAdd assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range);}

Ignoreremo esplicitamente il problema di DeleteExtra, per ora, con un assume.

// ... assume esiste i: nat :: i < |r| && r[i] == (startBefore,end) && ValidSeq(r[..i+1]) && ValidSeq(r[i+1..]); r := DeleteExtra(r, (startBefore,end));//...

Il validatore di Dafny ora si lamenta solo del nostro nuovo assert finale. Dice “l’assezione potrebbe non essere verificata”.

Ricordiamo che il codice di InternalAdd utilizza istruzioni if annidate per suddividere il lavoro in cinque casi. Successivamente sposteremo il nostro assert dalla fine del metodo alla fine di ogni caso. Cerchiamo le linee che terminano con un commento // case nel risultato:

method InternalAdd(xs: seq<NeIntRange>, range: IntRange) returns (r: seq<NeIntRange>) requires ValidSeq(xs) ensures ValidSeq(r) ensures SeqToSet(r) == SeqToSet(xs) + RangeToSet(range){ var (start, end) := range; if end < start { r := xs; assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // caso 0 - convalida return; } var beforeHi := IndexAtOrBeforePlusOne(xs, start); if beforeHi > 0 { // non va all'inizio var (startBefore, endBefore) := xs[beforeHi-1]; if endBefore+1 < start { r := InternalAdd2(xs, range); assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // caso 1 - convalida } else if endBefore < end { r := xs[..beforeHi-1] + [(startBefore, end)] + xs[beforeHi..]; assume esiste i: nat :: i < |r| && r[i] == (startBefore,end) && ValidSeq(r[..i+1]) && ValidSeq(r[i+1..]); r := DeleteExtra(r, (startBefore,end)); assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // caso 2 - fallisce } else{ r := xs; assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // caso 3 - fallisce } } else // va all'inizio { r := InternalAdd2(xs, range); assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // caso 4 - convalida }}

Dafny ci dice ora che i casi 0, 1 e 4 sono validi. Il caso 2 fallisce (e contiene quella assume che alla fine dovremo rimuovere). Per ora, però, lavoriamo sul caso 3.

Ricordate dalla regola 7 di questo articolo, che il caso 3 è quando aggiungiamo un nuovo intervallo (rosso) che è completamente coperto da un intervallo esistente (l’intervallo blu “prima”), quindi il codice non ha bisogno di fare nulla.

Quindi, pensando logicamente, cosa sappiamo? Sappiamo che gli interi coperti dall’intervallo precedente sono un superset degli interi coperti dal nuovo intervallo. Sappiamo anche che l’intervallo precedente fa parte della nostra lista originale ordinata e disgiunta di intervalli (gli intervalli blu). Aggiungeremo questi due suggerimenti al nostro codice tramite le dichiarazioni di assert:

Dafny concorda che questi due suggerimenti sono veri (segno di spunta verde), ma ancora non accetta l’assert di interesse (segnale rosso).

Sembra che abbiamo bisogno di un altro suggerimento. In particolare, dobbiamo convincere Dafny che gli interi coperti dall’intervallo precedente sono un sottoinsieme degli interi coperti dalla lista di tutti gli intervalli ordinati e disgiunti. Intuitivamente, questo è vero perché l’intervallo precedente è uno degli intervalli nella lista.

Scriviamo questo suggerimento come un lemma senza corpo. Dafny lo accetta.

Nota: Perché Dafny accetta questo lemma senza niente nel suo corpo? Non lo so e non ho una buona intuizione. Ha semplicemente funzionato. Se non lo avesse fatto, avrei provato ad aggiungere degli assert al corpo del lemma.

Utilizzando il lemma, il caso 3 ora è valido:

Questo significa che abbiamo validato i casi 0, 1, 3 e 4. Successivamente passeremmo al caso 2. Inoltre, alcuni dei metodi menzionati, ad esempio DeleteExtra, non sono ancora validi e dovremmo lavorare su quelli. [Puoi vedere il codice fino a questo punto, qui.]

Per consigli generali sul debug della verifica, consulta questa sezione della Guida dell’Utente di Dafny. Consiglio anche questa risposta di Stack Overflow e mini-tutorial del Prof. James Wilcox.

Nel complesso, l’idea è suddividere il compito di convalidare il proprio algoritmo in molti compiti di convalida più piccoli. Ho trovato questo più difficile della programmazione, ma non troppo difficile e comunque divertente.

Ho finito per aggiungere circa 200 righe di convalida alle 185 righe di codice regolari (codice completo qui). Quando ho finalmente convalidato l’ultimo metodo, ho pensato erroneamente di aver finito.

A mia sorpresa (e delusione) il lavoro non finisce la prima volta che tutto viene convalidato. Devi anche assicurarti che il tuo progetto verrà convalidato di nuovo e che verrà convalidato per gli altri. Ne parleremo nella prossima regola.

Regola 9: Rielabora la tua convalida per l’affidabilità.

Pensavo di avere finito. Poi ho spostato la definizione del math Min a sei righe dalla libreria standard di Dafny al mio codice. Questo ha causato la fallita della mia convalida, per nessuna ragione logica (letteralmente!). In seguito, dopo aver pensato di aver risolto il problema, ho eliminato un metodo non utilizzato. Di nuovo, la convalida ha iniziato a fallire senza una ragione logica.

Cosa sta succedendo? Dafny funziona in modo euristico tramite una ricerca casuale. Cambiare superficialmente il codice (o cambiare i seed casuali) può influire sul tempo necessario alla ricerca. A volte, la quantità di tempo cambia drasticamente. Se il nuovo tempo supera un limite di tempo impostato dall’utente, la convalida fallirà. [Parleremo più in dettaglio del limite di tempo nel suggerimento n. 3, qui sotto.]

Dovresti testare l’affidabilità della tua convalida provando seed casuali diversi. Ecco i comandi che ho usato (su Windows) per convalidare un file con 10 seed casuali.

@rem Trova la posizione di Dafny e aggiungila al tuo pathset path=C:\Users\carlk\.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%path%dafny verify seq_of_sets_example7.dfy --verification-time-limit:30 --cores:20 --log-format csv --boogie -randomSeedIterations:10

Il risultato è un file *.csv che puoi aprire come foglio di calcolo e cercare eventuali errori:

A proposito: per ulteriori idee sulla misurazione dell’affidabilità della convalida di Dafny, consulta questa risposta di Stack Overflow sulla analisi dei file *.csv e questa discussione su GitHub che consiglia lo strumento dafny-reportgenerator.

Trovati i punti problematici, ho coinvolto il co-autore Divyanshu Ranjan per ottenere aiuto. Divyanshu Ranjan ha utilizzato la sua esperienza con Dafny per risolvere i problemi di convalida del progetto.

Ecco i suoi suggerimenti, con esempi tratti dal progetto:

Suggerimento n. 1: Quando possibile, rimuovi le istruzioni require che coinvolgono “forall” ed “exists”.

Ricorda dalla regola 4 che la funzione fantasma SeqToSet restituisce l’insieme di interi coperti da una lista ordinata e disgiunta di intervalli non vuoti. Definiamo “ordinato e disgiunto” con la funzione ValidSeq, che internamente utilizza due espressioni forall. Possiamo rimuovere il requisito che la lista debba essere ordinata e disgiunta, così:

funzione fantasma SeqToSet(sequence: seq<NeIntRange>): set<int>  diminuisce |sequence|  // rimosso: requires ValidSeq(sequence){  if |sequence| == 0 then {}  else if |sequence| == 1 then RangeToSet(sequence[0])  else RangeToSet(sequence[0]) + SeqToSet(sequence[1..])}

Dal nostro punto di vista, abbiamo la stessa funzione utile. Dal punto di vista di Dafny, la funzione evita due espressioni forall ed è più facile da applicare.

Suggerimento n. 2: Usa calc per evitare congetture di Dafny.

Con una dichiarazione Dafny calc, elenchi i passaggi esatti necessari per arrivare a una conclusione. Ad esempio, ecco un calc dal metodo DeleteExtra:

calc {    SeqToSet(xs[..indexAfter+1]) + SeqToSet(xs[indexAfter+1..]);  ==    { SeqToSetConcatLemma(xs[..indexAfter+1], xs[indexAfter+1..]); }    SeqToSet(xs[..indexAfter+1] + xs[indexAfter+1..]);  ==    { assert xs == xs[..indexAfter+1] + xs[indexAfter+1..]; }    SeqToSet(xs);  ==    { SetsEqualLemma(xs, r[indexAfter], r2, indexAfter, indexDel); }    SeqToSet(r2);  }

In questo punto del codice, xs è una sequenza di intervalli, ma potrebbe non essere ordinata e disgiunta. Il calc asserisce che:

1. gli interi coperti dalle due parti di xs, sono uguali
2. gli interi coperti dalla concatenazione delle sue due parti, sono uguali
3. gli interi coperti da xs, sono uguali
4. rs.

Per ogni passaggio, è consentito includere lemmi o asserzioni per aiutare a dimostrare quel passaggio. Ad esempio, questa asserzione aiuta a dimostrare il passaggio dal passaggio 3 al 4:

{ assert xs == xs[..indexAfter+1] + xs[indexAfter+1..]; }

Per efficienza e controllo, questi lemmi e asserzioni non saranno visibili al validatore oltre al loro passaggio. Questo mantiene Dafny concentrato.

Consiglio n. 3: Usa timeLimit per fornire calcoli quando necessario.

Dafny smette di cercare di convalidare un metodo a un timeLimit impostabile dall’utente. Limiti di 10, 15 o 30 secondi sono comuni perché, come utenti, vogliamo generalmente che le convalide che non accadranno mai falliscano rapidamente. Tuttavia, se sappiamo che una convalida avverrà alla fine, possiamo impostare un limite di tempo specifico per il metodo. Ad esempio, Divyanshu Ranjan ha notato che DeleteExtra di solito viene convalidato, ma richiede più tempo rispetto agli altri metodi, quindi ha aggiunto un limite di tempo specifico per il metodo:

method {:timeLimit 30} DeleteExtra(xs: seq<NeIntRange>, internalRange: IntRange) returns (r: seq<NeIntRange>)// ...

Nota: timeLimit non tiene conto della differenza di velocità tra i computer, quindi impostalo un po’ generosamente.

Consiglio n. 4: Usa split_here per dividere un problema di convalida in due.

Come spiegano le Domande frequenti su Dafny, a volte convalidare un insieme di asserzioni insieme è più veloce e a volte convalidarle una alla volta è più veloce.

Usa l’istruzione assert {:split_here} true; per dividere una sequenza di asserzioni in due parti ai fini della convalida. Ad esempio, anche con il timeLimit, DeleteExtra ha superato il tempo limite fino a quando Divyanshu Ranjan ha aggiunto questo:

// ...else  {    r := (s[..i] + [pair]) + s[i..];    assert r[..(i+1)] == s[..i] + [pair];    assert r[(i+1)..] == s[i..];    assert {:split_here} true; // split validation into two parts    calc {      SeqToSet(r[..(i+1)]) + SeqToSet(r[(i+1)..]);// ...

Consiglio n. 5: Tieni i lemmi piccoli. Se necessario, dividi le garanzie tra i lemmi.

A volte i lemmi cercano di fare troppo in una volta sola. Considera il SetsEqualLemma. È correlato all’eliminazione di intervalli ridondanti. Ad esempio, se inseriamo a in xs, gli intervalli contrassegnati con “X” diventano ridondanti.

La versione originale di SetsEqualLemma conteneva 12 requires e 3 ensures. Divyanshu Ranjan l’ha diviso in due lemmi: RDoesntTouchLemma (11 requires e 2 ensures) e SetsEqualLemma (3 requires e 1 ensures). Con questo cambiamento, il progetto è stato convalidato in modo più affidabile.

Applicando questi consigli miglioreremo l’affidabilità della nostra prova. Possiamo rendere la convalida affidabile al 100%? Purtroppo no. C’è sempre una possibilità che con un seme sfortunato Dafny non riuscirà a convalidare. Quindi, quando smetti di cercare di migliorare la convalida?

In questo progetto, io e Divyanshu Ranjan abbiamo migliorato il codice di convalida fino a quando la possibilità di errori di convalida in una singola esecuzione è scesa al di sotto del 33%. Quindi, su 10 esecuzioni casuali, non abbiamo visto più di 2 o 3 errori. Abbiamo persino provato 100 esecuzioni casuali. Con 100 esecuzioni, abbiamo visto 30 errori.

Conclusione

Quindi, ecco a te: nove regole per dimostrare la correttezza di un algoritmo Rust con Dafny. Potresti essere scoraggiato dal fatto che il processo non sia più facile o automatico. Io, tuttavia, sono incoraggiato dal fatto che il processo sia possibile del tutto.

A proposito: dalla classe di geometria – al liceo – ho sempre trovato affascinanti e frustranti le dimostrazioni matematiche. “Affascinanti” perché un teorema matematico, una volta dimostrato, è considerato vero per sempre. (La geometria di Euclide è ancora considerata vera. La fisica di Aristotele no.) “Frustranti” perché le mie lezioni di matematica sembravano sempre vaghe su quali assiomi potevo assumere e quanto grandi potevano essere i passi della mia dimostrazione. Dafny e sistemi simili eliminano questa vaghezza con la verifica automatica delle prove. Ancora meglio, dal mio punto di vista, ci aiutano a creare prove su un’area che mi interessa profondamente: gli algoritmi.

Quando vale la pena fare una dimostrazione formale di un algoritmo? Considerato il lavoro coinvolto, lo farò solo quando l’algoritmo è una combinazione di complicato, importante o facile da dimostrare.

Come potrebbe migliorare il processo in futuro? Mi piacerebbe vedere:

• Interazione tra sistemi – Una volta dimostrato un teorema di geometria, non è necessario dimostrarlo nuovamente. Mi piacerebbe che i sistemi che controllano le prove algoritmiche potessero utilizzare le prove reciproche.
• Un sistema tutto-Rust facile da usare come Dafny – Per lavori in questa direzione, vedi [1,2].

A proposito: conosci un sistema di convalida Rust facile da usare? Ti prego di considerare l’applicazione alla convalida di internal_add. Ciò ci consentirebbe di confrontare la facilità d’uso e la potenza del sistema Rust con Dafny.

• La controparte delle affermazioni di validità dei file Cargo.lock di Rust – In Rust, utilizziamo Cargo.lock per bloccare una combinazione nota di dipendenze di progetto. Speravo che quando Dafny trovava il modo di dimostrare, ad esempio, un metodo, bloccasse anche i passaggi della prova trovati. Questo potrebbe rendere la convalida più affidabile.
• Miglior intelligenza artificiale per la convalida – La mia intuizione è che ChatGPT, leggermente migliorato, potrebbe essere bravo a creare il 90% del codice di convalida necessario. Al momento trovo che ChatGPT 4 sia scadente con Dafny, presumo per mancanza di esempi di addestramento di Dafny.
• Migliore convalida per l’intelligenza artificiale – Quando un’intelligenza artificiale genera codice, ci preoccupiamo della correttezza del codice. La convalida formale potrebbe aiutare a dimostrarne la correttezza. (Per un piccolo esempio di questo, vedi il mio articolo Check AI-Generated Code Perfectly and Automatically.)

Grazie per esserti unito al nostro viaggio nella correttezza del programma. Speriamo che se hai un algoritmo per il quale desideri una prova, questi passaggi ti aiuteranno a trovarla.

Per favore, segui Carl su VoAGI. Scrivo di programmazione scientifica in Rust e Python, apprendimento automatico e statistica. Solitamente scrivo circa un articolo al mese.

Leggi di più sui lavori di Divyanshu Ranjan sul suo blog. Oltre ai metodi formali, il blog tocca temi come la geometria, la statistica e altro ancora.