Table of Contents

XCend Schema

This is the underlying XCend Schema of the whole STAT System. Everything persistent is represented in the schema. The schema's top level element is The Whole Stat System, but it directly splits into the three main groups

Structure and Integrity Constraints

element stats {
  attribute revision { integer }
  element account * username {
    attribute lastName          { string }
    attribute firstName         { string }
    attribute email             { string }
    attribute password          { string }
    attribute code ?            { string }
    attribute reset ?           { string }
 
    element admin ?             { }
    element examiner * exam     {[ exists /exam[./exam]/examiner[../username] ]}
    element assistant * exercise {[ exists /exercise[./exercise]/assistant[../username] ]}
    element tutor * exercise {    
      element group * id        {[ exists /exercise[../exercise]/group[./id]/tutor[..account/username] ]}
    }                             
    element student ? {           
      attribute id              { ident [ count(., /account/student/id) = 1 ]}
    }                             
  } [ size(./account/admin) > 0 ]
  element exercise * id {
    attribute lecture           { string }
    attribute term              { string }
    attribute open              { boolean }
 
    element assistant * account {[ exists /account[./account]/assistant[..exercise/id] ]}
    element group * id {        [ count(./id, ..exercise/student/group) <= ./maxSize ]
      attribute day             { "Monday" | "Tuesday" | "Wednesday" | "Thursday" | "Friday" | "Saturday" | "Sunday" }
      attribute time            { string }
      attribute location        { string }
      attribute curSize         { integer [ . = count(../id, ..exercise/student/group) ]}
      attribute maxSize         { integer [ . >= 0 ]}
 
      element tutor * account   {[ exists /account[./account]/tutor[..exercise/id]/group[..group/id] ]}
    }                           
    element sheet * id {
      attribute maxPoints       { double [ . >= 0 ]}
    }                           
    element student * id {      [ count (./id, /account/student/id) = 1 ]
      attribute group ?         { ident [ exists ..exercise/group[.] ]}
      attribute team ?          { ident [ exists ../group ]}
      element result * sheet {  [ exists ..exercise/sheet[./sheet] ]
        attribute points        { double [ . >= 0 && . <= ..exercise/sheet[../sheet]/maxPoints ]}
      }                         
    }                           
  }                               
  element exam * id {             
    attribute title             { string }
    attribute date              { string }
    attribute time              { string }
    attribute location          { string }
    attribute free              { boolean }
    attribute published         { boolean }
 
    attribute exercise          { ident [ exists /exercise[.] ]}
 
    element examiner * account  {[ /account[./account]/examiner[..exam/id] ]}
 
    element task * id {         
      attribute maxPoints       { double [ . >= 0 ]}
    }                           
    element grade * id {           
      attribute name            { string } [count(./name, ../grade/name) = 1]
      attribute value           { double }
      attribute minPoints       { double }
    }                           [ {exists ./grade[x], exists ./grade[y], x != y} ./grade[x]/value != ./grade[y]/value ]
                                [ {exists ./grade[x], exists ./grade[y], x != y} ./grade[x]/minPoints != ./grade[y]/minPoints ]
                                [ {exists ./grade[x], exists ./grade[y], ./grade[x]/value < ./grade[y]/value} 
                                  ./grade[x]/minPoints > ./grade[y]/minPoints ]
    element participant * id {  [ count (./id, /account/student/id) = 1 ]
      element result * task {   [ exists ..exam/task[./task] ]
        attribute points        { double [ . >= 0 && . <= ..exam/task[../task]/maxPoints ]}
      }
    }
  }
}

Atomic Procedures

This section lists all atomic manipulations associated with the schema.

Associated to the Stat System

These are the associated procedures for The Whole Stat System, i.e. they have no necessary parameters, as the STAT System is unique and does not need disambiguation. Some of them, however, will have ident parameters, which makes it possible to offer them in these classes, too.

System Creation

This is not real atomic operation, more like a constructor for the whole type. It is useful to think about what the smallest valid document is, however.

createEmptyStats() {
  remove /stats; # procedures only operate on valid documents, so we have to get rid of "whatever was there" before
  insert / 
    <stats revision="0">
      <account username="admin" lastName="admin" firstName="admin" email="admin@stats.system" password="some hash of 'admin'">
        <admin />
      </account>
    </stats>;
}

Account Management

Three of the most important procedures, as they create and delete elements of a major part of the system, namely User Accounts and Roles.

