function max(a : int, b : int) : int
{
  if (a > b) then
    a
  else
    b
}

/*
ghost function max(a : int, b : int) : int
{
  if (a > b) then
    a
  else
    b
   }
method max(a : int, b : int) returns (r : int)
   ensures r == max(a, b)
{
 /* ... */
}
*/

predicate iseven(a : int)
{
  a % 2 == 0
}
/* syntactic sugar pentru
function iseven(a : int) : bool
{
  a % 2 == 0
}
 */

ghost predicate iseven1(a : int)
{
  exists b : int :: a == 2 * b
}

/*
   Limbajul functional:
   - expresii executabile
   - expresii neexecutabile
     (obligatoriu ghost)
 */

method Main()
{
  var r1 := max(3, 7);
  var r2 := iseven(8);
  print "Max 3, 7", r1, r2;
}