(****
 *

 * Of note here is the distinction between validating a degenerate
 * postcondition, versus a postcondition that explicitly evaluates to nil.  In
 * the former case, the validation itself returns a nil.  In the latter case,
 * the validation returns true or false, based on the logic of the
 * postcondition.


*)


(*
 * Create some testing values.
 *)
val ur1:UserRecord = {"Corwin", "1", nil, nil};
val ur2:UserRecord = {"Fisher", "2", nil, nil};
val ur3:UserRecord = {"Other", "3", nil, nil};
val ur4:UserRecord = {"Extra", "4", nil, nil};
val udb = [ur1, ur2];
val udb_added = udb + ur3;
val udb_spurious_addition = udb + ur3 + ur4;
val udb_spurious_deletion = udb + ur3 - ur2;

> "Expected results of FindUser(udb,''Other'')?->ur3 are { true, true }:";
> FindUserByName(udb,"Other")?->ur3;