Logika Algorytmiczna: Różnice pomiędzy wersjami

Wersja z 06:17, 29 lip 2014

Logika algorytmiczna jest rachunkiem logicznym. Język logiki algorytmicznej zawiera programy i formuły algorytmiczne. Formuły tworzą algebrę z działaniami: konkatenacji, alternatywy, negacji i implikacji oraz z działaniami nieskończonymi tj kwantyfikatorami, ponadto programy są modalnościami. Programy też tworzą algebrę: działaniami tej algebry są iteracja, rozgałęzienie i złożenie programów. Mamy więc do czynienia ze splotem dwu algebr. Możemy go nazwać rachunkiem programów. Zadaniem logiki algorytmicznej jest poszukiwanie praw rachunku programów.

Celem jest zebranie praw i reguł wnioskowania, które umożliwią analizę algorytmów i wydawanie opinii o ich własnościach semantycznych, bez wykonywania obliczeń, na podstawie samego tekstu algorytmu i aksjomatów struktury danych w jakiej dany program ma byc interpretowany.

Przykład Rozpatrzmy prosty program

   (* Dane: [math]x\gt0[/math] i [math]y\gt0[/math] liczby naturalne *)
   [math]\color{blue}\mathbf{Deklaracje: }\ typ(x, y, n, m, r, q, max)=\mathbb{N}\ \land\  typ(n\_mniejsze)=Boolean [/math]

(* Wynik: [math]nwd(x,y) [/math] *) n:=x; m:=y; while n ≠ m do

   \color{red}\mathbf{Oznaczenie}\ niech\ l=max(n,m)
   r:=0; 
   while r ≠n and r ≠m 
   do
       r:=r+1 
   od; 
   if r=n then n_miejsze:=true; max:=m else n_mniejsze:=false; max:=n fi; 
   \color{blue}\mathbf{Stwierdzenie}\ (n<m \wedge m=max(n,m) \vee m<n \wedge n=max(n,m))
   q:=0; 
   while r≠max 
   do
       r:= r+1; q:=q+1 
   od; 
   \color{blue}\mathbf{Stwierdzenie}\ q = |m-n| \land (1 \leq q < max(n,m))\land r=max(n,m)
   if n_mniejsze then m:=q else n := q fi 
   \color{blue}\mathbf{Stwierdzenie}\ max(n,m) < \color{red}l

od ( wynik = n)

Co robi ten program? Czy to jest pytanie dobrze postawione? Czy obliczenie tego programu jest skończone dla każdych danych n i m? Czym są te dane? Jakie znaczenie mają operacje - i + oraz stała 1? Jakie znaczenie ma predykat <?

Podręczniki

• Grażyna Mirkowska, Andrzej Salwicki, Algorithmic Logic -- monografia -- większy nacisk położono na badania systemu AL
• Grażyna Mirkowska, Andrzej Salwicki, Logika Algorytmiczna dla programistów cz.1
• Grażyna Mirkowska, Andrzej Salwicki, Logika Algorytmiczna dla programistów cz.2
• Algorithmic Logic for Software Construction and Verification

Program logiki algorytmicznej

Zadaniem logiki algorytmicznej jest dostarczenie narzędzi do analizowania semantycznych własności programów takich jak: własność stopu, poprawność programu, etc. Znaczeniem programu [math]P[/math] jest funkcja ze zbioru [math]W[/math] wartościowań zmiennych w ten sam zbiór. Zazwyczaj funkcję tę określa się przy pomocy pojęcia obliczenia programu.

Bibliografia

1. [AlgoLog] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic. Warszawa: PWN, 1987, s. 345.
2. [LogProg] Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów. Warszawa: WNT, 1992, s. 294.
3. [AL4software]Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic for Software Construction and Verification. Dąbrowa Leśna: Dąbrowa Research, 2014, s. 154.