class Secret{
  var secret : int; // A secret number between 1...10
  var known : bool; // Has the secret been guessed yet?
  var count : int;  // How many guesses has been made?
  
  method Init(x: int)
   modifies this;
   requires 0 < x <= 10; 
   ensures known == false;
   ensures secret == x;
   ensures count == 0;
   {
    secret := x;
    known := false;
    count := 0;
  }
  
  method guess(g : int) returns (result : bool, guesses : int)
  modifies this`known, this`count;
  requires !known;
  ensures count == old(count) + 1 && guesses == count;
  ensures g == secret ==> known && result;
  ensures g != secret ==> !known && result==false;
  {
    count := count +1;
    guesses := count;

    if (g == secret) 
    {known := true; 
    result := true; 
    }
    else{
    result := false; 
    }
  }
  
  method Main(){
    var s := new Secret;
    s.Init(5);
    
    var result : bool := false;
    var guesses : int := 0;

    result, guesses := s.guess(6);
    assert !s.known && !result && guesses == 1;

    result, guesses := s.guess(5);
    assert s.known && result && guesses == 2;
    }
}