Una specifica di correttezza totale è anche una specifica di correttezza parziale. La correttezza parziale è più debole perché ha bisogno dell'aiuto aggiuntivo di "S termina" per giungere alla conclusione: R rimane nello stato finale.

Per una specifica di correttezza parziale {Q} S {R}, è possibile ottenere le seguenti informazioni: Dato uno stato iniziale che soddisfa Q, S può terminare o meno. Se S termina, dopo l'esecuzione di S, raggiungerai uno stato finale che soddisfa R. In caso contrario, R è inutile poiché non esiste uno stato finale.

Per esempio:

{X} == 10
while (y! = 0):
    y = y - 1
x = 0
{X == 0}

È una specifica di correttezza parziale. Se y viene inizializzato con un numero uguale o maggiore di 0, S terminerà e dopo che x è 0. Mentre se y inizia con un numero negativo, S verrà ripetuto per sempre e poiché non termina, non si raggiungerà uno stato ' dopo l'esecuzione di S '.

In effetti, R può essere qualsiasi cosa se S è un circuito chiuso. Ad esempio, per qualsiasi Q e R:

{Q}
while (true):
    y = y - 1
{R}

è sempre una specifica di correttezza parziale.

Se Q non è abbastanza forte, non puoi garantire la fine di S, figuriamoci la ragione dello stato dopo l'esecuzione di S. In questo caso è possibile aggiungere manualmente una condizione: S termina. Con Q e esso, il ragionamento può continuare.

Per la specifica di correttezza totale {Q} S {R}, Q è abbastanza forte da garantire la terminazione di S, quindi puoi concludere che S terminerà e lo stato finale soddisfa R.

Per esempio:

{x == 10}
while (x! = 0):
    x = x - 1
{x == 0}

è una specifica di correttezza totale.

A proposito: non sono sicuro che la risposta sia corretta perché la domanda è taggata con correttezza politica. Mentre la definizione nella domanda sembra esattamente la stessa di Informatica.