# Formal verification of function contract?

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

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