deleteExam(ident uid, ident id) { assume exists /account[uid]/admin; assume exists /exam[id]; assume size(/exam[id]/examiner) = 0; assume size(/exam[id]/participant) = 0; # don't allow to delete if participants are there remove /exam[id]; }