Logika Algorytmiczna: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
(Bibliografia)
(Bibliografia)
Linia 40: Linia 40:
 
== Bibliografia ==
 
== Bibliografia ==
 
# [AlgoLog] [[Media:Algorithmic_Logic.pdf | {{cytuj książkę |odn=tak| nazwisko = Mirkowska| imię = Grażyna | nazwisko2 = Salwicki | imię2 = Andrzej | tytuł = Algorithmic Logic | wydawca = PWN | miejsce = Warszawa | data = 1987 | strony = 345}}]]  
 
# [AlgoLog] [[Media:Algorithmic_Logic.pdf | {{cytuj książkę |odn=tak| nazwisko = Mirkowska| imię = Grażyna | nazwisko2 = Salwicki | imię2 = Andrzej | tytuł = Algorithmic Logic | wydawca = PWN | miejsce = Warszawa | data = 1987 | strony = 345}}]]  
# [LogProg] [[Media:LogikaAlgorytmiczna_1z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }} cz.1
+
# [LogProg] [[Media:LogikaAlgorytmiczna_1z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }}]] cz.1
# [LogProg] [[Media:LogikaAlgorytmiczna_2z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }} cz.1
+
# [LogProg] [[Media:LogikaAlgorytmiczna_2z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }}]] cz.1
 
#[AL4software] [[Media:AlgoLogic.pdf| {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Algorithmic Logic for Software Construction and Verification|wydawca=Dąbrowa Research | miejsce=Dąbrowa Leśna| data=2014|strony=154 }}]]
 
#[AL4software] [[Media:AlgoLogic.pdf| {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Algorithmic Logic for Software Construction and Verification|wydawca=Dąbrowa Research | miejsce=Dąbrowa Leśna| data=2014|strony=154 }}]]
 
   
 
   
 
[[Category:Logika Algorytmiczna]]
 
[[Category:Logika Algorytmiczna]]

Wersja z 09:43, 26 lis 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:  x>0  i  y>0  liczby naturalne *)
   Deklaracje:  typ(x, y, n, m, r, q, max)=N &  typ(n\_mniejsze)=Boolean 
   (* Wynik:  nwd(x,y)   *)
   n:=x; m:=y;
   while n ≠ m do
      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; 
      Stwierdzenie (n<m & m=max(n,m) lub m<n & n=max(n,m))
      q:=0; 
      while r≠max  do  r:= r+1; q:=q+1  od; 
      Stwierdzenie q = |m-n| & (1 ≤ q < max(n,m))& r=max(n,m)
      if n_mniejsze then m:=q else n := q fi 
      Stwierdzenie max(n,m) <  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

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. cz.1
  3. [LogProg] Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów. Warszawa: WNT, 1992, s. 294. cz.1
  4. [AL4software] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic for Software Construction and Verification. Dąbrowa Leśna: Dąbrowa Research, 2014, s. 154.