(****
 *
 * One of the fundamental questions to ask about pre- and postconditions is if
 * they're strong enough.  In general, adding additional predicate clauses
 * strengthens the conditions. For example, the true precondition for
 * \fCAddUser\fP is relatively weaker than one that specifies input
 * constraints, such as the name or id not being nil.
 *
 * In general, there are two aims to strengthening a specification:
 *
 *     1. Ensuring that all user-level requirements are met.
 *     2. Ensuring that a system implementation works properly.
 *
 * The first aim is accomplished via continued consultation with the end user.
 * Accomplishing the second aim requires an experienced analyst, who
 * understands the kinds of problems that can arise in an implementation.
 *
 * In the case of the user database example, as well as similar database
 * applications, an area of potential implementation error is the introduction
 * of spurious entries into the database and/or the spurious deletion of
 * entries.  That is, an AddUser implementation could add a record properly,
 * but also add other junk that does not belong there, or delete existing
 * records that should stay there.
 *
 * So, a question to ask of the AddUser postcondition is this: Does it deal
 * with the case where an implementation erroneously adds extra records into
 * the database, or deletes ones that it shouldn't?  This question can be asked
 * (and answered) with some validation examples.
 *
 *)


val ur1 = {"Corwin", "1", nil, nil};
val ur2 = {"Fisher", "2", nil, nil};
val ur3 = {"Other", "3", nil, nil};
val ur4 = {"Extra", "4", nil, nil};
val udb = [ur1, ur2];

(*
 * A database value representing a spurious addition having been made.
 *)
val udb_spurious_addition = udb + ur3 + ur4;

(*
 * A database value representing a spurious deletion having been made.
 *)
val udb_spurious_deletion = udb + ur3 - ur2;

> print("Expected results of AddUser(udb,ur3)?->(udb_spurious_addition) are ...\n");
> print("    Hmm, let's see.\n");
> AddUser(udb,ur3)?->(udb_spurious_addition);

> print("\nExpected results of AddUser(udb,ur3)?->(udb_spurious_deletion) are ... \n");
> print("    Hmm, let's see, again.\n");
> AddUser(udb,ur3)?->(udb_spurious_deletion);