/* Sample solution to SE304 Lab 1
** Author: Gareth Carter
*/

/* Student: Design Decisions.

   Students each take two subjects
   They cannot take the same subject twice, we maintain this fact
   We assume the class will never be asked to override the subject
    values, creating a situation wherein a student can take two subjects
   We allow students to change subjects, on the assumption that this has
    not happened.
*/

class Student{
 private /*@ non_null @*/ String name;
 private /*@ spec_public @*/ int id;
 private /*@ spec_public non_null @*/ String subject1;
 private /*@ spec_public non_null @*/ String subject2;

 /*@ invariant id>0; @*/
 /*@ invariant !subject1.equals(subject2); @*/

 /*@ requires i>0 &
   @          !s1.equals(s2);
   @*/
 public Student(String n, int i, String s1, String s2){
    name=n;
    id=i;
    subject1=s1;
    subject2=s2;
 }

 public /*@ pure non_null @*/ String getName(){
    return name;
 }

 public /*@ pure @*/ int getID(){
    return id;
 }

 public /*@ pure non_null @*/ String getSubject1(){
    return subject1;
 }

 public /*@ pure non_null @*/ String getSubject2(){
    return subject2;
 }

 /*@ requires !s1.equals(subject2); @*/
 public void setSubject1(/*@ non_null @*/ String s1){
    subject1=s1;
 }

 /*@ requires !subject1.equals(s2); @*/
 public void setSubject2(/*@ non_null @*/ String s2){
    subject2=s2;
 }

}

/* Admin: Design Decisions.

  We keep a track of the students, searchable on their id number (position in array)
  If the system is asked to accept a student that takes the same subject twice, we will
   refuse the subject, otherwise, we create the student and add him/her to our records
  We will print the information of any valid student (we can assume the student does not
   take the same subject twice).
*/
class Admin{
    Student[] allTheStudents = {new Student("John Galt",1,"Economics","Geography"),
                                new Student("Dagny Taggart",2,"Engineering","Economics"),
                                new Student("Hank Reardon",3,"Physics","Chemistry"),
                                new Student("Francisco d'Anconais",4,"Philosophy","Politics")
                               };

    public Admin(){

    }

    public void addStudent(/*@ non_null @*/ String n,
                           /*@ non_null @*/ String s1,
                           /*@ non_null @*/ String s2){
        if(s1.equals(s2)){
            System.out.println("Subjects are the same, please try again");
        }else{
            Student[] temp = new Student[allTheStudents.length+1];
            for(int i=0; i<allTheStudents.length; i++){
                temp[i]=allTheStudents[i];
            }
            temp[temp.length-1]=new Student(n,allTheStudents.length,s1,s2);
            allTheStudents=temp;
        }
    }

    public void printStudent(/*@ non_null @*/ Student s){
        System.out.println("Student: " + s.getName() + ", Id: " + s.getID() +
                           ", Subject1: " + s.getSubject1() + ", Subject2: " +
                           s.getSubject2() + ".");
    }
}