Naturally, a lot of things depend on accounts and their associated roles. Especially the student role restricts the deletion of accounts.

The third procedure is a compound procedure, which combines account and student role creation and therefore also combines their preconditions. This is the procedure which should be offered for everyone, especially guests.

Finally, there are more procedures which can be called by anyone, as they are concerned about users who lost their password.

# This doesn't take account validation into consideration at all. It probably has to be allowed to replace an unvalidated account.
createAccount(ident uid, ident username, string lastName, string firstName, string email, string password) {
  assume exists /account[uid]/admin;
 
  assume not exists /account[username];
 
  insert / <account username=[username] lastName=[lastName] firstName=[firstName] email=[email] password=[password] />
}
deleteAccount(ident uid, ident username) {
  assume exists /account[uid]/admin;
  assume uid != username; # or do we want to allow an admin to delete himself?
 
  assume exists /account[username];
 
  assume size(/account[username]/examiner) = 0;
  assume size(/account[username]/assistant) = 0;
  assume size(/account[username]/tutor) = 0;
 
  # not yet a constraint of the implementation, but is seems practically relevant :-)
  if exists /account[username]/admin then
    assume size(/account/admin) > 1;
  fi
 
  if exists /account[username]/student then
    assume size(/exercise/student[/account[username]/student/id]) = 0;
    assume size(/exam/participant[/account[username]/student/id]) = 0;
  fi
 
  remove /account[username];
}
createStudentAccount(ident username, ident studentId, string lastName, string firstName, string email, string password, string code) {
  assume not exists /account[username];
  assume count(studentId, /account/student/id) = 0;
 
  insert /
    <account username=[username] lastName=[lastName] firstName=[firstName] email=[email] password=[password] code=[code]>
      <student id=[studentId] />
    </account>
}
requestReset(ident username, string reset) {
  assume exists /account[username];
 
  assume not exists /account[username]/code; # account is already validated
 
  if not exists /account[username]/reset then
    insert /account[username]/reset;
  fi
  update /account[username]/reset reset;
}
resetPassword(ident username, string reset, string password) {
  assume exists /account[username]/reset; # reset code was requested before, implies account exists
  assume /account[username]/reset = reset; 
 
  remove /account[username]/reset;
  update /account[username]/password password;
}

Validation and Authentication

The free procedures to create a student account comes with the obligation to validate the email address. Its only then that the user can authenticate. The latter is not a real procedure, as nothing even gets modified in the system. It is there to illustrate who the Roles system works.

validateAccount(ident username, string code) {
  assume exists /account[username]/code; # implies existence of the account
 
  assume /account[username]/code = code;
 
  remove /account[username]/code;
}
authenticate(ident username, string password) {
  assume exists /account[username];
 
  assume /account[username]/password = password;
}

Exercise Management

Also two of the most important procedures, as they create and delete elements of a major part of the system, namely Exercise Management and Sheets.

A few roles, like tutor and assistant, depend on the existence of an exercise. Students sign-up status, on the other hand, just gets removed as well.

createExercise(ident uid, ident id, string lecture, string term) {
  assume exists /account[uid]/admin;
 
  assume not exists /exercise[id];
 
  insert / <exercise id=[id] lecture=[lecture] term=[term] open=[false] />
}
deleteExercise(ident uid, ident id) {
  assume exists /account[uid]/admin;
 
  assume exists /exercise[id];
 
  assume size(/exercise[id]/assistant) = 0;
  assume size(/exercise[id]/group/tutor) = 0;
 
  assume size(/exercise[id]/student) = 0; # don't allow to delete if students are there
 
  remove /exercise[id];
}

Exam Management

Finally, the last two of the most important procedures, which create and delete elements of a major part of the system, namely Exam Management and Grades.

The examiner role depends on the existence of an exam.

createExam(ident uid, ident id, ident eid, string title, string date, string time, string location) {
  assume exists /account[uid]/admin;
 
  assume not exists /exam[id];
  assume exists /exercise[eid];
 
  insert /
    <exam id=[id] title=[title] date=[date] time=[time] location=[location] free=[false] published=[false] exercise=[eid] />
}
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];
}

Admin Management

The admin role procedures from User Accounts and Roles can be offered here, too.

grantAdminRights(ident uid, ident username) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]; # implicitly true in OO implementations
  assume not exists /account[username]/admin;
 
  insert /account[username] <admin />;
}
revokeAdminRights(ident uid, ident username) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]/admin; # implies the account exists, which is implicitly true anyway
 
  assume size(/account/admin) > 1; # kind of a practical constraint
 
  remove /account[username]/admin;
}

