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


Głos w dyskusji na temat powiększenia Instytutu Informatyki

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 ...
 

  1. 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ę

  1. Ulepszyc VLP Virtual Loglan Processor tak by współpracowal z nowszymi wersjami biblioteki Qt,

  2. Przenieść VLP na platformę Windows,

  3. Napisać nowy kompilator.