Hope (1980)

dec fact : num -> num;
--- fact 0 <= 1;
--- fact n <= n*fact(n-1);