全体の正確さと部分的な正確さとの違いは何ですか?


答え 1:

完全な正確性の仕様は、部分的な正確性の仕様でもあります。結論に至るには「Sが終了する」という追加の助けが必要であるため、部分的な正確性は弱くなります。Rは最終状態のままです。

部分的な正確性の指定{Q} S {R}の場合、次の情報を取得できます。Qを満たす開始状態が与えられると、Sは終了するかどうかが決まります。 Sが終了すると、Sの実行後にRを満たす最終状態に到達します。そうでない場合、最終状態がないためRは役に立たなくなります。

例えば:

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

これは部分的な正確性の仕様です。 yが0以上の数値で初期化されると、Sは終了し、その後xは0になります。yが負の数値で始まる場合、Sは永久にループし、終了しないため、状態 ' Sの実行後」。

実際、Sがデッドループの場合、Rは何でもかまいません。たとえば、QとRの場合:

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

常に部分的な正確性の仕様です。

Qが十分に強力でない場合、Sの実行後の状態についての理由は言うまでもなく、Sの終了を保証することはできません。この場合、条件を手動で追加できます。Sは終了します。 Q and itを使用すると、推論を続行できます。

完全な正確さの仕様{Q} S {R}の場合、QはSの終了を保証するのに十分な強さなので、Sが終了し、最終状態がRを満たすと結論付けることができます。

例えば:

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

完全な正確性の仕様です。

ところで:質問が政治的正しさでタグ付けされているので、答えが正しいかどうかわかりません。質問の定義はコンピューターサイエンスの定義とまったく同じに見えますが。