Associated to Account

These are the associated procedures for User Accounts and Roles, i.e. one of their parameters is a username and they will most likely be offered in a corresponding Account class in an OO setting. Many of them, however, will also have other ident parameters, which makes it possible to offer them in these classes, too.

Change Attributes

Password Management

changePassword(ident uid, ident username, string password) {
  assume exists /account[uid]/admin || uid = username;
 
  assume exists /account[username]; # implicitly true in OO implementations
 
  update /account[username]/password password;
}
requestReset(ident username, string reset) {
  assume exists /account[username];
 
  assume not exists /account[username]/code; # account is already validated
 
  if not exists /account[username]/reset then
    insert /account[username]/reset;
  fi
  update /account[username]/reset reset;
}
resetPassword(ident username, string reset, string password) {
  assume exists /account[username]/reset; # reset code was requested before, implies account exists
  assume /account[username]/reset = reset; 
 
  remove /account[username]/reset;
  update /account[username]/password password;
}

Student Role

The students in the Exercise Management and Sheets section, as well as the participants in the Exam Management and Grades section, depend on the student role. This restricts the deletion of the role, i.e. the host language first has to delete these dependencies with corresponding procedures.

addStudentId(ident uid, ident username, ident id) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]; # implicitly true in OO implementations
  assume not exists /account[username]/student;
  assume count(id, /account/student/id) = 0;
 
  insert /account[username] <student id=[id] />;
}
removeStudentId(ident uid, ident username) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]/student; # implies the account exists, which is implicitly true anyway
 
  assume size(/exercise/student[/account[username]/student/id]) = 0;
  assume size(/exam/participant[/account[username]/student/id]) = 0;
 
  remove /account[username]/student;
}

Admin Role

The admin role is pretty much just a flag, without any constraints at all. The precondition is therefore only concerned with uniqueness and trivial stuff.

grantAdminRights(ident uid, ident username) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]; # implicitly true in OO implementations
  assume not exists /account[username]/admin;
 
  insert /account[username] <admin />;
}
revokeAdminRights(ident uid, ident username) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]/admin; # implies the account exists, which is implicitly true anyway
 
  assume size(/account/admin) > 1; # kind of a practical constraint
 
  remove /account[username]/admin;
}

Examiner Role

The examiner role has to fulfill integrity constraints and has a counterpart in the Exam Management and Grades section of the document.

grantExaminerRights(ident uid, ident username, ident examId) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]; # implicitly true in OO implementations
  assume exists /exam[examId];
 
  assume not exists /account[username]/examiner[examId]);
  assume not exists /exam[examId]/examiner[username]); # implied by integrity and the assumption before
 
  insert /account[username] <examiner exam=[examId] />;
  insert /exam[examId] <examiner account=[username] />;
}
revokeExaminerRights(ident uid, ident username, ident examId) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]/examiner[examId]; # implies the account exists, which is implicitly true anyway
  assume exists /exam[examId]/examiner[username]; # implied by integrity and the assumption before
 
  remove /account[username]/examiner[examId];
  remove /exam[examId]/examiner[username];
}

Assistant Role

The assistant role relates to exercises like the examiner role relates to exams, so it also has to fulfill integrity constraints and has a counterpart in Exercise Management and Sheets.

grantAssistantRights(ident uid, ident username, ident exerciseId) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]; # implicitly true in OO implementations
  assume exists /exercise[exerciseId];
 
  assume not exists /account[username]/assistant[exerciseId]);
  assume not exists /exercise[exerciseId]/assistant[username]; # implied by integrity and the assumption before
 
  insert /account[username] <assistant exercise=[exerciseId] />;
  insert /exercise[exerciseId] <assistant account=[username] />;
}
revokeAssistantRights(ident uid, ident username, ident exerciseId) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]/assistant[exerciseId]; # implies the account exists, which is implicitly true anyway
  assume exists /exercise[exerciseId]/assistant[username]; # implied by integrity and the assumption before
 
  remove /account[username]/assistant[exerciseId];
  remove /exercise[exerciseId]/assistant[username];
}

Tutor Role

The tutor role also behaves similarly, but this time it references two identifiers in the Exercise Management and Sheets section, where it also has a counterpart.

This modeling of tutor rights is different from the current implementation. It might also be a nice design, if you can be tutor for an exercise, without (yet) having a group. This would grant some access rights already, I think.

