Andrzej Salwicki
prof. dr hab. Andrzej Salwicki
E-mail : salwicki .NA. mimuw.edu.pl
Po wielu latach pracy dla Instytutu Informatyki pożegnałem się z uczelnią.
Na razie strona ta jeszcze istnieje. Może komuś się przydadzą informacje tu zawarte.
Poszukuję współpracowników do nowych projektów badawczych. Zapraszam!
Strona ta zostanie wkrótce przeorganizowana wg schematu
Nowe projekty badawcze
Materiały dydaktyczne
Głosy w sprawie Instytutu/Wydziału Informatyki
Nowe projekty badawcze
Polecam (na razie - 23.09.2015) obejrzenie stron
http://lem12.uksw.edu.pl
L1. Nowy język programowania obiektowego - Nowy Loglan
Istnieje kilka powodów dla których warto stworzyć nowy
język programowania obiektowego - nazwijmy go na razie nowy Loglan.
Po pierwsze, po zapoznaniu sie z najbardziej popularnymi obecnie
językami rogramowania obiektowego: Java, C#, C++, ... stwierdzam, że
żaden z nich nie jest doskonały. Każdemu z tych języków można
bez trudu wytknąc wiele wad. ...
Po drugie, podejmując się tego zadania możemy liczyć na opracowania naukowe, publikacje i rozprawy...
Po trzecie, mamy zamiar zbudować język raczej prosty i zrobic to w
nowym stylu. Chcemy podać i gramatykę bezkontekstową i gramatkę
kontekstową dla naszego języka. Ta ostatnia pozwoli precyzyjnie
opisać zbiór programów poprawnie zbudowanych. Dla
programów poprawnie zbudowanych mamy zamiar opisać semantykę
(znaczenie) programów. Chcemy to zrobic trzykrotnie definiując
trzy semantyki: operacyjną, obliczeń formalnych i aksjomatyczną. Widać
stąd, że powstanie wiele problemów badawczych.
Chcemy by nowy język stał się jednym z elementów kolejnego projektu badawczego SpecVer o którym piszemy poniżej.
L1.1 Zadania
L1.1.1 Definicja języka
L1.1.1.1 Gramatyka
Opis gramatyki będzie składał się z trzech części:
opis lexemów,
gramatyka bezkontekstowa,
gramatyka kontekstowa.
Opis lexemów to jest ta część w której zawarte są definicje pojęć takich jka identyfikator, liczba etc.
Gramatyka bezkontekstowa będzie znacznie prostsza ....
Gramatyka kontekstowa ma pozwolić na odpowiedź na pytanie: czy podany kod źródłowy jest poprawnie zbudowany (ang.
well-formed formula). Wykorzystując dwie funkcje bind oraz inh opiszemy
jak poszczególnym fragmentom programu przypisać odpowiedź czy są
czy też nie wff?
l1.1.1.2 Semantyka
Naszym zadaniem jest podanie trzech semantyk:
semantyki operacyjnej,
semantyki obliczeń formalnych,
semantyki aksjomatycznej.
Semantyka operacyjna jest w gruncie rzeczy opisem maszyny wirtualnej i
relacji bezpośredniego następstwa konfiguracji (stanu) tej maszyny.
Semantyka obliczeń formalnych. Tego rodzaju semantyka pozwala wywodzić
wartość wyrażenia w danej konfiguracji (następną konfigurację będącą
efektem wykonania instrukcji).
Tego rodzaju semantykipodawane były wielokrotnie np. Salwicki w 1974, G.Plotkin w 1976, Igarashi & Pierce w 2003.
Semantyka aksjomatyczna: pewną próbę podjęli Hoare i Wirth dla
Pascala. Mirkowska i Salwicki wykazali, że aksjomaty i reguły
dowodzenia logiki algorytmicznej while programów definiuja
semantykę z dokładnością do izomorfizmu.
Kolejne zadania pojawią sie w naturalny sposób. Np. Zbadanie relacji pomiędzy tymi semantykami.
L1.1.2 Realizacja języka
L1.1.1.2.1 Maszyna wirtualna
Pierwszym zadaniem tej grupy jest opis maszyny wirtualnej.
L1.1.2.2 Kompilator
Kompilacja wymagać będzie rozwiązania kilku nowych problemów:
...(uzupełnić)
L1.1.3 Badania eksploatacyjne
Zbadać przydatność nowego języka w dydaktyce.
Zbadać przydatność nowego języka w projekcie SpecVer o którym piszemy poniżej
S1. SpecVer Metodyka tworzenia oprogramowania integrująca zadania specyfikacji, implementacji i weryfikacji modułów programów
Większe
projekty programistyczne w rodzaju oprogramowania dla Biur Podatkowych
we Francji powstają we wspólpracy wielu ludzi. Jedni z nich
opisują wymagania, inni implementują te wymagania w postaci klas i
procedur, jeszcze inni sprawdzają czy zaoferowane implementacje
stanowią poprawne rozwiązanie.
Praca ta wymaga na ogół powtarzania pewnych etapów
ponieważ w miarę realizacji zmieniają się wymagania, a więc naturalne
jest wykonanie nowych implementacji i ponowne weryfikowanie nowych
produktów programistycznych względem kolejnych specyfikacji.
Proponujemy stworzenie odpowiednich narzędzi, a przede wszystkim oferujemy pewną metodologiię prac.
Przemysł już zaczyna dostrzegać konieczność kupowanie nie tylko
programów ale i programów wraz z dowodami ich
poprawności. Jesteśmy w stanie zaoferować coś oryginalnego.
Oczywiście i tu jest źródło wielu problemów naukowych. Praca nad nimi może zaowocować publikacjami, rozprawam...
S1.1 Zadania
S1.1.1 opracować wtyczkę do Eclipse sprawdzającą integralność projektu programistycznego
S1.1.2 opracować nową wersję Mizara dla weryfikowania dowodów poprawności napisanych formalne
S1.1.3 opracować podręcznik tworzenia specyfikacji modułów oprogramowania
...
Materiały dydaktyczne
Logika Algorytmiczna
Języki
Programowania Obiektowego
Metody
Realizacji Języków Programowania
Seminarium: Zagadnienia
Programowania Obiektowego
Zaproszenie do udziału w seminarium magisterskim
Zagadnienia
Programowania Obiektowego
Pytania, problemy, zadania
Na zasadzie "cicer cum caule" (czyli groch
z kapustą) zapisuję tu
1)
pytania na które nie umiem odpowiedzieć,
2) problemy i zadania z których mogą
powstać publikacje, rozprawy, oprogramowanie ...
-
Czy elementarna teoria kolejek jest
rozstrzygalna?
Jeżeli
tak jest to posiada ona programowalny i nieosiągalny model. W
takim modelu z pewnych kolejek można wyjmować elementy bez
końca.
Obecna wersja Loglanu ma wiele lat.
Przydałoby się
-
Ulepszyc VLP Virtual
Loglan Processor tak by współpracowal z nowszymi wersjami
biblioteki Qt,
-
Przenieść
VLP na platformę Windows,
-
Napisać nowy
kompilator.