(****
 *
 * The validation tests in the previous step showed that the AddUser
 * postcondition is not strong enough.  The problem is that it allows an output
 * database with extra records, or erroneously deleted records.
 *
 * To strengthen the post condition, we add an additional logic clause that says
 * this: 
 *
 *    Except for the newly added record, all of the records in the output
 *    database are those from the input database, and only those.
 *
 * This new logic can then be tested with the same validation calls that
 * failed on the weaker postcondition.  Here "failed" means that the validation
 * gave a postcondition result of true when it should have been false.
 *
 *
 * The tests given below can be run on the strengthened AddUser postcondition,
 * as well as its simplified version.  In both cases, the results should be the
 * same.
 *
 * The simplified logic can be proved equivalent to the initial version, using
 * a basic logic proof.  Such a proof may in fact be valuable in a fully formal
 * development cycle.  The utility of validation tests is to detect basic flaws
 * in logic, before such proofs are conducted.  Validation tests are useful for
 * obtaining quick, mechanized feedback, short of more time-consuming proofs.
 *
 * Proof tools can be difficult to use when the proof outcome is negative.  In
 * such cases, the tool may not readily reveal the cause of the negative
 * outcome.  The incremental nature of validation tests can be useful in this
 * regard, since it focuses on a single specific test case to be validated.
 * Such focusing can make it easier to debug the logic of a flawed
 * specification than is possible with a proof tool.
 *
 *)


(*
 * Create some testing values.  These are the same as in the preceding test
 * cases, but here the type of the test values is explicitly declared as
 * UserRecord.  It can be argued that these declarations make the spec more
 * clear, which they probably do.  However, the reason the explicit
 * declarations are needed here relates to the creation of value universes,
 * on which unbounded quantifiers rely.  This topic was discussed in Section
 * 3.2, and will be investigated further in upcoming testing examples.
 *)
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;

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

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

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