(*
 * This file is a copy of adduser-strengthened.fmsl, with the addition of
 * logic equivalent to the AddUser postcond, written as a recursive fucntion.
 * The point is to test that the 
 *)

operation AddUser
    inputs: udb:UserDB, ur:UserRecord;
    outputs: udb':UserDB;

    postcondition:
        (*
         * The given user record is in the output UserDB.
         *)
        (ur in udb')

            and

        (*
         * All the other records in the output db are those from the input db,
         * and only those.
         *)
        forall (ur':UserRecord | ur' != ur)
            if (ur' in udb)
            then (ur' in udb')
            else not (ur' in udb');

end AddUser;

var ur_universe:UserDB;

> "ur_universe = ";
> set ur_universe = [ { "Other", "3", nil, nil }, { "Corwin", "1", nil, nil }, { "Fisher", "2", nil, nil }, { "Extra", "4", nil, nil } ];

var count: integer;

(*
 * Operation e is the logical equivalent of the AddUser postcond.  It's sent a
 * UserRecord universe in the ur_universe parameter.  The other parms are those
 * that appear in the postcond logic.
 *)
op e(ur:UserRecord, udb:UserDB, udb':UserDB, ur_universe:UserDB) =
    if (#ur_universe = 0) then true
    else
	e1(ur, ur_universe[1], udb, udb')
	    and
	e(ur, udb, udb', ur_universe[2:#ur_universe]);

(*
 * Operation e1 is one iteration of the body of the postcond quantifier.
 *)
op e1(ur:UserRecord, ur':UserRecord, udb:UserDB, udb':UserDB) = (
	set count = count + 1;

        ur in udb'

	    and

	if (ur' != ur) then
            if (ur' in udb)
            then (ur' in udb')
            else not (ur' in udb');
);

> set count = 0;
> "e's 1st output; should be false";
> e(ur3, udb, udb_spurious_addition, ur_universe);
> "e's 2nd output; should be false";
> e(ur3, udb, udb_spurious_deletion, ur_universe);
> "e's 3rd output; should be true:";
> e(ur3, udb, udb+ur3, ur_universe);
> count;