// Syntax of function call:  var = f(args);

// 'result' is a keyword which stands for the return value of the function call.

// No side-effects via parameters permitted.  Only call-by-value.

@requires x >= 0
@ensures result = x+2
int add2(int x) {
    return x+2;
}

@requires x >= 0
@ensures result = x-2
int sub2(int x) {
   return x-2;
}

// main program

@requires y >= 0
@ensures ans = y*y
@program
    @var ans, t1, t2, y : int
    t1 = add2(y);
    t2 = sub2(y);
    ans = t1*t2 + 4;
@end
--