Come dimostrare $ c = a + b $ utilizzando le tecniche di verifica del programma

Question

Sto cercando di dimostrare una cosa elementare, ma a un certo punto sembra che tu stia arrivando atomi dove non puoi provare nient'altro. Questo è il motivo per cui mi chiedo di provare $ c = a + b $, sembra un atomo.

inizio {align} {a, b } c = a + b {a, b, c = a + b } end {align}

Questo è il mio tentativo di un'affermazione di Hoare. Dice "dato $ a $ e $ b $, se assegno $ c $ a $ a + b $, allora finisco con $ a $ e $ b $ invariati e $ c $ assegnati a $ a + b $ . " Cioè, sta dicendo "Se faccio $ c = a + b $, allora finisco con $ c = a + b $", che sembra rosso. Inoltre, questo sembra difficile da formalizzare nella programmazione. Se il modulo è $ {p_1 } q {p_2 } $, allora $ q $ e $ c $ parte di $ p_2 $ è lo stesso codice, vale a dire $ c = a + b $. Quindi non vedo che ci sia bisogno di scrivere un'affermazione per l'aggiunta, possiamo semplicemente dichiarare le sue proprietà (che restituisce un numero) ed è dimostrato per definizione. Cioè, è un assioma.

Mi chiedo se questo è vero o dove mi manca qualcosa. Perché quando ho provato a scrivere questo nel software, finisco praticamente come appare in quella definizione dell'asserzione Hoare sopra, $ c = a + b $ due volte.