(****
 *
 * Another way to simplify the AddUser postcondition is to use a constructive
 * list operator.  With this style of constructive specification, the
 * postcondition logic constructs a concrete value from the inputs.  This value
 * is then compared with the declared operation output.
 *
 * In contrast, an analytic specification states postconditions without using
 * constructive operations.  This is the case in the preceding specifications
 * of AddUser.  In these, the postcondition is stated in terms of boolean
 * operations on the output, without actual construction of an object value.
 *
 * Analytic specifications have the benefit of introducing minimum
 * implementation bias.  Constructive specifications can be useful to simplify
 * specification logic. A complete discussion of analytic versus constructive
 * specification is beyond the scope of this thesis.  Validation invocations
 * can be used with either style.
 *
 * While value construction need not be used in a postcondition, it is
 * definitely required for validations calls.  The point of a validation call
 * is to test constructed values against pre- and postcondition logic.
 *
 * There are different styles to accomplish this.  Which style to use is a
 * matter of convenience and clarity of presentation.  For example, the set-up
 * below creates the same testing values as in the preceding examples, but
 * without using list concatenation or deletion operators.  These tests produce
 * the same results, with either the constructive or analytic AddUser
 * specification.
 *
 *)

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};

> print("Expected retults are\n");
> print("{ true, true }\n");
> AddUser([ur1, ur2], ur3) ?-> [ur1, ur2, ur3];

> print("\nExpected results are\n");
> print("{ true, false }\n");
> AddUser([ur1, ur2], ur3) ?-> [ur1, ur2, ur3, ur4];

> print("\nExpected results of AddUser(udb,ur3)?->(udb_spurious_deletion) are\n");
> print("{ true, false }\n");
> AddUser([ur1, ur2], ur3) ?-> [ur1, ur3];