0
$\begingroup$

This is the proram for which I have to prove correctness using Hoare's Axioms:

{X = |x|}

if(x<=0)

   x:=-x;

else

   skip;

{X=x}

This is my solution so far by applying Haore's conditional transformation:

(x<=0 => wp(x:=-x; X=x)) ^ (~(x<=0) => wp(skip, X=x))

(x<=0 => X=-x) ^ (~(x<=0) => X=x)

Now the thing I am confused about is how can I prove X = |x|?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.