:- module(_,[loop/2],[assertions,regtypes,nativeprops]).

% a simple increment program, adapded from the `Incr` example of the
% Interproc analyzer
%   http://pop-art.inrialpes.fr/interproc/interprocweb.cgi
%
% proc incr (x:int) returns (y:int)
% begin
%   y = x+1;
% end
%
% var i:int;
% begin
%   i = 0;
%   while (i<=10) do
%     i = incr(i);
%   done;
% end

:- entry loop(X,Y) : constraint([X >= 0]).
:- pred loop(X,Y) : constraint([X >= 0]) => constraint([Y >= 10]).

loop(X,Y) :- X > 10, !, Y = X.
loop(X,Y) :-
        inc(X,X1),
        loop(X1,Y).

:- pred inc(A,B) : constraint([A=A]) => constraint([B > A]).

inc(I,I1) :- I1 is I + 1.
