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

@requires marks = 75
@ensures  grade = B

@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
--