@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

  grade = F;

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