grantTutorRights(ident uid, ident username, ident exerciseId, ident groupId) {
  assume exists /account[uid]/assistant[exerciseId];
 
  assume exists /account[username]; # implicitly true in OO implementations
  assume exists /exercise[exerciseId]/group[groupId];
 
  assume not exists /account[username]/tutor[exerciseId]/group[groupId]);
  assume not exists /exercise[exerciseId]/group[groupId]/tutor[username];
    # implied by integrity and the assumption before
 
  if not exists /account[username]/tutor[exerciseId] then # we could split the tutor rights here
    insert /account[username] <tutor exercise=[exerciseId] />;
  fi
  insert /account[username]/tutor[exerciseId] <group id=[groupId] />;
  insert /exercise[exerciseId]/group[groupId] <tutor account=[account] />;
}
revokeTutorRights(ident uid, ident username, ident exerciseId, ident groupId) {
  assume exists /account[uid]/assistant[exerciseId];
 
  assume exists /account[username]/tutor[exerciseId]/group[groupId];
  assume exists /exercise[exerciseId]/group[groupId]/tutor[username];
    # implied by integrity and the assumption before
 
  remove /account[username]/tutor[exerciseId]/group[groupId];
  if size(/account[username]/tutor[exerciseId]/group) = 0 then # should this be an additional procedure?
    remove /account[username]/tutor[exerciseId];
  fi
  remove /exercise[exerciseId]/group[groupId]/tutor[username];
}

Associated to Exam

These are the associated procedures for Exam Management and Grades, i.e. one of their parameters is an id of an exam and they will most likely be offered in a corresponding Exam class in an OO setting. Again, these procedures might be offered in other classes, too.

Change Attributes

changeAttributes(ident uid, ident id, string title, string date, string time, string location) {
  assume exists /account[uid]/admin || exists /account[uid]/examiner[id];
 
  assume exists /exam[id]; # implicitly true in OO implementations
 
  update /exam[id]/title title;
  update /exam[id]/date date;
  update /exam[id]/time time;
  update /exam[id]/location location;
}

Examiner Management

grantExaminerRights(ident uid, ident username, ident examId) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]; # implicitly true in OO implementations
  assume exists /exam[examId];
 
  assume not exists /account[username]/examiner[examId]);
  assume not exists /exam[examId]/examiner[username]); # implied by integrity and the assumption before
 
  insert /account[username] <examiner exam=[examId] />;
  insert /exam[examId] <examiner account=[username] />;
}
revokeExaminerRights(ident uid, ident username, ident examId) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]/examiner[examId]; # implies the account exists, which is implicitly true anyway
  assume exists /exam[examId]/examiner[username]; # implied by integrity and the assumption before
 
  remove /account[username]/examiner[examId];
  remove /exam[examId]/examiner[username];
}

Task Management

Results depend on tasks, so deleting them is impossible, if they are still referenced. If this is really necessary, the host language has to use the deleteResult procedures first.

createTask(ident uid, ident id, ident taskId, double maxPoints) {
  assume exists /account[uid]/examiner[id];
 
  assume exists /exam[id]; # implicitly true in OO implementations
  assume not exists /exam[id]/task[taskId];
 
  assume maxPoints >= 0;
 
  insert /exam[id] <task id=[taskId] maxPoints=[maxPoints] />;
}
deleteTask(ident uid, ident id, ident taskId) {
  assume exists /account[uid]/examiner[id];
 
  assume exists /exam[id]/task[taskId]; # implies the exam exists, which is implicitly true anyway
 
  assume size(/exam[id]/participant/result[taskId]) = 0;
 
  remove /exam[id]/task[taskId];
}

Grade Management

The grades only have to be consistent within themselves, nothing depends on them from the outside.

Changing the values of a grade is a method currently present in the implementation, which can be done by removing the grade and adding it. An additional procedure for this might make sense though.

