createGrade(ident uid, ident id, ident gradeId, double value, double minPoints) {
  assume exists //accounts/account[uid]/examiner[id];
 
  assume exists //exams/exam[id]; # implicitly true in OO implementations
  assume not exists //exams/exam[id]/grades/grade[gradeId];
 
  assume count(value, //exams/exam[id]/grades/grade/value) = 0;
  assume count(minPoints, //exams/exam[id]/grades/grade/minPoints) = 0;
 
  assume //exams/exam[id]/grades/grade[x]/value < value -> //exams/exam[id]/grades/grade[x]/minPoints > minPoints;
  assume value < //exams/exam[id]/grades/grade[x]/value -> minPoints < //exams/exam[id]/grades/grade[x]/minPoints;
 
  insert //exams/exam[id]/grades <grade id=[gradeId] value=[value] minPoints=[minPoints] />;
}