(***
 *
 * To test the comment-only version of AddUser, give it a simple test case.
 * The expected results are {true, nil}.  This is a degenerate case, in that
 * only comments have been defined for the precondition and postcondition.
 *
 * The point of running this example is just to see what happens.  It
 * reinforces the idea that an empty precondition is unconditionally true, and
 * an empty postcondition is unconditionally nil.
 *
 *)


(*
 * Create some testing values.
 *)
val ur1 = {"Corwin", "1", nil, nil};	-- a sample user record
val ur2 = {"Fisher", "2", nil, nil};	-- another sample user record
val ur3 = {"Other", "3", nil, nil};	-- a record to be added by AddUser
val udb = [ur1, ur2];			-- the initial input database
val udb_added = udb + ur3;		-- the expected result of AddUser

> print("Expected results of AddUser(udb,ur3)?->(udb_added) are\n");
> print("{ true, nil }\n");
> AddUser(udb,ur3)?->(udb_added);