% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% =================================================================
% Program
:- pred append(list(int),list(int),list(int)).
:- mode append(in,in,out).

append([],Ys,Ys).
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).

% ============================================================
% Catamorphisms.
% -------------

% listMax(List,B,Res):  if B then Res is the maximun element of List
:- pred listMax(list(int),bool,int).
:- mode listMax(in,out,out).
:- cata listMax/3-1.

listMax([],B,Res) :- constr( ((~B) & Res=0) ).
listMax([H|T],B,Res) :-
        constr( B & ( Res=ite(BT, ite(H>ResT,H,ResT), H) ) ),
        listMax(T,BT,ResT).

% =================================================================
% ------ Verification of contract on append:

:- pred ff1.
ff1 :-
        constr(~((( ((BXs &  BYs) => ( BZs & (MZs=ite(MXs>MYs,MXs,MYs)))) & % Xs not empty and Ys not empty
                   ((BXs & ~BYs) => ( BZs & (MZs=MXs) ))) &  % Xs not empty and Ys empty
                  ((~BXs &  BYs) => ( BZs & (MZs=MYs) ))) &  % Xs empty and Ys not empty
                  ((~BXs & ~BYs) =  (~BZs)) )),              % Xs empty and Ys empty             
        listMax(Xs,BXs,MXs), listMax(Ys,BYs,MYs), listMax(Zs,BZs,MZs),
        append(Xs,Ys,Zs).

% =================================================================
:- query ff1/0.
% =================================================================