(*
 * As of 27feb09, things work here, except for the two commented-out cases.
 * The first case is the result of list index out-of-bounds not being properly
 * handled.  There's now code in doArrayRef to issue a runtime error message.
 * However, the propogation of the null Value does not work after the error is
 * issued.  The proper solution to this problem is to make the longjmp error
 * handling in the interpreter work properly.  This is a TODO item, as
 * indicated by comments in interp.c and the bug log.
 *
 * The second non-functioning case is due the interpreter being called, even
 * after a type checking error is detected.  In all likelihood, this will be
 * easily fixed by having translator.c check for all cases of type checking
 * failure, and not calling the interpreter thereafter.
 *)
op w(l:integer*) -> (l':integer*)
    pre: forall (e in l) e >= 0;
    post: if (#l' = #l) then forall (i in [1..#l]) l'[i] = l[i] + 1;
end;

> w([1,2,3]) ?-> ([2,3,4]);	-- should be { true, true }
> w([1,2,3]) ?-> ([2,3,5]);	-- should be { true, false }
> w([1,2,-1]) ?-> ([2,3,0]);	-- should be { false, nil }
> w([1,2,-1]) ?-> ([2,3,0]);	-- should be { false, nil }
> w([1,2,3]) ?-> ([2,3]);	-- should be { true, true } -- WEAK, but correct

> w([1]) ?-> [2];		-- should be { true, true } 
> w([]) ?-> ([]);		-- should be { true, true }

obj ValidationTuple = boolean and boolean;
var result: ValidationTuple;


(*
 * The remaining lines illustrate an as-yet undocumented feature for accessing
 * tuple fields by constant integer position.  It's been described in the
 * implementation notes for some time, but not the reference manual.  Code has
 * been added to chkRecordRef and RecordRef to support this feature.  It's
 * particularly useful for accessing the results of a validation call, since
 * the return value is a boolean 2-tuple, but without any names for tuple
 * fields.  This feature has exactly the same semantics as ML's '#' operator,
 * for accessing tuple component.
 *)
> set result = w([1,2,3]) ?-> ([2,3,5]);	-- { true, false }
> result.1;					-- true
> result.2;					-- false
--> result.3;					-- type check error, but should
						-- cause interp not be called