(*  CSC 590 Fall 1994
    COMMENTS ON Some Possible Assignment #3 Solutions    *)


(****  Rolodex File Operations   *****) 

(*  A RolodexFileSpace is a collection of Rolodexii; the file is the
    persistent object in the Rolodex application              *)

object RolodexFileSpace =  Rolodex*;

(*  A Rolodex is identified by a unique name *)
object Rolodex =  name:string and cards:CardList and isOpen:boolean;
object Card;
object CardList =  Card*;
object Printout =  CardList;

(*  A workspace is the user manifestation of an "open" Rolodex; the
    user performs Rolodex operations in a WorkSpace             *)
object WorkSpace
  components:  Rolodex;
end Workspace;


(*****  AXIOMS       *****)
(*  Only one Rolodex can be open at a time *)
axiom A1 = exists (r:Rolodex | r.isOpen) 
      forall (r':Rolodex | r'!= r) r'.isOpen = false;


(*****  OPERATIONS   *****)
op new(rf:RolodexFile,r:Rolodex,name:string) -> (rf':RolodexFile)
  pre:
      (*   The requested Rolodex name doesn't already exist *)
       not (exists(r':Roldex) r'.name = name);
  post: 
       (*  There is a new Rolodex in the file; all former Roledexii remain *)
       (*  Analytic specification *)
       forall (r':Rolodex) (r' in rf') iff (r' in rf) or (r' = r)
       (*  Constructive specification *)  
       or rf' = rf + r

       and

       (*  The Rolodex name is assigned by the user *)
       rf'.r.name = name

       and

       (*  The new Rolodex is empty *)
       rf'.r.CardList = nil

       and

       (*  The new Rolodex is open *)
       rf'.r.isOpen = true;

  description:
       (*  The user can create a new Rolodex *);
end new;

op open(rf:RolodexFile, name:string) -> (ws:WorkSpace)
  pre:  
      (*  No other Rolodex is open *)
      forall (r in rf) r.isOpen = false;

  post:
      (*  Rolodex name is open *)
      exists (r:Rolodex | r.name = name) r.isOpen = true;

  description:
      (*  The use can open a Rolodex *);
end open;


op save(rf:RolodexFile,r:Rolodex) -> (rf':RolodexFile)
  pre: 
      (* The user is working on a Rolodex *)
      r.isOpen = true;
  
  post:
      (* The open Rolodex has been saved but is still open *) 
      r in rf' and r.isOpen = true

      and

      (* The Rolodex file hasn't been corrupted *)
      forall (r':Rolodex) (r' in rf') iff (r' in rf) or (r' = r);

  description:
      (*  The user can save the open Rolodex  *);
end save;

(*  The user can save the open Rolodex with a new name *)
op saveAs(rf:RolodexFile,r:Rolodex,name:string) -> (rf':RolodexFile)
  pre: 
      (* The user is working on r *)
      r.isOpen = true;
  
  post:
      (* The open Rolodex has been saved but is still open *) 
      r in rf' and r.isOpen = true

      and

      (* The name has been changed *)
      r.name = name 
  
      and
      (* The Rolodex file hasn't been corrupted *)
      forall (r':Rolodex) (r' in rf') iff (r' in rf) or (r' = r);

  description:
      (*  The user can save the open Rolodex  *);
end save;

(*  The user can print a Rolodex sorted by ID *)
op printRolodex(r:Rolodex) -> (p:Printout)
  post: 
         (*  All cards are printed in order *)
         forall (i:integer | i in [1..#p]) 
           forall (j:integer | j in [i+1..#p]) 
             p[i].id < p[j].id;
end printRolodex;