Hoare Calcul Axiom de l'affectation incorrecte

Question

Je me prépare actuellement à un examen et je suis récemment tombé sur l'exercice suivant et je voudrais savoir si ma solution serait correcte.

Exercer: Prouver que l'axiome suivant n'est pas correct dans le calcul Hoare:

{true} u: = t {u = t}

Ma preuve via reductio ad absurdum:

Hypothèse:

L'axiome est un axiome de calcul Hoare valide et est donc d'accord avec les autres axiomes.

Preuve:

Considérez le triple hoare: {t = u + 1} u: = t {u = t}

Ce triple est évidemment invalide car il n'est pas d'accord avec l'axiome d'affectation du calcul Hoare.

Cependant, compte tenu de notre hypothèse, nous pouvons le dériver comme un triple valide:

(t = u + 1) => (true) (affaiblir la condition préalable)

{true} u: = t {u = t} (axiome de l'hypothèse)

=> {t = u + 1} u: = t {u = t} <- contradiction! => L'hypothèse était fausse, l'axiome n'est pas correct.

QED