Mis vahe on täieliku ja osalise korrektsuse vahel?


Vastus 1:

Totaalse õigsuse spetsifikatsioon on ka osalise õigsuse spetsifikatsioon. Osaline korrektsus on nõrgem, kuna järelduse tegemiseks on vaja 'S lõpeb' täiendavat abi: R hoiab lõppseisundis.

Osalise õigsuse spetsifikatsiooni {Q} S {R} saamiseks võite saada järgmise teabe: Arvestades Q-le vastavat lähteseisundit, võib S lõppeda või mitte. Kui S lõpeb, jõutakse pärast S täitmist lõppseisundini, mis vastab R-le. Kui ei, siis R on kasutu, kuna lõplikku olekut pole.

Näiteks:

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

See on osalise õigsuse spetsifikatsioon. Kui y initsialiseeritakse arvuga, mis on võrdne või suurem kui 0, lõpeb S ja pärast seda on x 0. Kui y algab negatiivse numbriga, siis S silmustab igavesti ja kuna see ei lõpe, siis te ei jõua olekusse ' pärast S hukkamist ”.

R võib tõepoolest olla ükskõik milline, kui S on surnud ahel. Näiteks mis tahes Q ja R jaoks:

{Q}
kuigi (tõsi):
    y = y - 1
{R}

on alati osalise õigsuse spetsifikatsioon.

Kui Q pole piisavalt tugev, ei saa te S-i lõpetamist garanteerida, rääkimata S-i hukkamise järgsest olekust. Sel juhul saate tingimuse käsitsi lisada: S lõpeb. Q ja selle korral võib arutluskäik jätkuda.

{Q} S {R} täieliku õigsuse täpsustamiseks on Q piisavalt tugev, et tagada S lõppemine, nii et võite järeldada, et S lõpeb ja lõppseisund vastab R-le.

Näiteks:

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

on täielik õigsuse spetsifikatsioon.

BTW: Ma pole kindel, kas vastus on õige, kuna küsimus on märgistatud poliitilise korrektsusega. Kuigi küsimuses esitatud määratlus näeb välja täpselt samasugune nagu arvutiteaduses.