Przykład

Autor: Przemysław Kobylański | Data: 10.07.2016 | Modyfikacja: 22.07.2016

W pracy F.L. Morris, C.B. Jones, An Early Program Proof by Alan Turing przypomniano pierwszy dowód poprawności algorytmu, który Alan Turing zaprezentował na konferencji w czerwcu 1949 roku (Checking a large routine).

Przykład ten opisany jest również w J.C. Filliatre, Deductive Program Verification with Why3. A Tutorial.

Poniżej przedstawiono schemat blokowy algorytmu analizowanego przez Turinga:

Z niektórymi łukami diagramu związano przerywanymi liniami komentarze zawierające warunki jakie są spełnione przez wartości zmiennych, w chwili kiedy następuje przejście danym łukiem.

Jak widać, zakładając, że na początku zmienna N ma wartość dodatnią, otrzymujemy, przy dojściu do końca diagramu, w zmiennej U ma wartość N! (silnia N).

Powyższy algorytm zapisać można w języku Ada w postaci następującej funkcji:

function Comp (N : Natural) return Natural
is
  U : Natural := 1;
  V : Natural;
begin
  for R in 1 .. N - 1 loop
    V := U;
    for S in 1 .. R loop
      U := U + V;
    end loop;
  end loop;
  return U;
end Comp;

Aby udowodnić formalnie, że powyższa funkcja liczy wartość N! należy dołączyć do niej kontrakt wyrażający, że funkcja Comp oblicza silnię.

Zawartość pliku turing.ads:

package Turing with SPARK_Mode is

   function Factorial (N : Natural) return Natural
   is
     (if N = 0 then 1 else N * Factorial (N - 1))
   with
   Ghost,
   Pre => N <= 12,
   Contract_Cases =>
     (
      N = 0 => Factorial'Result = 1,
      others => Factorial'Result = N * Factorial (N - 1)
     );

   function Comp (N : Natural) return Natural
     with
       Pre => N <= 12,
       Post => Comp'Result = Factorial (N);

end Turing;

Warunek Pre w funkcji Comp wyraża założenie, że parametr N będzie miał wartość co najwyżej 12, natomiast warunek Post twierdzi, że wynik zwracany przez funkcję Comp jest równy wartości funkcji Factorial, obliczającej silnię, dla argumentu N.

Funkcja Factorial ma atrybut Ghost, zatem nie jest tłumaczona przez kompilator a jedynie służy do dowodzenia poprawności programu.

Zawartość pliku turing.adb:

package body Turing with SPARK_Mode is

   function Comp (N : Natural) return Natural
   is
      U : Natural := 1;
      V : Natural;
   begin
      for R in 1 .. N - 1 loop
         pragma Loop_Invariant (U = Factorial (R));
         V := U;
         for S in 1 .. R loop
            U := U + V;
            pragma Loop_Invariant (U = V + S * V);
         end loop;
      end loop;
      return U;
   end Comp;

end Turing;

W każdej z dwóch pętli umieszczono niezmienniki pętli, tj. warunki które są spełnione przy każdym z ich przebiegów.


Zawartość pliku main.adb:

with Ada.Text_IO; use Ada.Text_IO;
with Turing; use Turing;

procedure Main is
begin
   Put_Line( Natural'Image (Comp (12)));
end Main;

Zawartość pliku turing.gpr:

project Turing is

   for Main use ("main.adb");

end Turing;