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