createGrade(ident uid, ident id, ident gradeId, string name, double value, double minPoints) {
  assume exists /account[uid]/examiner[id];
 
  assume exists /exam[id]; # implicitly true in OO implementations
  assume not exists /exam[id]/grade[gradeId];
 
  assume count(value, /exam[id]/grade/value) = 0;
  assume count(minPoints, /exam[id]/grade/minPoints) = 0;
 
  assume exists /exam[id]/grade[x] && /exam[id]/grade[x]/value < value -> /exam[id]/grade[x]/minPoints > minPoints;
  assume exists /exam[id]/grade[x] && value < /exam[id]/grade[x]/value -> minPoints > /exam[id]/grade[x]/minPoints;
 
  insert /exam[id] <grade id=[gradeId] name=[name] value=[value] minPoints=[minPoints] />;
}
deleteGrade(ident uid, ident id, ident gradeId) {
  assume exists /account[uid]/examiner[id];
 
  assume exists /exam[id]/grade[gradeId]; # implies the exam exists, which is implicitly true anyway
 
  remove /exam[id]/grade[gradeId];
}

Participant Management

Currently, the participants are not hardwired to an account, I just changed that fact for the schema. Besides that, participants stand for themselves, so deleting one does not affect anything.

openRegistration(ident uid, ident id) {
  assume exists /account[uid]/examiner[id];
 
  assume exists /exam[id];
 
  assume not /exam[id]/free;
 
  update /exam[id]/free true;
}
closeRegistration(ident uid, ident id) {
  assume exists /account[uid]/examiner[id];
 
  assume exists /exam[id];
 
  assume /exam[id]/free;
 
  update /exam[id]/free false;
}
addParticipant(ident uid, ident id, ident studentId) {
  assume exists /account[uid]/student && /account[uid]/student/id = studentId && /exam[id]/free
      || exists /account[uid]/examiner[id];
 
  assume exists /exam[id]; # implicitly true in OO implementations
  assume count (studentId, /account/student/id) = 1;
 
  assume not exists /exam[id]/participant[studentId];
 
  insert /exam[id]/participant[studentId];
}
removeParticipant(ident uid, ident id, ident studentId) {
  assume exists /account[uid]/student && /account[uid]/student/id = studentId && /exam[id]/free
      || exists /account[uid]/examiner[id];
 
  assume exists /exam[id]/participant[studentId]; # implies the exam exists, which is implicitly true anyway
 
  assume size(/exam[id]/participant[studentId]/result) = 0; # don't allow to remove if results are there
 
  remove /exam[id]/participant[studentId];
}

Result Management

Results depend on tasks and have numeric constraints. The procedures can be (and currently are) associated with the Participant class, rather than the Exam class. Basically this means we now have two actually implicit parameters.

Again, changing the values can be done by adding and removing, which also invokes most of the checks. One could offer a change Method of course, which can actually make sense, as the precondition will be easier.

addResult(ident uid, ident id, ident studentId, ident taskId, double points) {
  assume exists /account[uid]/examiner[id];
 
  assume exists /exam[id]/participant[studentId]; # can also be implicitly true in an OO language
  assume exists /exam[id]/task[taskId];
 
  assume not exists /exam[id]/participant[studentId]/result[taskId];
 
  assume points >= 0 && points <= /exam[id]/task[taskId]/maxPoints;
 
  insert /exam[id]/participant[studentId] <result task=[taskId] points=[points] />;
}
changeResult(ident uid, ident id, ident studentId, ident taskId, double points) {
  assume exists /account[uid]/examiner[id];
 
  assume exists /exam[id]/participant[studentId];
  assume exists /exam[id]/task[taskId];
 
  assume points >= 0 && points <= /exam[id]/task[taskId]/maxPoints;
 
  assume exists /exam[id]/participant[studentId]/result[taskId];
 
  update /exam[id]/participant[studentId]/result[taskId]/points points;
}
removeResult(ident uid, ident id, ident studentId, ident taskId) {
  assume exists /account[uid]/examiner[id];
 
  assume exists /exam[id]/participant[studentId]/result[taskId];
    # implies the exam, account, student role and task exist by integrity
 
  remove /exam[id]/participant[studentId]/result[taskId];
}
publishResults(ident uid, ident id) {
  assume exists /account[uid]/examiner[id];
 
  assume exists /exam[id];
 
  assume not /exam[id]/published;
 
  update /exam[id]/published true;
}
hideResults(ident uid, ident id) {
  assume exists /account[uid]/examiner[id];
 
  assume exists /exam[id];
 
  assume /exam[id]/published;
 
  update /exam[id]/published false;
}

Associated to Exercise

These are the associated procedures for Exercise Management and Sheets, i.e. one of their parameters is an id of an exercise and they will most likely be offered in a corresponding Exercise class in an OO setting. Again, these procedures might be offered in other classes, too.

Change Attributes

