(*
 * This is a very simple specification for Database objects and related
 * operations.  To run it through the spec checker, use the following
 * command-line invocation:
 *
 *      % rsl db-v3.rsl
 *
 *)

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


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

object Name = string;
object Age = number;
object Address = string;


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;


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;


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;