(*
 * Operation with postcondition specifying sorted output.
 *)
operation Sort(l:integer*)->(l':integer*)
    pre: ;
    post:
        forall (i:integer | (i >= 1) and (i < #l))
	    l'[i] < l'[i+1];
end Sort;

(*
 * Version of Sort that uses bounded forall, instead of such-that.
 *)
operation SortBounded(l:integer*)->(l':integer*)
    pre: ;
    post:
        forall (i in [1..#l-1])
	    l'[i] < l'[i+1];
end SortBounded;

(*
 * The postcond error in this function is in the second operand of the
 * such-that clause:
 *
 *     (i <= #l)
 *
 * should be
 *
 *     (i < #l)
 *
 * This error should make the postcond always evaluate to nil, since the
 * out-of-bounds list access l[i+1] should propagate nil, making the entire
 * postcond go nil.
 *)
operation SortWithPostcondError(l:integer*)->(l':integer*)
    pre: ;
    post:
        forall (i:integer | (i >= 1) and (i <= #l))
	    l'[i] < l'[i+1];
end SortWithPostcondError;

(*
 * Version of preceding function that uses bounded quantifier.
 *)
operation SortWithPostcondErrorBounded(l:integer*)->(l':integer*)
    pre: ;
    post:
        forall (i in [1..#l])
	    l'[i] < l'[i+1];
end SortWithPostcondErrorBounded;

(*
 * Force an out-of-bound list access in a postcond;
 *)
operation ForcedPostcondError(l:integer*)->integer
    pre: ;
    post: l[#l + 1] = 1;	-- Unconditional error
end ForcedPostcondError;
    
(*
 * Force an out-of-bound list access in an operation body.
 *)
operation ForcedError(l:integer*)->integer =
    l[#l + 1];

(*
 * Force an out-of-bounds list access in a bounded quantifier body.
 *)
operation ForcedQuantifierErrorBounded(l:integer*)->integer =
    forall (i in [1..2]) l[#l + 1] = 1;

(*
 * Force an out-of-bounds list access in an unbounded quantifier body.
 *)
operation ForcedQuantifierErrorUnbounded(l:integer*)->integer =
    forall (i:integer) l[#l + 1] = 1;

(*
 * Force an out-of-bound list access in a precond;
 *)
operation ForcedPostcondError(l:integer*)->integer
    pre: ;
    post: l[#l + 1] = 1;	-- Unconditional error
end ForcedPostcondError;


var l1,l2,l3,l4:integer*;

(*
 * This is a testing function to try to see what's going on in the bounded
 * quantifier.  It's a hack, but it shouldn't blow up, which it currently
 * does.
 *)
function f1(upper:integer) =
    forall (i in [1..upper]) (
	set l1 = l1 + i;
        true;
    );

(*
 * This is another testing function, with an fully unbounded quantifier body,
 * to help diagnose what's going on with quantifier vars in the type checker.
 *)
function f2(i:integer) =
    forall (i:integer) i > 0;	-- OK, so it's some alternative universe.


> forall (i in [1..100]) true;	-- populate integer univers

> 2;
> set l1 = [0];		-- non-nil initialization, so list concat works
> "Value of l1, before call to f1:";
> l1;
> f1(3);		-- Previously, when commented out, results are different
> "Value of l1, after call to f1:";
> l1;
> #l1-1;
> set l2 = [1,2,3];
> l2[4] > 0;
> forall (i in [1 .. #l2 + 1]) l2[i] > 0;
> l1[#l1 + 1];

> set l3 = [];
> forall (i in [1 .. #l1 + 1]) (set l3 = l3 + l1[i]; true);
> "l3 = ";
> l3;

> set l4 = [];
> forall (i in [1 .. #l1 + 10]) (set l4 = l4 + i; true);
> "l4 = ";
> l4;

> "Validation of Sort([3,2,1]) ?-> [1,2,3] should be {true,true}:";
> Sort([3,2,1]) ?-> [1,2,3];

> "Validation of SortBounded([3,2,1]) ?-> [1,2,3] should be {true,true}:";
> SortBounded([3,2,1]) ?-> [1,2,3];

> "Validation of SortBounded([3,2,1]) ?-> [3,2,1] should be {true,false}:";
> SortBounded([3,2,1]) ?-> [3,2,1];

> "Validation of SortWithPostcondError([3,2,1]) ?-> [1,2,3] should be {true,nil}:";
> SortWithPostcondError([3,2,1]) ?-> [1,2,3];

> "Validation of SortWithPostcondErrorBounded([3,2,1]) ?-> [1,2,3] should be {true,nil}:";
> SortWithPostcondErrorBounded([3,2,1]) ?-> [1,2,3];

> "Validation of ForcedPostcondError([1,2,3]) ?-> 1 should be {true,nil}, preceded by error message:";
> ForcedPostcondError([1,2,3]) ?-> 1;

> "Execution of ForcedError([1,2,3]) should be nil, preceded by error message:";
> ForcedError([1,2,3]);

> "Execution of 'true and ForceError([1,2,3])' should be nil, preceded by error message:";
> true and (ForcedError([1,2,3]) = 10);

> "Execution of ForcedQuantifierErrorBounded([1,2,3]) should be nil, preceded by error message:";
> ForcedQuantifierErrorBounded([1,2,3]);

> "Execution of ForcedQuantifierErrorUnbounded([1,2,3]) should be nil, preceded by error message:";
> ForcedQuantifierErrorUnbounded([1,2,3]);

var l:integer*;

function PopulateInts(i:integer) =
    if (i > 0)
    then PopulateInts(i-1);

> PopulateInts(100);
> set l = [1,2,3];
> set l4 = [];
> forall (i:integer | (i >= 1) and (i <= 40)) (set l4 = l4 + i; true);
> l4;
> set l4 = [];
> forall (i:integer) (set l4 = l4 + i; true);
> l4;