1
$\begingroup$

How could I formally reason about the following function:

function f(x){
    if(x>=0){
        return 1;
    }else{
        return 0;
    }
    return 2;
}

The statement I'd like to prove is \forall x: f(x)!=2

How can I do it meticulously, using Hoare logic? My main concern is how to prevent the consecutive return to overwrite the previous, so what axiom to use to not to be able to do that.

In this blog the writer defines the function call as enter image description here

This is good to reason about return values, but I don't see how it could be useful.

$\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.