** Sample solution to SE304 Lab 5
** Author: Gareth Carter

module STUDENT {

*[Student]*
[Nat String]

** Define the signatures of the operations in the STUDENT module

** Not a behavioural operator, but a constructor of an empty Student
op newStudent : -> Student

** Operators on the class
bop setStudentID : Student Nat -> Student
bop setStudentName : Student String -> Student
bop setStudentSubject1 : Student String -> Student
bop setStudentSubject2 : Student String -> Student
bop getStudentID : Student -> Nat
bop getStudentName : Student -> String
bop getStudentSubject1 : Student -> String
bop getStudentSubject2 : Student -> String


** !!!!NOT REQUIRED FOR LAB 8!!!!!

** Define the meanings of the operations
var I : Nat    ** using these variables
var N : String
var S : Student

** Define getStudentID
eq getStudentID(setStudentID(S,I)) = I .                                  ** base case
eq getStudentID(setStudentName(S,N)) = getStudentID(S) .
eq getStudentID(setStudentSubject1(S,N)) = getStudentID(S) .
eq getStudentID(setStudentSubject2(S,N)) = getStudentID(S) .

** Define getStudentName
eq getStudentName(setStudentName(S,N)) = N .                              ** base case
eq getStudentName(setStudentID(S,I)) = getStudentName(S) .
eq getStudentName(setStudentSubject1(S,N)) = getStudentName(S) .
eq getStudentName(setStudentSubject2(S,N)) = getStudentName(S) .

** Define getStudentSubject1
eq getStudentSubject1(setStudentSubject1(S,N)) = N .                      ** base case
eq getStudentSubject1(setStudentID(S,I)) = getStudentSubject1(S) .
eq getStudentSubject1(setStudentName(S,N)) = getStudentSubject1(S) .
eq getStudentSubject1(setStudentSubject2(S,N)) = getStudentSubject1(S) .

** Define getStudentSubject2
eq getStudentSubject2(setStudentSubject2(S,N)) = N .                      ** base case
eq getStudentSubject2(setStudentID(S,I)) = getStudentSubject2(S) .
eq getStudentSubject2(setStudentName(S,N)) = getStudentSubject2(S) .
eq getStudentSubject2(setStudentSubject1(S,N)) = getStudentSubject2(S) .

}


module ADMIN {
 *[Admin]*
 [Nat String Student]

** Define the signatures of the operations in the Admin module
 op emptyAdmin : -> Admin
 bop createStudent : Admin String Nat String String -> Admin
 bop printStudentInfo : Admin Student -> Admin
}