changeAttributes(ident uid, ident id, string lecture, string term) {
  assume exists /account[uid]/admin || exists /account[uid]/assistant[id];
 
  assume exists /exercise[id]; # implicitly true in OO implementations
 
  update /exercise[id]/lecture lecture;
  update /exercise[id]/term term;
}

Assistant Management

The procedures from User Accounts and Roles for the assistant role can be directly reused.

grantAssistantRights(ident uid, ident username, ident exerciseId) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]; # implicitly true in OO implementations
  assume exists /exercise[exerciseId];
 
  assume not exists /account[username]/assistant[exerciseId]);
  assume not exists /exercise[exerciseId]/assistant[username]; # implied by integrity and the assumption before
 
  insert /account[username] <assistant exercise=[exerciseId] />;
  insert /exercise[exerciseId] <assistant account=[username] />;
}
revokeAssistantRights(ident uid, ident username, ident exerciseId) {
  assume exists /account[uid]/admin;
 
  assume exists /account[username]/assistant[exerciseId]; # implies the account exists, which is implicitly true anyway
  assume exists /exercise[exerciseId]/assistant[username]; # implied by integrity and the assumption before
 
  remove /account[username]/assistant[exerciseId];
  remove /exercise[exerciseId]/assistant[username];
}

Group Management

The tutor role from section User Accounts and Roles and the students depend on groups, which restricts deletion. The Exercise Groups are a large enough parts of the schema to have their own section and associated procedures.

createGroup(ident uid, ident id, ident groupId, string day, string time, string location, integer maxSize) {
  assume exists /account[uid]/assistant[id];
 
  assume exists /exercise[id];
  assume not exists /exercise[id]/group[groupId];
 
  assume maxSize >= 0;
  assume day = "Monday" || day = "Tuesday" || ...;
 
  insert /exercise[id] <group id=[groupId] day=[day] time=[time] location=[location] curSize=[0] maxSize=[maxSize] />;
}
deleteGroup(ident uid, ident id, ident groupId) {
  assume exists /account[uid]/assistant[id];
 
  assume exists /exercise[id]/group[groupId];
 
  assume size(/exercise[id]/group[groupId]/tutor) = 0;
  assume count(groupId, /exercise[id]/student/group)) = 0;
 
  remove /exercise[id]/group[groupId];
}

Sheet Management

The student results depend on sheets.

createSheet(ident uid, ident id, ident sheetId, double maxPoints) {
  assume exists /account[uid]/assistant[id];
 
  assume exists /exercise[id];
  assume not exists /exercise[id]/sheet[sheetId];
 
  assume maxPoints >= 0;
 
  insert /exercise[id] <sheet id=[sheetId] maxPoints=[maxPoints] />;
}
deleteSheet(ident uid, ident id, ident sheetId) {
  assume exists /account[uid]/assistant[id];
 
  assume exists /exercise[id]/sheet[sheetId]; # implies existence of the exercise
 
  assume size(/exercise[id]/student/result[sheetId]) = 0;
 
  remove /exercise[id]/sheet[sheetId];
}

Student Management

Students themselves depend on an account, but nothing depends on them; Their results stand for themselves. As with Exercise Groups, Registered Students are large enough to warrant their own section and associated procedures.

registerStudent(ident uid, ident id, ident studentId) {
  assume count (studentId, /account/student/id) = 1;
 
  assume exists /exercise[id] && /exercise[id]/open && 
         exists /account[uid]/student && /account[uid]/student/id = studentId
      || exists /account[uid]/assistant[id];
 
  assume exists /exercise[id];
  assume not exists /exercise[id]/student[studentId];
 
  insert /exercise[id] <student id=[studentId] />;
}
unregisterStudent(ident uid, ident id, ident studentId) {
  assume exists /exercise[id] && /exercise[id]/open && 
         exists /account[uid]/student && /account[uid]/student/id = studentId
      || exists /account[uid]/assistant[id];
 
  assume exists /exercise[id]/student[studentId]; # implies the exercise exists
 
  assume size(/exercise[id]/student[studentId]/result) = 0; # don't allow unregistering if results are there
  assume not exists /exercise[id]/student[studentId]/group; # don't allow if signed in a group
 
  remove /exercise[id]/student[studentId];
}
openSignUp(ident uid, ident id) {
  assume exists /account[uid]/assistant[id];
 
  assume exists /exercise[id];
 
  assume not /exercise[id]/open;
 
  update /exercise[id]/open true;
}
closeSignUp(ident uid, ident id) {
  assume exists /account[uid]/assistant[id];
 
  assume exists /exercise[id];
 
  assume /exercise[id]/open;
 
  update /exercise[id]/open false;
}

