Wat is het verschil tussen totale correctheid en gedeeltelijke correctheid?


Antwoord 1:

Een specificatie voor totale correctheid is ook een specificatie voor gedeeltelijke correctheid. Gedeeltelijke correctheid is zwakker omdat het de extra hulp van 'S eindigt' nodig heeft om tot de conclusie te komen: R blijft in de definitieve staat.

Voor een gedeeltelijke correctheidsspecificatie {Q} S {R} kunt u de volgende informatie krijgen: Gegeven een startstatus die voldoet aan Q, kan S eindigen of niet. Als S eindigt, na de uitvoering van S, zul je een eindtoestand bereiken die voldoet aan R. Zo niet, dan is R nutteloos omdat er geen eindtoestand is.

Bijvoorbeeld:

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

Het is een gedeeltelijke correctheidsspecificatie. Als y wordt geïnitialiseerd met een getal gelijk aan of groter dan 0, zal S eindigen en daarna is x 0. Terwijl als y begint met een negatief getal, zal S voor altijd doorlopen en aangezien het niet eindigt, bereikt u geen status ' na de executie van S '.

Inderdaad, R kan alles zijn als S een dead-loop is. Voor elke Q en R:

{V}
terwijl (waar):
    y = y - 1
{R}

is altijd een gedeeltelijke correctheidsspecificatie.

Als Q niet sterk genoeg is, kunt u de beëindiging van S niet garanderen, laat staan ​​redeneren over de staat na de uitvoering van S. In dit geval kunt u handmatig een voorwaarde toevoegen: S wordt beëindigd. Met Q en het kan de redenering doorgaan.

Voor de specificatie van de totale juistheid {Q} S {R} is Q sterk genoeg om de beëindiging van S te garanderen, dus u kunt concluderen dat S wordt beëindigd en de definitieve status voldoet aan R.

Bijvoorbeeld:

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

is een totale correctheidsspecificatie.

Tussen haakjes: ik weet niet zeker of het antwoord correct is, omdat de vraag is getagd met politieke correctheid. Terwijl de definitie in de vraag er precies hetzelfde uitziet als in de informatica.