First Factorial

with Ada.Text_IO; use Ada.Text_IO;

with Ada.Integer_Text_IO; use Ada.Integer_Text_IO;

procedure test is

    X: Natural := 4;

    Y: Natural := 5;

    function factorial(n: Integer) return Integer

        with Pre => (n >= 0)  

    is

        result : Integer := 1;

    begin

        for index in 1..n loop

            result := result*index;

        end loop;

        return result;

    end factorial;

begin

    Put(factorial(Y));

    Put(factorial(X));

end test;