How do I modify my post condition to achieve Gold standard of Spark proof - Ada SPARK

Question

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.

Answer 1

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.