(*
 * This a very simple specification for a Database objects and related
 * operations.  To run it through the spec checker, use the following UNIX
 * command:
 *
 *	% ~gfisher/440/bin/rsl db-v3.rsl
 *
 *)

object Database
    components: Record*;
    description:
	(* A database is an object that contains zero or more Records *);
end Database;


object Record
    components: Name and Age and Address;
    description:
	(* A Record contains Name, Age, and Address components. *);
end Record;


operation AddRecord
    inputs: Database, Record;
    outputs: Database;
    description:
	(* AddRecord is a database operation that inserts a new record
	 * into a Database, producing a new database *);
end AddRecord;


(*
 * The following three are atomic objects.  The four built-in atomic types are
 * string, number, boolean, and opaque.
 *)
object Name is string;
object Age is number;
object Address is string;

operation DeleteRecord
    inputs: Database, Name;
    outputs: Database;
    description:
	(* DelRecord is a database operation that deletes a record by name
	 * from a Database, producing a new database *);
end DeleteRecord;


operation ChangeRecord
    inputs: Database, Name, Age, Address;
    outputs: Database;
    description:
	(* ChangeRecord is a database operation that changes the Age and
	 * Address in a record of a given Name, producing a new Database. *);
end ChangeRecord;