(****
 *
 * 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 ur5:UserRecord = {"Other", "5", nil, nil};
val ur6:UserRecord = {"Other", "6", 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;
val url = [ur3];
val udb6 = udb_added + ur4 + ur5 + ur6;
val found_other = [ur3, ur5, ur6];
val found_some = [ur3, ur6];
val found_too_many = [ur3, ur5, ur6, ur6, ur6];

> print("\nExpected results of FindUser(udb,''3'')?->ur3 are\n");
> print("{ true, false }\n");
> FindUser(udb,"3")?->ur3;

> print("\nExpected results of FindUser(udb_added,''3'')?->ur3 are\n");
> print("{ true, true }\n");
> FindUser(udb_added,"3")?->ur3;

> print("\nExpected results of FindUserByName(udb,''Other'')?->ur3 are\n");
> print("{ true, false }\n");
> FindUserByName(udb,"Other")?->url;

> print("\nExpected results of FindUserByName(udb_added,''Other'')?->ur3 are\n");
> print("{ true, true }\n");
> FindUserByName(udb_added,"Other")?->url;

> print("\nExpected results of FindUserByName(udb6, ''Other'')?->found_other are\n");
> print("{ true, true }\n");
> FindUserByName(udb6, "Other")?->found_other;

> print("\nExpected results of FindUserByName(udb6, ''Other'')?->found_some are\n");
> print("{ true, false }\n");
> FindUserByName(udb6, "Other")?->found_some;

> print("\nExpected results of FindUserByName(udb6, ''Other'')?->found_too_many are\n");
> print("{ true, true }\n");
> FindUserByName(udb6, "Other")?->found_too_many;

(*
 * The following function could be used in the FindUserByName postcond to
 * disallow duplicate records in the output list.
 *)
function NoUserRecordDups(url:UserRecord*) =
    forall (ur in url) not (ur in (url - ur));

> print("\nNext three outputs should be false, true, true\n");
> NoUserRecordDups(found_too_many);
> NoUserRecordDups(found_some);
> NoUserRecordDups(found_other);