ZETT

MODULE AbsModule;
IMPORT Out, SYSTEM;

PROCEDURE Abs(x: INTEGER): INTEGER;
VAR
  res: INTEGER;
BEGIN
  IF x < 0 THEN
    res := -x
  ELSIF x = 0 THEN
    res := 0
  ELSE
    res := x
  END;
  (* Runtime test: input equals output or negation of output, and output is positive or zero *)
  IF NOT (res >= 0 AND (x = res OR x = -res)) THEN
    Out.String("Assertion failed in Abs: input /= output and input /= -output or output < 0"); Out.Ln;
    SYSTEM.Halt(1)
  END;
  Abs := res
END Abs;

BEGIN
  Out.String("Abs(-5) = "); Out.Int(Abs(-5), 0); Out.Ln;
  Out.String("Abs(0)  = "); Out.Int(Abs(0), 0);  Out.Ln;
  Out.String("Abs(7)  = "); Out.Int(Abs(7), 0);  Out.Ln
END AbsModule.

% Reversible factorial relation
% fact(N, F) is true when F = N!
% Works when N is given, when F is given, or when both are variables.

% public entry
fact(N, F) :-
    (  nonvar(N) ->                % N is known: compute F directly
         integer(N), N >= 0,
         fact_from_n(N, F)
    ;  nonvar(F) ->                % F is known: search N by growing factorial
         integer(F), F >= 0,
         fact_from_f(F, N)
    ;  % both variables: enumerate N = 0,1,2,...
         nat(N),
         fact_from_n(N, F)
    ).

% compute factorial when N is known
fact_from_n(0, 1) :- !.
fact_from_n(N, F) :-
    N > 0,
    N1 is N - 1,
    fact_from_n(N1, F1),
    F is F1 * N.

% find N given F by iterative search
% handles F = 0 only if you want to treat 0 specially (0! = 1), so we require F >= 0
fact_from_f(F, N) :-
    % start search from 0 with accumulator 1
    fact_search(0, 1, F, N).

% fact_search(CurrentN, Acc, TargetF, ResultN)
fact_search(N, Acc, F, N) :-
    Acc =:= F, !.
fact_search(N, Acc, F, Res) :-
    Acc < F,
    N1 is N + 1,
    Acc1 is Acc * N1,
    fact_search(N1, Acc1, F, Res).
% If Acc > F the search fails (no integer N with N! = F).
% nat/1 enumerates natural numbers 0,1,2,...
nat(0).
nat(N) :- nat(M), N is M + 1.