Hoare Calculus Axiom di assegnazione errata

Question

Attualmente mi sto preparando per un esame e recentemente mi sono imbattuto nel seguente esercizio e vorrei sapere se la mia soluzione sarebbe corretta.

Esercizio: Dimostra che il seguente assioma non è corretto nel calcolo di Hoare:

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

La mia prova tramite Reductio ad Absurdum:

Assunzione:

Axiom è valido il calcolo Hoare Axiom e quindi concorda con gli altri assiomi.

Prova:

Considera la tripla Hoare: {t = u+1} u: = t {u = t}

Questa tripla è ovviamente non valida perché non è d'accordo con l'assioma di assegnazione del calcolo Hoare.

Tuttavia, dato il nostro presupposto, possiamo derivarlo come una tripla valida:

(t = u+1) => (true) (indebolire precondizionismo)

{true} u: = t {u = t} (axiom del presupposto)

=> {t = u+1} u: = t {u = t} <- contraddizione! => Il presupposto era falso, l'assioma non è corretto.

QED