Jaka jest różnica między całkowitą poprawnością a częściową poprawnością?


Odpowiedź 1:

Całkowita specyfikacja poprawności jest również częściową specyfikacją poprawności. Częściowa poprawność jest słabsza, ponieważ wymaga dodatkowej pomocy „S terminates”, aby dojść do wniosku: R utrzymuje się w stanie końcowym.

W przypadku częściowej specyfikacji poprawności {Q} S {R} można uzyskać następujące informacje: Biorąc pod uwagę stan początkowy, który spełnia Q, S może zakończyć się lub nie. Jeśli S zakończy działanie, po wykonaniu S osiągniesz stan końcowy, który spełnia R. Jeśli nie, R jest bezużyteczne, ponieważ nie ma stanu końcowego.

Na przykład:

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

Jest to częściowa specyfikacja poprawności. Jeśli y zostanie zainicjowane z jakąś liczbą równą lub większą niż 0, S zakończy się, a następnie x wyniesie 0. Podczas gdy y zaczyna się od liczby ujemnej, S zapętla się na zawsze, a ponieważ się nie kończy, nie osiągniesz stanu „ po egzekucji S. ”.

Rzeczywiście, R może być dowolne, jeśli S jest w martwej pętli. Na przykład dla dowolnego pytania i odpowiedzi:

{Q}
podczas gdy (prawda):
    y = y - 1
{R}

jest zawsze specyfikacją częściowej poprawności.

Jeśli Q nie jest wystarczająco silny, nie możesz zagwarantować zakończenia S, nie mówiąc już o uzasadnieniu stanu po wykonaniu S. W takim przypadku możesz ręcznie dodać warunek: S kończy. Z Q i tym rozumowanie może być kontynuowane.

Dla specyfikacji całkowitej poprawności {Q} S {R}, Q jest wystarczająco silny, aby zagwarantować zakończenie S, więc możesz stwierdzić, że S zakończy się, a stan końcowy spełni R.

Na przykład:

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

jest specyfikacją całkowitej poprawności.

BTW: Nie jestem pewien, czy odpowiedź jest prawidłowa, ponieważ pytanie jest oznaczone poprawnością polityczną. Podczas gdy definicja w pytaniu wygląda dokładnie tak samo jak w informatyce.