changeAttributes(ident uid, ident id, ident taskId, double maxPoints) { assume exists /account[uid]/examiner[id]; assume exists /exam[id]/task[taskId]; # implies the existence of the exam assume maxPoints >= 0; assume /exam[id]/participant[x]/result[taskId]/points <= maxPoints; update /exam[id]/task[taskId]/maxPoints maxPoints; }