Hoare Logic Loop Invariant

Question

Sto guardando Hoare Logic e ho problemi a capire il metodo per trovare il ciclo invariante.

Qualcuno può spiegare il metodo utilizzato per calcolare il ciclo invariante?

E cosa dovrebbe contenere un invariante di loop per essere uno "utile"?

Sono solo trattare con semplici esempi, trovando invarianti e dimostrando la correzione parziale e completo in esempi come:

{ i ≥ 0 } while i > 0 do i := i−1 { i = 0 } 

Answer 1

Se stiamo parlando di Logica di Hoare per dimostrare la correttezza (parziale) dei programmi, quindi si utilizza la precondizione e postcondizione, scomporre il programma e utilizzare le regole del sistema di deduzione logica di Hoare per creare e dimostrare una formula induttiva.

Nel tuo esempio, si vuole scomporre il programma utilizzando la regola

{p} while b do S {p^not(b)} <=> {p^b} S {p} 

Nel tuo caso

• p: i ≥ 0
• b: i> 0
• S: i: = i-1.

Quindi nel passaggio successivo deduciamo {i ≥ 0^i > 0} i := i−1 {i ≥ 0}. Questo può essere ulteriormente dedotto e dimostrato abbastanza facilmente. Spero che questo aiuti.

Answer 2

Essere utile (per il vostro ragionamento) è il punto principale del invariante. Quindi, guarda la post-condizione che vuoi dimostrare e prova a creare un invariante che ti aiuti ad arrivare al post-condizione post-condizione e che è derivabile dal codice del ciclo.

Answer 3

Non sono sicuro se questo sarà rispondere alla tua domanda, ma solo nel caso in cui lo fa:

• A "invariante di ciclo" informale è un dato di fatto che rimane fedele prima e dopo un iterazione di un ciclo continuo. Definisce essenzialmente il vincolo di coerenza del programma rispetto a quel ciclo.
• Non so abbastanza su Hoare Logic per dirti esattamente come un ciclo invariante sarebbe 'calcolato', ma sospetto che una cosa del genere dipenda dal linguaggio del codice che viene analizzato più che dal linguaggio formale di prova stesso . Hai una descrizione algoritmica formale con cui stai lavorando? Potrei essere in grado di andare oltre con un po 'più di esperienza.
• Un utile ciclo invariante descrive qualcosa di specifico sullo stato di un'applicazione. Ad esempio se stavi scrivendo Insertion Sort, un utile ciclo invariante per il loop di movimento dell'elemento principale indicava essenzialmente che l'elenco (sotto) contiene la stessa collezione di oggetti prima e dopo l'esecuzione del ciclo, e forse che gli elementi che erano precedentemente nell'ordine ordinato rimangono in ordine.