This is an old revision of the document!
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] />; }