% ================================================================= :- pred constr(bool). :- mode constr(in). :- ignore constr/1. % ================================================================= % Program. ascending sorting :- pred insertionsort(list(int),list(int)). :- mode insertionsort(in,out). insertionsort([],[]). insertionsort([X],[Y]). % error: Y --> X insertionsort([X|Xs],S) :- ord_ins(X,TS,S), insertionsort(Xs,TS). :- pred ord_ins(int,list(int),list(int)). :- mode ord_ins(in,in,out). ord_ins(A,[],[A]). ord_ins(A,[B|Xs],[A,B|Xs]) :- constr( A=B ), ord_ins(A,Xs,AXs). % ================================================================= % catamorphism %----- listsum --- sum of integers in nodes of the given list. :- pred listsum(list(int),int). :- mode listsum(in,out). :- cata listsum/2-1. listsum([],S) :- S=0. listsum([H|T],S) :- S=(H+ST), listsum(T,ST). % ================================================================= % Verification. % Property: :- pred ff1. ff1 :- constr( ~(LS=SS)), listsum(L,LS), listsum(S,SS), insertionsort(L,S). %% contracts (postcondition: true) % %:- spec ord_ins(A,L1,L2) ==> listsum(L1,SL1), listsum(L2,SL2). % ================================================================= :- query ff1/0. % ================================================================= % Catamorphic abstraction :- cata_abs list(int) ==> listsum(L1,SL1). % ================================================================