(***
 *
 * The next step is to test the first version of AddUser with a formal
 * postcondition.  This confirms that the basic idea of the postcondition is
 * correct.  I.e., that the UserRecord to be added is in the updated UserDB.
 * The expected validation result in this case is {true, true}.
 *
 *)


(*
 * Create some testing values.  These are the same as the comment-only version.
 *)
val ur1 = {"Corwin", "1", nil, nil};
val ur2 = {"Fisher", "2", nil, nil};
val ur3 = {"Other", "3", nil, nil};
val udb = [ur1, ur2];
val udb_added = udb + ur3;

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