changeAttributes(ident uid, ident id, ident groupId, string day, string time, string location, integer maxSize) { assume exists /account[uid]/assistant[id]; assume exists /exercise[id]/group[groupId]; # implicitly true in OO implementations assume maxSize >= 0; assume /exercise[id]/group[groupId]/curSize <= maxSize; update /exercise[id]/group[groupId]/day day; update /exercise[id]/group[groupId]/time time; update /exercise[id]/group[groupId]/location location; update /exercise[id]/group[groupId]/maxSize maxSize; }