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

@requires marks = 75
@ensures  grade = B

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