Associated to Group

These are the associated procedures for Exercise Groups, i.e. they have two parameters for the exercise id and the group id. They will also most likely be offered in a corresponding Group class in an OO setting, which has an associated Exercise object.

Change Attributes

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;
}

Tutor Management

The procedures for tutor management can be directly taken from the User Accounts and Roles section. In an OO setting this placement of the method in the Group class takes the least number of explicit parameters, as the exercise and group ids are implicit.

grantTutorRights(ident uid, ident username, ident exerciseId, ident groupId) {
  assume exists /account[uid]/assistant[exerciseId];
 
  assume exists /account[username]; # implicitly true in OO implementations
  assume exists /exercise[exerciseId]/group[groupId];
 
  assume not exists /account[username]/tutor[exerciseId]/group[groupId]);
  assume not exists /exercise[exerciseId]/group[groupId]/tutor[username];
    # implied by integrity and the assumption before
 
  if not exists /account[username]/tutor[exerciseId] then # we could split the tutor rights here
    insert /account[username] <tutor exercise=[exerciseId] />;
  fi
  insert /account[username]/tutor[exerciseId] <group id=[groupId] />;
  insert /exercise[exerciseId]/group[groupId] <tutor account=[account] />;
}
revokeTutorRights(ident uid, ident username, ident exerciseId, ident groupId) {
  assume exists /account[uid]/assistant[exerciseId];
 
  assume exists /account[username]/tutor[exerciseId]/group[groupId];
  assume exists /exercise[exerciseId]/group[groupId]/tutor[username];
    # implied by integrity and the assumption before
 
  remove /account[username]/tutor[exerciseId]/group[groupId];
  if size(/account[username]/tutor[exerciseId]/group) = 0 then # should this be an additional procedure?
    remove /account[username]/tutor[exerciseId];
  fi
  remove /exercise[exerciseId]/group[groupId]/tutor[username];
}

Member Management

Another example of another association of procedures; The sign up and out procedures for students from the Exercise Management and Sheets section could also be offered on groups, as they have the necessary parameters (It is not currently realized like this in the implementation).

signUpGroup(ident uid, ident id, ident studentId, ident groupId) {
  assume exists /exercise[id] && /exercise[id]/open && 
         exists /account[uid]/student && /account[uid]/student/id = studentId
      || exists /account[uid]/assistant[id];
 
  assume exists /exercise[id]/student[studentId]; # implies the existence of the exercise
  assume exists /exercise[id]/group[groupId]; # also implies it, but once is really enough
 
  assume not exists /exercise[id]/student[studentId]/group;
  assume /exercise[id]/group[groupId]/curSize < /exercise[id]/group[groupId]/maxSize;
 
  insert /exercise[id]/student[studentId]/group groupId;
  update /exercise[id]/group[groupId]/curSize (/exercise[id]/group[groupId]/curSize + 1);
}
signOutGroup(ident uid, ident id, ident studentId) {
  assume exists /exercise[id] && /exercise[id]/open && 
         exists /account[uid]/student && /account[uid]/student/id = studentId
      || exists /account[uid]/assistant[id];
 
  assume exists /exercise[id]/student[studentId]/group;
    # implies existence of the exercise and student, even the group
 
 
  update /exercise[id]/group[/exercise[id]/student[studentId]/group]/curSize
    (/exercise[id]/group[/exercise[id]/student[studentId]/group]/curSize - 1)
  remove /exercise[id]/student[studentId]/group;
}

Associated to Student

These are the associated procedures for Registered Students, i.e. they have two parameters for the exercise id and the student id. They will also most likely be offered in a corresponding Student class in an OO setting, which has an associated Exercise object.

Exercise Registration

Before a student can sign up for a group, he has to register for the exercise in general. (Which is not a student method in the current implementation.)

registerStudent(ident uid, ident id, ident studentId) {
  assume count (studentId, /account/student/id) = 1;
 
  assume exists /exercise[id] && /exercise[id]/open && 
         exists /account[uid]/student && /account[uid]/student/id = studentId
      || exists /account[uid]/assistant[id];
 
  assume exists /exercise[id];
  assume not exists /exercise[id]/student[studentId];
 
  insert /exercise[id] <student id=[studentId] />;
}
unregisterStudent(ident uid, ident id, ident studentId) {
  assume exists /exercise[id] && /exercise[id]/open && 
         exists /account[uid]/student && /account[uid]/student/id = studentId
      || exists /account[uid]/assistant[id];
 
  assume exists /exercise[id]/student[studentId]; # implies the exercise exists
 
  assume size(/exercise[id]/student[studentId]/result) = 0; # don't allow unregistering if results are there
  assume not exists /exercise[id]/student[studentId]/group; # don't allow if signed in a group
 
  remove /exercise[id]/student[studentId];
}

