obj Artifact;
  obj Errors =  el:ErrorList and s:ListState;
  obj ErrorList =  Error*;
  obj Error;
  obj ListState =  integer
    description: (*
	List state = 0 means that there are no errors.  List state between 1
	and the length of the list means that errors are being processed by
	NextError.  When the value of list state goes > the length of the
	errors list, the state is set back to 1 by NextError.
    *);
  end;
	

  op Check(Artifact)->(es:Errors)
    post:
	(*
	 * Specific logic for the kind of checking performed, including setting
	 * elements of es.el.
	 *)
	...

	    and

	(*
	 * Set the state of the returning errors to 0 if there no errors, to 1
	 * otherwise.
	 *)
	(es.s = if (#(es.el) = 0) then 0 else 1);
    end;

  op NextError(es:Errors)->(e:Error, es':Errors)
    post:
	(*
	 * If the error state is 0, return the tuple {nil, unchanged list}.
	 *)
	if (es.s = 0) then
	    (e = nil) and (es' = es)

	(*
	 * If the error state > length of the list, return the tuple {nil,
	 * errors with the state set back to 1 and the errors list unchanged}.
	 *)
	else if (es.s > #(es.el)) then
	    (e = nil) and (es'.s = 1) and (es'.el = es.el)

	(*
	 * If the error state is between 1 and the length of the list, return
	 * the tuple {error at the current state number, errors with the state
	 * incremented by 1 and the errors list unchanged}.
	 *)
	else
	    (e = es.el[es.s]) and (es'.s = es.s + 1) and (es'.el = es.el);
  end;