p q r	(p and q) xor r 	if p then q else r	(p and q) or r

0 0 0    0 and 0  xor 0 = 0	if 0 then 0 else 0 = 0	 0 and 0  or 0 = 0
0 0 1	 0 and 0  xor 1 = 1	if 0 then 0 else 1 = 1	 0 and 0  or 1 = 1
0 1 0	 0 and 1  xor 0 = 1	if 0 then 1 else 0 = 0	 0 and 1  or 0 = 0
0 1 1	 0 and 1  xor 1 = 1	if 0 then 1 else 1 = 1	 0 and 1  or 1 = 1
1 0 0	 1 and 0  xor 0 = 0	if 1 then 0 else 0 = 0	 1 and 0  or 0 = 0
1 0 1	 1 and 0  xor 1 = 1	if 1 then 0 else 1 = 0	 1 and 0  or 1 = 1 **
1 1 0	 1 and 1  xor 0 = 1	if 1 then 1 else 0 = 1	 1 and 1  or 0 = 1
1 1 1	 1 and 1  xor 1 = 0	if 1 then 1 else 1 = 1	 1 and 1  or 1 = 1

The deal is, the following FindUser postcond does not cut the mustard

  operation FindUser is
    inputs: udb:UserDB, id:Id;
    outputs: ur':UserRecord;

    precondition: ;

    postcondition:
        (*
         * If there is a record with the given id in the input db, then the
         * output record is equal to that record, otherwise the output record
         * is empty.
         *)
        (exists (ur in udb) (ur.id = id) and (ur' = ur))
            or        -- or even xor
        (ur' = nil);

    description: (*
        Find a user by unique id.
    *);
  end FindUser;

whereas the following one does:

    \& ...

    postcondition:
        (*
         * If there is a record with the given id in the input db, then the
         * output record is equal to that record, otherwise the output record
         * is empty.
         *)
        (exists (ur in udb) (ur.id = id) and (ur' = ur))
            or
        (not (exists (ur in udb) (ur.id = id)) and (ur' = nil));