Niezawodne programowanie

Ciąg Fibonacciego

15/12/15 19:18
referral_campaign_blog

fibonacci.ads



pragma SPARK_Mode(on);

function Fibonacci (N : Natural) return Natural
  with
    Pre => N <= 46,
    Contract_Cases =>
      (N = 0  => Fibonacci'Result = 0,
       N = 1  => Fibonacci'Result = 1,
       others => Fibonacci'Result = Fibonacci(N - 1) + Fibonacci(N - 2));



fibonacci.adb



 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
pragma SPARK_Mode(on);

function Fibonacci (N: Natural) return Natural
is
   X : Natural := 0;
   Y : Natural := 1;
   Z : Natural := 1;
begin
   case N is
      when 0 =>
         return 0;
      when 1 =>
         return 1;
      when others =>
         for I in 2 .. N loop
            Z := X + Y;
            pragma Loop_Invariant (X = Fibonacci(I-2)
                                   and Y = Fibonacci(I-1)
                                   and Z = Fibonacci(I));
            X := Y;
            Y := Z;
         end loop;
         return Z;
   end case;
end Fibonacci;



github repozytorium

Tags: