Correctness of Algorithms

Correctness of algorithms: preconditions, postconditions, loop invariants, weakest precondition, structural rules, total correctness and partial correctness, halting problem.

Program state, condition (assertion), operations of logic (sentential calculus). Precondition and postcondition. External specification. Total correctness theorem. Weakest precondition method. Proof by structure of an algorithm. Deduction rules - empty program, superposition, assignment, if-clause. Partial correctness, halting problem. Loop invariant. While-clause.
Examples of proofs.

---

Defineerida algoritmi olek (näit. kõigi algoritmis esinevate muutujate hetkeväärtuste korteež, peaks lubama ka väärtust "väärtustamata").

Tingimus - väide oleku kohta (tõene/väär).

Tingimuste kombineerimiseks loogikatehted: eitus (!), disjunktsioon (||), konjunktsioon (&&), implikatsioon (=>), ...

Eeltingimus - väide oleku kohta enne algoritmi täitmise algust.

Järeltingimus - väide oleku kohta peale algoritmi täitmise lõppu.

Paar (eeltingimus, järeltingimus) on antud algoritmi (välimine) spetsifikatsioon.

Vt. pilt

Täieliku korrektsuse teoreem: Kui algoritmi täitmist alustatakse olekus, mis rahuldab eeltingimust, siis algoritmi täitmine lõpeb lõpliku aja jooksul nii, et saavutatud olek rahuldab järeltingimust.

Algoritm on (täielikult) korrektne etteantud spetsifikatsiooni suhtes, kui saab tõestada (täieliku) korrektsuse teoreemi.

Korrektsuse tõestamiseks spetsifikatsiooni (P, Q) suhtes nõrgima eeltingimuse Wp abil konstrueeritakse antud järeltingimusest Q ja algoritmist  lähtudes  niisugune  eeltingimus Wp,  mis on järeldatav  (igast)  antud eeltingimusest P  -  seda nim. nõrgimaks eeltingimuseks:  P => Wp &&  paari (Wp, Q) jaoks kehtib täieliku korrektsuse teoreem.

Nõrgima eeltingimuse leidmiseks kasutatakse algoritmi struktuuri - iga konstruktsiooni jaoks algoritmis on teatud tuletusreegel.

Tühi algoritm: olek ei muutu, nõrgimaks eeltingimuseks on järeltingimus ise: Wp = Q

Superpositsioon (kahe algoritmi järjestikune rakendamine):  kui esimese algoritmi järeltingimus on teise algoritmi nõrgimaks eeltingimuseks, siis esimese algoritmi nõrgim eeltingimus on superpositsiooni nõrgimaks eeltingimuseks.

Omistamine x := e : nõrgim eeltingimus saadakse, kui omistamislause järeltingimuses Q asendada kõik muutuja x esinemised avaldisega e (ning eeldada, et e arvutamine toimub kõrvalefektideta).

if-lause: konstruktsiooni  if (t) A1 else A2; nõrgim eeltingimus konstrueeritakse algoritmide A1 ja A2 nõrgimatest eeltingimustest Wp1 ja Wp2 eeldusel, et mõlemal harul on sama lõpptingimus Q ning tingimuse t kontrollimine on kõrvalefektideta:
  t && Wp1  ||    !t  && Wp2

Tsüklite korral toome sisse veel osalise korrektsuse mõiste: kui algoritmi täitmist alustatakse olekus, mis rahuldab eeltingimust, siis algoritmi täitmine lõpeb nii, et saavutatud olek rahuldab järeltingimust või ei lõpe täitmine üldse.

Lõplikkuse teoreem: kui algoritmi täitmist alustatakse olekus, mis rahuldab eeltingimust, siis algoritm lõpetab töö lõpliku hulga operatsioonide täitmise järel.

Täielik korrektsus = osaline korrektsus + lõplikkus

Tsükli invariant: tingimus, mis kehtib enne iga tsüklisammu algust.

while-tsükkel:  konstruktsiooni while(t) A; nõrgima eeltingimuse konstrueerimiseks kasutatakse tsükliinvarianti R  (eeldame taas, et jätkamistingimuse t kontrollimine on kõrvalefektideta):
invariantsus: tsükli samm A on osaliselt korrektne (t && R , R) suhtes.
sihipärasus: !t && R  => Q, kus Q on tsükli järeltingimus.
invariandi kehtivus algoleku jaoks: P => R, kus P on tsükli eeltingimus.
Tsükli täieliku korrektsuse tõestamiseks tuleb lisaks tõestada lõplikkuse teoreem.

Selline programmeerimiskeel võimaldab väljendada kõiki Turingi mõttes arvutatavaid funktsioone.


Näide: Kasutame FPP programmitõestamise tarkvara aadressilt http://psc.informatik.uni-jena.de/fpp/fpp-main.htm

FPP (Frege Program Prover) University of Jena, Germany

--!pre       : (x + y = m);
 
--> wp       :     (x >= 1 + y AND y <= x AND x + y = m)
-->            OR (x < 1 + y AND x <= y AND x + y = m)
--> vc       :      (x + y = m)
-->            ==>     (x >= 1 + y AND y <= x AND x + y = m)
-->                 OR (x < 1 + y AND x <= y AND x + y = m)
--> Result: proved

