@type letter = A | B | C | D | F

@function map: int -> letter

@axiom A1: all n:int. 
 (n > 90 ==> map(n) = A) &&
 (n > 70 && n =< 90 ==> map(n) = B) &&
 (n > 50 && n =< 70 ==> map(n) = C) &&
 (n > 30 && n =< 50 ==> map(n) = D) &&
 (n =< 30 ==> map(n) = F)


@requires  0 =< marks =< 100
@ensures   grade = map(marks)


@program 
  @var marks : int
  @var grade : letter

  if (marks > 90) 
	grade = A;
  else  if (marks > 70) 
	    grade = B;
  	else if (marks > 50)
		  grade = C;
	     else if (marks > 30)
		  	grade = D;
		  else  grade = F;
@end
--