Esistono numerosi framework per dimostrare che il codice è corretto. Puoi leggere alcuni di essi in libri come
-
Una teoria pratica della programmazione , Hehner, 1993-2014.
-
La scienza della programmazione , Gries, 1981.
-
Un metodo di programmazione , Dijkstra e Feijn, 1988.
-
Programmazione da specifiche , Morgan, 1990, 1994, 1998.
Per il tuo programma, presumo che non ti importi del n negativo e che puoi gestire i casi n==0 , n==1 e n==2 senza alcun aiuto; Vedrò solo il caso in cui n>2 .
La chiave è di notare che (nei casi in cui n > 2 ) ogni volta che viene valutata l'espressione di guardia del ciclo divisor <= limit , i seguenti 5 fatti sono veri dello stato del programma:
n % i != 0, for all i from 2 up to, but not including divisor
limit == n-1
2 <= divisor && divisor <= n
mod != 0 || divisor == 2
n is the same as the argument // i.e. n hasn't been changed
Questi 5 fatti sono chiamati invarianti del ciclo. Confidare che l'invarianza del loop tenga dove ho detto che lo fa, puoi controllare
- che contiene la prima volta che la guardia viene valutata e
- che, se l'invariante è vero e la guardia è vera, allora una esecuzione del corpo del ciclo lascerà il programma in uno stato in cui l'invariante è di nuovo vero.
Pertanto, quando e se il ciclo termina normalmente *, tutto quanto sopra è vero e così è divisor > limit . Questo ti dice che divisor == n e quindi hai
n % i != 0, for all i from 2 up to, but not including n
mod != 0
n is the same as the argument // i.e. n hasn't been changed
Pertanto, se il ciclo termina normalmente, verrà eseguito il return true dopo il ciclo e l'argomento è primo.
Gli unici casi di cui preoccuparsi sono quelli in cui il ciclo non termina normalmente. Ci sono due motivi per cui un ciclo potrebbe non terminare normalmente: è infinito o c'è un salto fuori da esso, come un'interruzione, un ritorno o un'eccezione. Nel tuo codice, è possibile mostrare che il ciclo non è infinito e l'unico salto è quando n % divisor == 0 . Dal momento che, a quel punto, abbiamo anche
2 <= divisor // from the invariant
divisor <= limit // from the guard
limit == n-1 // from the invariant
abbiamo 2<=divisor && divisor < n . Quindi se viene eseguito il return false nel ciclo, è solo quando n % divisor == 0 e divisor è maggiore di 1 e minore di n , e quindi n (e quindi l'argomento) non è Prime.
In sintesi
- per non scadenti (maggiore di 2), il ciclo non può terminare normalmente e quindi è necessario eseguire
return false e
- per i primi (maggiore di 2) il ciclo deve terminare normalmente e in uno stato in cui
mod != 0 e quindi verrà eseguito return true .
La dimostrazione suggerisce alcuni modi per semplificare il codice. I libri che ho menzionato forniscono dei modi per rendere l'analisi più formale, anche se penso che solo Hehner's offra un modo per gestire le prime uscite dai loop.
[*] Con "termina normalmente", intendo che termina perché la sua guardia è falsa.
Questa analisi ti dà la certezza assoluta che il tuo codice è impeccabile? Spero di no. Ma dovrebbe darti rassicurazione. Uno può utilizzare strumenti come ESC / Java2 o Spec # in modo che un computer possa verificare che non si siano commessi errori. Ciò aumenterebbe il livello di fiducia che il codice ha raggiunto un livello molto alto. Ovviamente potrebbero esserci dei bug nel programma che si usa per controllare la verifica o nell'hardware su cui gira. Per scopi pratici, codice come il tuo può essere verificato e la verifica può essere verificata con strumenti accuratamente scritti e affidabili.