@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  55 =< marks =< 65
@ensures   grade = C

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

  grade = map(marks);
@end
--