By backward substitution show that the Pre-condition can be derived from the Post-condition: {true} (Pre-condition) if x < 0 (cond) then x = - x else x = x (in other words, do nothing) { x >= 0 } (Post-condition)
{true} (Pre-condition) if x < 0 (cond) then x = - x else x = x (in other words, do nothing) { x >= 0 } (Post-condition)
