I am totally new to Ada, and have been trying to implement some basics. I have a simple function to flip a coin - not randomly, heads should be flipped to tails and vice versa. I added a post condition that flip(coin) != coin. It is supposed to say that a flipped coin must not equal the original coin, but when I try to prove the file with --mode gold, I get the following warnings:
flip_coin.ads:8:06: warning: postcondition does not mention function result
flip_coin.ads:8:14: warning: call to "flip" within its postcondition will lead to infinite recursion
flip_coin.ads:8:14: medium: postcondition might fail, cannot prove flip(x) /= x[#0]
Here is the ads file
package flip_coin with SPARK_Mode
is
type Coin is (Heads, Tails);
function flip (x : Coin) return Coin with
Post => flip(x) /= x;
end flip_coin;
And here is the .adb file
package body flip_coin with SPARK_Mode
is
function flip (x : Coin) return Coin
is
begin
if x = Heads then return Tails; else return Heads; end if;
end flip;
end flip_coin;
Any help would be great! I will be asking plenty more over the next 2 weeks.
Try the postcondition:
function flip (x : Coin) return Coin with
Post => flip'Result /= x;
This ensures that the function result does not equal the function input x
.
Stating flip(x)
in your postcondition will indeed result in infinite recursion as the postcondition will be checked for each invocation of flip
. As a result, the function will always be evaluated one more time to check the postcondition: infinite recursion.