(** This file contains a discussion of fixes to
 *
 *  CSC 590 Fall 1994
 *  Some Possible Assignment #3 Solutions
 *
 *  Search for comments "WAS:", "NOW IS:", and "FIX"
 *
 **)


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

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

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


(* WAS:
object Card;
 *)

(* NOW IS: *)
object Card =  id:string and ...; 
(* FIX:        ^^^^^^^^^ at least the id field is necessary, since it's
			 referenced in the postcond of printRolodex. *)


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 *)  

(* WAS:
       or rf' = rf + r				*)

(* NOW IS: *)
       or (rf' = rf + r)
(* FIX:   ^            ^ these parens are needed for precedence *)

       and

       (*  The Rolodex name is assigned by the user *)

(* WAS:
        (rf'.r.name = name)						*)

(* NOW IS: *)
        (r'.name = name)
(* FIX: ^              ^ these parens are needed for precedence *)
(* FIX:  ^^ use r', not rf'.r.
(* DISCUSSION: rf' is a list, not a tuple, so rf'.r is incorrect.  Use of r' in
 *             this context solves the type checking problem.  However, the r'
 *             that is visible in the current universal quantifier scope does
 *             not appear to be the Rolodex that is needed for the requirement
 *             stated in the comment above, i.e.,
 *
 *		     The Rolodex name is assigned by the user
 *
 *	       Rather, an existential quantifier should be used as the outer
 *	       scope of this postcondition to instantiate a subject Rolodex.
 *)
       and

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

(* NOW IS: *)
       (r'.cards = nil)
(* FIX:    ^^^^^ use cards instead of CardList.  cards is the field name,
 *		 CardList is the type of field.  Also, the same fix as above
 *		 was made to rf'.r and the same discussion applies. *)

       and

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

(* NOW IS: *)
       (r'.isOpen = true);
(* FIX: same fix as above to rf'.r; same discussion applies. *)

  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) (*
 FIX: ^        ^     ^               ^ parens are needed for precedence *)

      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) (*
 FIX: ^        ^     ^               ^ parens are needed for precedence *)

      and

      (* The name has been changed *)
      (r.name = name) (*
 FIX: ^             ^ parens are needed for precedence *)
  
      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;
(* FIX:		 ^^^       ^^^   these references require definition of id
 *				 field earlier. *)

end printRolodex;