Strona główna: Różnice pomiędzy wersjami
Z Lem
| Linia 23: | Linia 23: | ||
|♥ 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.<br /> | |♥ 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.<br /> | ||
→ '''[[SpecVer]]''' | → '''[[SpecVer]]''' | ||
| − | | | + | |- |
| − | Wizja przyszłości(jeszcze jeden projekt na lata dla wielu osób).<br /> | + | |♥ Wizja przyszłości(jeszcze jeden projekt na lata dla wielu osób).<br /> |
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: | 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: | ||
| Linia 33: | Linia 33: | ||
# 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), | # 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), | ||
# obmyśleć sposób gromadzenia i udostępniania wiedzy. Czy ma to być swego rodzaju wyszukiwarka Google matematyczno-algorytmiczna? | # obmyśleć sposób gromadzenia i udostępniania wiedzy. Czy ma to być swego rodzaju wyszukiwarka Google matematyczno-algorytmiczna? | ||
| + | |} | ||
Wersja z 10:19, 7 lip 2018
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.
| ♥ Projekt 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 ... |
♥ Odkryj język programowania obiektowego i rozproszonego Loglan'82. Projekt Loglan'82 zaowocował sformułowaniem języka programowania obiektowego na wiele lat przed powstaniem języków C++ i Java. Te dwa (oraz inne) języki programowania nie przyswoiły sobie rozwiązań znanych w Loglanie od ponad 30 lat. I nie zanosi się na to, by w najbliższej przyszłości, ta sytuacja uległa zmianie . Wykorzystaj swoją szansę. 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 i zacząć lepiej zarabiać. |
| ♥ 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. |
♥ 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 |
| ♥ Wizja przyszłości(jeszcze jeden projekt na lata 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ć:
|
