Logika Algorytmiczna: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 1: Linia 1:
 
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''.  
 
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 omożliwią analiże 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
+
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
 +
  q:=n;  r:=m;
 +
  '''while'' r < m '''do'''
 +
      q:=q+1:
 +
      r:=r-n
 +
  '''od'''
 +
Co robi ten program? Czy to jest pytanie dobrze postawione?
 +
Czy obliczenie tego programu jest skończone dla każdych danych n i m?
 +
 
 +
 
 +
 
 
   
 
   
 
== Podręczniki ==   
 
== Podręczniki ==   

Wersja z 18:32, 28 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

  q:=n;  r:=m;
  while r < m do'
     q:=q+1:
     r:=r-n
  od

Co robi ten program? Czy to jest pytanie dobrze postawione? Czy obliczenie tego programu jest skończone dla każdych danych n i m?



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.
  3. [AL4software]Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic for Software Construction and Verification. Dąbrowa Leśna: Dąbrowa Research, 2014, s. 154.