IF x > y THEN 
   a := x;
   x := y;
   y := a;
END IF;

--!post      : (x <= y AND x + y = m);

--> wp       : (x >= y AND 2*x = 0 OR x < y AND -2 + 2*y = 0)

IF x >= y THEN 
   y := x;
ELSE
   x := y - 2;
END IF;

--!post: (x + y = 0);

--!pre       : (x <= 0 AND y = 1 OR x = 0 AND y <= 0);
 
--> wp       : (x >= y AND 2*x = 0 OR x < y AND -2 + 2*y = 0)
--> vc       :      (x <= 0 AND y = 1 OR x = 0 AND y <= 0)
-->            ==> (x >= y AND 2*x = 0 OR x < y AND -2 + 2*y = 0)
--> Result: proved

IF x >= y THEN 
   y := x;
ELSE
   x := y - 2;
END IF;

--!post: (x + y = 0);

s := 0;

--!pre       : (s = 0 AND n >= 1);
--!post      : (s = n*(1 + n)/2);
--!inv       : (s = i*(1 + i)/2);
 
-->functionality ---------------------------
-->func      : (initial AND induction AND final AND null loop)
-->initial   :(1 <= n AND s = 0 AND n >= 1 => s = 0)
--> Result    : proved
-->induction :(1 <= n AND s = (-1 + i)*i/2 => i + s = i*(1 + i)/2)
--> Result    : proved
-->final     :(1 <= n AND s = n*(1 + n)/2 => s = n*(1 + n)/2)
--> Result    : proved
-->null loop :(1 >= 1 + n AND s = 0 AND n >= 1 => s = n*(1 + n)/2)
--> Result    : proved

FOR i IN 1 .. n  LOOP
   s := s + i;
END LOOP;

--!pre       : (i >= 1 AND j >= 1 AND i = k1 AND j = k2);
--!post      : (i = j AND i = GGT(k1,k2));
--!inv       : (i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2));
--!term      : (j + i);

-->functionality ---------------------------
-->initial   :     (i >= 1 AND j >= 1 AND i = k1 AND j = k2)
-->            ==> (i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2))
--> Result    : proved
-->induction :     (i /= j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2))
-->            ==>          (i >= 1 + j)
-->                     AND (-j + i >= 1)
-->                     AND (j >= 1)
-->                     AND (GGT(i,j) = GGT(k1,k2))
-->                 OR (i < 1 + j AND i >= 1 AND j - i >= 1 AND GGT(i,j) = GGT(k1,k2))
--> Result    : proved
-->final     :     (i = j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2))
-->            ==> (i = j AND i = GGT(k1,k2))
--> Result    : proved
-->termination ---------------------------
-->initial   :(i /= j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2) => j + i >= 1)
--> Result    : proved
-->induction :     (i /= j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2))
-->            ==> (i >= 1 + j AND j + i >= 1 + i OR i < 1 + j AND j + i >= 1 + j)
--> Result    : proved

WHILE i /= j LOOP
   IF i > j THEN 
      i := i - j;
   ELSE
      j := j - i;
   END IF;
END LOOP;

--!pre       : (n >= 3);
 
--> wp       : (2 <= n)
--> vc       : (n >= 3 => 2 <= n)
--> Result: proved

f0 := 0;
f1 := 1;
i := 2;
fi := f0 + f1;

--!pre       :      (f0 + f1 = fi)
-->            AND (i <= n)
-->            AND (i = 2)
-->            AND (2**i/4 >= 1 + f0)
-->            AND (2**i/2 >= 1 + f1);
--!post      : (2**n >= 1 + fi);
--!inv       : (f0 + f1 = fi AND 2**i/4 >= 1 + f0 AND 2**i/2 >= 1 + f1);

-->functionality ---------------------------
-->func      : (initial AND induction AND final AND null loop)
-->initial   :          (3 <= n)
-->                 AND (f0 + f1 = fi)
-->                 AND (i <= n)
-->                 AND (i = 2)
-->                 AND (2**i/4 >= 1 + f0)
-->                 AND (2**i/2 >= 1 + f1)
-->            ==> (f0 + f1 = fi AND 1 >= 1 + f0 AND 2 >= 1 + f1)
--> Result    : proved
-->induction :     (3 <= n AND f0 + f1 = fi AND 2**i/8 >= 1 + f0 AND 2**i/4 >= 1 + f1)
-->            ==> (2**i/4 >= 1 + f1 AND 2**i/2 >= 1 + fi)
--> Result    : proved
-->final     :     (3 <= n AND f0 + f1 = fi AND 2**n/4 >= 1 + f0 AND 2**n/2 >= 1 + f1)
-->            ==> (2**n >= 1 + fi)
--> Result    : proved
-->null loop :          (3 >= 1 + n)
-->                 AND (f0 + f1 = fi)
-->                 AND (i <= n)
-->                 AND (i = 2)
-->                 AND (2**i/4 >= 1 + f0)
-->                 AND (2**i/2 >= 1 + f1)
-->            ==> (2**n >= 1 + fi)
--> Result    : proved

FOR i IN 3 .. n  LOOP
   f0 := f1;
   f1 := fi;
   fi := f0 + f1;
END LOOP;

Jaanus Pöial