Complétez la précondition : { ??? } x = y; y = temp; { x = Y ∧ y = X } (échange des valeurs initiales X et Y)

x = X && y = Y && temp = Y

Précondition {P} :

Écrivez la précondition. Format : 0 <= |x|

Valider