(**
 * 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 that idea that an empty precondition is unconditionally true, and
 * an empty postcondition is unconditionally nil.
 *)

(*
 * Define some working test variables.
 *)
var ur1,ur2,ur3: UserRecord;
var udb, udb_added: UserDB;

(*
 * Create some testing values.
 *)
> set ur1 = {"Corwin", "1", nil, nil};
> set ur2 = {"Fisher", "2", nil, nil};
> set ur3 = {"Other", "3", nil, nil};

> set udb = [ur1, ur2];
> set udb_added = udb + ur3;

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