Strona główna: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 6: Linia 6:
 
Na tych stronach przedstawiamy cztery projekty badawcze: Logika Algorytmiczna(od 1968), Loglan'82(od 1978), SpecVer(2007), Lem(2012).
 
Na tych stronach przedstawiamy cztery projekty badawcze: Logika Algorytmiczna(od 1968), Loglan'82(od 1978), SpecVer(2007), Lem(2012).
 
Dwa pierwsze projekty przyniosły wiele wyników i będą stosowane przez wiele lat.<br />
 
Dwa pierwsze projekty przyniosły wiele wyników i będą stosowane przez wiele lat.<br />
Lothar Collatz miał rację, przeczytaj nasz raport.  
+
Lothar Collatz miał rację, przeczytaj nasz raport [[Media:DowódStopu-20-12-2018.pdf]].  
  
{|  class="wikitable"
+
{|  class="wikitable"edia
 
|-  
 
|-  
 
|♥ Projekt badawczy  ''Logika Algorytmiczna'' zajmuje się odkrywaniem praw [[rachunek programów |rachunku programów]] i znajduje zastosowanie w weryfikacji programów tzn. w dowodzeniu prawdziwości takich własności programów jak [[poprawność]], niezapetlanie się i in. Język logiki algorytmicznej pozwala nie tylko wyrażać własności algorytmów(programów) ale także umożliwia aksjomatyzacje wielu struktur danych. Zarówno tych znanych i niezbędnych w algorytmice np. stosy, drzewa binarnych poszukiwań, kopce, etc. jak i wielu struktur badanych w matematyce. Można uznać, że matematyka zajmuje się badaniem, czy dana formuła <math> \alpha </math> jest prawdziwa w danej strukturze <math> \mathbb{A} </math>. Ale większośc struktur nie daje sie opisać przy pomocy aksjomatów zapisanych w języku pierwszego rzędu! Przyjęcie języka logiki algorytmicznej (krócej, języka algorytmicznego) umożliwia podanie ...<br />
 
|♥ Projekt badawczy  ''Logika Algorytmiczna'' zajmuje się odkrywaniem praw [[rachunek programów |rachunku programów]] i znajduje zastosowanie w weryfikacji programów tzn. w dowodzeniu prawdziwości takich własności programów jak [[poprawność]], niezapetlanie się i in. Język logiki algorytmicznej pozwala nie tylko wyrażać własności algorytmów(programów) ale także umożliwia aksjomatyzacje wielu struktur danych. Zarówno tych znanych i niezbędnych w algorytmice np. stosy, drzewa binarnych poszukiwań, kopce, etc. jak i wielu struktur badanych w matematyce. Można uznać, że matematyka zajmuje się badaniem, czy dana formuła <math> \alpha </math> jest prawdziwa w danej strukturze <math> \mathbb{A} </math>. Ale większośc struktur nie daje sie opisać przy pomocy aksjomatów zapisanych w języku pierwszego rzędu! Przyjęcie języka logiki algorytmicznej (krócej, języka algorytmicznego) umożliwia podanie ...<br />

Wersja z 15:17, 20 gru 2018

22px-English language.svg.png Main page

These pages are under permanent (re)construction.


Na tych stronach przedstawiamy cztery projekty badawcze: Logika Algorytmiczna(od 1968), Loglan'82(od 1978), SpecVer(2007), Lem(2012). Dwa pierwsze projekty przyniosły wiele wyników i będą stosowane przez wiele lat.
Lothar Collatz miał rację, przeczytaj nasz raport Media:DowódStopu-20-12-2018.pdf.

♥ Projekt badawczy Logika Algorytmiczna zajmuje się odkrywaniem praw rachunku programów i znajduje zastosowanie w weryfikacji programów tzn. w dowodzeniu prawdziwości takich własności programów jak poprawność, niezapetlanie się i in. Język logiki algorytmicznej pozwala nie tylko wyrażać własności algorytmów(programów) ale także umożliwia aksjomatyzacje wielu struktur danych. Zarówno tych znanych i niezbędnych w algorytmice np. stosy, drzewa binarnych poszukiwań, kopce, etc. jak i wielu struktur badanych w matematyce. Można uznać, że matematyka zajmuje się badaniem, czy dana formuła [math] \alpha [/math] jest prawdziwa w danej strukturze [math] \mathbb{A} [/math]. Ale większośc struktur nie daje sie opisać przy pomocy aksjomatów zapisanych w języku pierwszego rzędu! Przyjęcie języka logiki algorytmicznej (krócej, języka algorytmicznego) umożliwia podanie ...

Logika Algorytmiczna
ulotka Logika Algorytmiczna

♥ Projekt badawczy Loglan'82 wniósł język programowania obiektowego i rozproszonego o tej samej nazwie. Opublikowanie języka i dystrybucja kompilatora poprzedzone zostały badaniami problemów badawczych. Wymieńmy dla przykładu:

• Rozwiązanie problemu bezpiecznej i efektywnej dealokacji niepotrzebnych obiektów. • Rozwiązanie problemu (statycznej) semantyki jaki pojawia się gdy moduły klas mogą być zagnieżdżane (klasy wewnętrzne) i rozszerzane (dziedziczenie). • Oryginalny protokół współpracy obiektów procesów, jakie programista może alokować w sieci komputerowej (protokół alien call). Język Loglan powstał wiele lat przed językami C++(1986) i Java(1995). Te dwa (oraz inne) języki programowania nie przyswoiły sobie rozwiązań znanych w Loglanie od ponad 30 lat. Zapoznanie się z Loglanem może całkowicie zmienić Twój pogląd na inżynierię oprogramowania. Wykorzystując wiedzę i umiejętności oferowane przez Loglan możesz w znaczący sposób podnieść swoje kwalifikacje.
Loglan'82
ulotka Loglan'82

♥ LEM jest nazwą nowego projektu badawczego.

Celem tego projektu jest zbadanie czy można stworzyć język programowania o pewnych określonych cechach (zob. specyfikacja LEM). Język LEM ma oprzeć się na osiągnięciach projektu Loglan'82 i wykorzystać to co dobre w językach programowania obiektowego nowszych generacji: Java, C++, C#, python etc.
LEM

♥ Projekt SpecVer ma potwierdzić przydatność stosowania praw logiki algorytmicznej w inżynierii oprogramowania. Język LEM może okazać się przydatny w pracach projektu SpecVer.

SpecVer

♥ Biblioteka klas i wiedzy matematycznej przydatnej programistiom.
Wizja przyszłości (jeszcze jeden projekt na lata pracy dla wielu osób).

Zacznijmy od paru pytań: Czy można zawrzeć wiedzę matematyczną w komputerze? Czy można zawrzeć wiedzę informatyczną w komputerze? D. Knuth w latach 70-tych XX wieku miał taka ambicję rozpoczynając tworzenie swojej The Art of Programming. Dziś po prawie 50 latach wiedza informatyczna rozrosła się i nie wyfaje się mozliwe by można ją było zawrzeć w komputerze. A jednak, po pierwsze komputery sa znacznie większe i znacznie szybsze niż kiedyś, po drugie istnieje sieć komputerowa. (Spełniła sie wizja S. Lema z lat 50-tych). Przejdźmy do szkicowania koncepcji: Stworzyć:

  1. magazyn wiedzy z jakiej korzystają twórcy oprogramowania. Znajdą się w nim biblioteki klas i metod i ponadto ...
  2. stworzyć język w jakim twórcy oprogramowania będą zapisywac swoje argumenty na rzecz wygłaszanych (drukowanych, rozpowszechnianych, ...) komunikatów, Język taki powinien być czytelny dla ludzi i na tyle sformalizowany by możliwa była komputerowa analiza przedstawianych dowodów.
  3. narzędzie do weryfikacji poprawności dowodów (Potrzebny będzie proof checker, ale istotnie inny od Mizara i jemu podobnych, ponieważ dowody będą zapisywane w systemie AL bogatszym od rachunku predykatów),
  4. obmyśleć sposób gromadzenia i udostępniania wiedzy. Czy ma to być swego rodzaju wyszukiwarka Google matematyczno-algorytmiczna?