La definizione di precondizionismo più debole per un linguaggio non deterministico

Question

Nel linguaggio di IMP classico, la definizione di presupposto più debole è:

definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t"

Ciò afferma che dallo stato s, dopo aver eseguito C, arriviamo a uno stato che soddisfa Q. La mia domanda arriva quando si gestisce il costrutto IF FI nella lingua dei comandi protetti (vedere il comando di selezione in Wikipedia). La mia ipotesi è che in questo caso bisogna definire:

definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ (∀ t'. (c,s) ⇒ t' ⟶ Q t')"

Mi chiedo se questo sia corretto e se è il modo standard di scriverlo in letteratura.

Attualmente, sto avendo problemi a dimostrare la definizione preliminare più debole per la composizione sequenziale dei comandi:

"wp (c1;;c2) Q s = wp c1 (wp c2 Q) s" 

Quindi, sto cominciando a pensare che la mia definizione sia sbagliata. Citando Wikipedia:

Il risultato di questa funzione, indicato WP (s, R), è il preliminare "più debole" sullo stato iniziale che garantisce che l'esecuzione di S termina in uno stato finale che soddisfa R.

Quindi la terminazione è richiesta nella definizione, e questo non è correttamente imposto finora. Potrebbero esserci rami non terminanti.