changeAttributes(ident uid, ident id, ident sheetId, double maxPoints) {
assume exists /account[uid]/assistant[id];
assume exists /exercise[id]/sheet[sheetId]; # implies the existence of the exercise
assume maxPoints >= 0;
assume /exercise[id]/student[x]/result[sheetId]/points <= maxPoints;
update /exercise[id]/sheet[sheetId]/maxPoints maxPoints;
}