The Ada Program: binomial.adb
1
2
3
4
5
6
7
8
9
10
11 function Binomial (N, R : Natural) return Positive is
12
13 function Factorial (N : Natural) return Positive is
14 F : Positive := 1;
15 begin
16 for I in 2 .. N loop
17 F := F*I;
18 end loop;
19 return F;
20 end Factorial;
21
22 B : Positive := 1;
23
24 begin
25
26 pragma Assert (R>=0, "R negative");
27 pragma Assert (N>=R, "N not greater than R");
28
29 for I in R+1 .. N loop
30 B := B*I;
31 end loop;
32
33 pragma Assert (B=Factorial(N)/Factorial(R), "B not correct");
34
35 for I in 2 .. N-R loop
36 pragma Assert (B mod I = 0, "B mod I /= 0");
37 B := B/I;
38 end loop;
39
40 pragma Assert (B=Factorial(N)/(Factorial(R)*Factorial(N-R)),
41 "postcondition does not hold!");
42
43 return B;
44
45 end Binomial;