Sign-Up and Sign-Out

One of the main things a student can do by himself, signing into and out of groups.

signUpGroup(ident uid, ident id, ident studentId, ident groupId) {
  assume exists /exercise[id] && /exercise[id]/open && 
         exists /account[uid]/student && /account[uid]/student/id = studentId
      || exists /account[uid]/assistant[id];
 
  assume exists /exercise[id]/student[studentId]; # implies the existence of the exercise
  assume exists /exercise[id]/group[groupId]; # also implies it, but once is really enough
 
  assume not exists /exercise[id]/student[studentId]/group;
  assume /exercise[id]/group[groupId]/curSize < /exercise[id]/group[groupId]/maxSize;
 
  insert /exercise[id]/student[studentId]/group groupId;
  update /exercise[id]/group[groupId]/curSize (/exercise[id]/group[groupId]/curSize + 1);
}
signOutGroup(ident uid, ident id, ident studentId) {
  assume exists /exercise[id] && /exercise[id]/open && 
         exists /account[uid]/student && /account[uid]/student/id = studentId
      || exists /account[uid]/assistant[id];
 
  assume exists /exercise[id]/student[studentId]/group;
    # implies existence of the exercise and student, even the group
 
 
  update /exercise[id]/group[/exercise[id]/student[studentId]/group]/curSize
    (/exercise[id]/group[/exercise[id]/student[studentId]/group]/curSize - 1)
  remove /exercise[id]/student[studentId]/group;
}

Team Assignment

The tutors assign teams to the students of their groups.

assignTeam(ident uid, ident id, ident studentId, ident teamId) {
  assume exists /account[uid]/tutor[id]/group[/exercise[id]/student[studentId]/group];
    # implies the existence of the student, the exercise, the group and enough rights by a tutor account
 
  assume not exists /exercise[id]/student[studentId]/team;
 
  insert /exercise[id]/student[studentId]/team teamId;
}
leaveTeam(ident uid, ident id, ident studentId) {
  assume exists /account[uid]/tutor[id]/group[/exercise[id]/student[studentId]/group];
    # implies the existence of the student, the exercise, the group and enough rights by a tutor account
 
  assume exists /exercise[id]/student[studentId]/team;
 
  remove /exercise[id]/student[studentId]/team;
}

Result Management

addResult(ident uid, ident id, ident studentId, ident sheetId, double points) {
  assume exists /account[uid]/assistant[id] 
      || exists /account[uid]/tutor[id]/group[/exercise[id]/student[studentId]/group];
 
  assume exists /exercise[id]/student[studentId]; # implies the existence of the exercise
  assume exists /exercise[id]/sheet[sheetId]; # dito
 
  assume not exists /exercise[id]/student[studentId]/result[sheetId];
 
  assume points >= 0 && points <= /exercise[id]/sheet[sheetId]/maxPoints;
 
  insert /exercise[id]/student[studentId] <result sheet=[sheetId] points=[points] />;
}
changeResult(ident uid, ident id, ident studentId, ident sheetId, double points) {
  assume exists /account[uid]/assistant[id]
      || exists /account[uid]/tutor[id]/group[/exercise[id]/student[studentId]/group];
 
  assume exists /exercise[id]/student[studentId]; # implies the existence of the exercise
  assume exists /exercise[id]/sheet[sheetId]; # dito
 
  assume points >= 0 && points <= /exercise[id]/sheet[sheetId]/maxPoints;
 
  assume exists /exercise[id]/student[studentId]/result[sheetId];
 
  update /exercise[id]/student[studentId]/result[sheetId]/points points;
}
removeResult(ident uid, ident id, ident studentId, ident sheetId) {
  assume exists /account[uid]/assistant[id]
      || exists /account[uid]/tutor[id]/group[/exercise[id]/student[studentId]/group];
 
  assume exists /exercise[id]/student[studentId]/result[sheetId]; # implies the existence of pretty much everything
 
  remove /exercise[id]/student[studentId]/result[sheetId];
}