obj Record = name:string and data:Whatever;
obj Whatever;

(*
 * Find a record of the given name in the give Record list.  Return nil if not
 * found.
 *)
op Find(name:string, records:Record*)->found:Record
   post:
      (exists (record in records) (record.name = name) and (found = record))
         or
      (not (exists (record in records) (record.name = name))) and (found = nil);
end;