Comment résoudre pour la condition préalable donne une post-condition qui doit satisfaire à deux conditions

Question

J'ai essayé de résoudre la question de l'examen passée, mais il y a celle-ci que je n'ai pas pu résoudre.

La question stipule qu'une condition préalable appropriée doit être trouvée pour la déclaration.

$$ a = i +2; i ++ {(a = 7) land (i = 5) } $$ Voici ma solution et où j'ai été coincé:

$$ wp (a = i +2; i ++, (a = 7 land i = 5) = wp (a = i +2, wp (i = i + 1, a = 7 land i = 5) $$

J'ai essayé de le résoudre intuitivement et j'arrive à la conclusion qu'aucune valeur de ce type pour iJe devrais exister.

Je n'ai pas pu trouver de règle pour combiner les deux prédicats du post-condition.

S'il vous plaît, je voudrais savoir lors de la résolution de questions similaires, puis-je changer le ^ à un symbole d'algèbre ou devrais-je prendre la condition pertinente et trouver la condition la plus faible avec cela.