Tematyka projektu

Proponowany przez nas projekt dotyczy kluczowych zagadnień programistycznych: specyfikowania, konstruowania i weryfikowania.

Każde z trzech wyróżnionych wyżej pojęć wyjaśnić można poprzez odwołanie się do relacji binarnej sat pomiędzy programami z jednej, a specyfikacjami z drugiej strony. Relacja ta formalizuje kluczowe pojęcie: poprawności programów względem specyfikacji, albo, inaczej rzecz ujmując, pojęcie spełniania specyfikacji przez program.

• Zagadnienie weryfikowania oprogramowania pojawia się wówczas, gdy zarówno program p jak i specyfikacja A są dane. Pozostaje jedynie sprawdzić, czy ów program spełnia daną specyfikację. Zagadnienie weryfikowania formalizujemy pisząc

  p sat A

  weryfikowanie

  gdzie zmienna p przebiega składniową klasę programów, a zmienna A przebiega składniową klasę specyfikacji.

• Zagadnienie specyfikowania odnosi się do sytuacji w której program p jest dany z góry, a zadanie polega na znalezieniu specyfikacji którą p spełnia. Do oznaczenia tej nieznanej specyfikacji używać będziemy metazmiennej ?A. Zagadnienie specyfikowania można wówczas sformalizować w następujący sposób.

  p sat ?A

  specyfikowanie

  Metazmienne, zwane też zmiennymi schematycznymi są wygodnym sposobem zaznaczania dziury, którą wypełnić można bardziej dookreślonymi elementami z odpowiedniej klasy składniowej --- w naszym przypadku bardziej dookreślonymi specyfikacjami (Precyzyjniej, chodzi o pre-porządek, w którym metazmienne są najmniej dookreślonymi termami, zaś jeden term jest bardziej dookreślony od drugiego, gdy można uzyskać go przez zastąpienie w tym drugim pewnych metazmiennych jakimiś termami).

• Zagadnienie konstruowania jest dualne do zagadnienia specyfikowania. Mamy z nim do czynienia wówczas, gdy dana jest specyfikacja A, a problem polega na znalezieniu spełniającego ją programu. Formalnie, zagadnienie konstruowania ma więc następującą postać

  ?p sat A

  konstruowanie

• Zagadnienia mieszane. Uogólniając, rozważać można zagadnienia, w których zarówno program jak i specyfikacja są częściowo niedookreślone. Z tego punktu widzenia trzy pierwsze typy zagadnień są szczególnymi przypadkami zagadnienia mieszanego, w których ograniczono możliwość umieszczania metazmiennych po jednej ze stron, a w przypadku zagadnienia weryfikowania, po obu stronach. Przykładem krańcowym zagadnienia typu mieszanego, mało interesującym z pragmatycznego punktu widzenia, jest programowanie dowolne, to jest zagadnienie postaci ?p sat ?A. Są jednak i bardziej interesujące przykłady nie podpadające pod schemat jednego z trzech podstawowych. Można na przykład rozważać zagadnienie typu konstruowania, w którym pewne składowe specyfikacji (wyrażenia indywiduowe) pozostawia się niedookreślone by ułatwić pracę programiście, patrz bb96-opis.

Zagadnienie konstruowania programów jest kluczowym zagadnieniem programistycznym. Ponieważ jest też najtrudniejszym zagadnieniem, w praktyce stosuje się najrozmaitsze, często nieformalne techniki przyspieszające proces konstruowania, zadowalając się weryfikowaniem i/lub testowaniem powstałego w ten sposób produktu.

Można by sądzić, że trzy wyróżnione przez nas typy zagadnień są od siebie w zasadzie niezależne. W praktyce okazuje się, że przy naturalnych założeniach są one ze sobą ściśle związane.

Zwykle specyfikacje są formułami pewnej logiki specyfikacji. A wówczas, rozwiązując na przykład zagadnienie typu weryfikowania: psat A, możemy być zainteresowani zastąpieniem specyfikacji A przez inną, równoważną jej specyfikację B mając nadzieję, że problem p sat B będzie łatwiejszy do rozwiązania. Proces postępowania w tym przypadku polegać może na zastąpieniu problemu p sat A dwoma problemami p sat ?A oraz ?A ≡ A. Można teraz rozwiązać problem równoważności ?A ≡ A wstawiając zamiast ?A specyfikację B i mimochodem redukując pozostały podproblem do p sat B. Ale można też wybrać inną drogę postępowania. Można mianowicie rozwiązać podproblem specyfikowania p sat ?A zastępując ?A specyfikacją C, a następnie starać się dowieść równoważność C ≡ A.

Zagadnienia specyfikowania i konstruowania komplikuje się częstokroć, żądając by poszukiwane specyfikacje i programy spełniały jakieś dodatkowe kryteria.

W przypadku specyfikowania może to być oczekiwanie, by znaleźć najbardziej reprezentatywną spośród specyfikacji spełnianych przez dany program i/lub by miała ona pożądaną postać składniową.

W przypadku konstruowania można żądać, by poszukiwany program miał możliwie największą dziedzinę stosowalności, albo by miał pożądaną postać składniową, bądź też by miał niewielką złożoność obliczeniową. Większość z tych kryteriów wykracza poza przedstawiony wyżej schemat.

Podstawowe ograniczenie obszaru naszych zainteresowań dotyczy przyjęcia kryterium poprawności oprogramowania jako podstawowego wyróżnika jakości oprogramowania. W ten sposób ograniczamy obszar potencjalnych zastosowań jedynie do tych dziedzin, w których poprawność działania jest sprawą o podstawowym znaczeniu. Oznacza to również, że jako zagadnienia drugorzędne traktujemy dodatkowe wymagania dotyczące jakości poszukiwanych programów lub specyfikacji.

Ewentualne zastrzeżenie można odpierać na dwa sposoby.

Po pierwsze, ograniczenie to nie dotyczy dziedzin o istotnym znaczeniu, takich jak programowanie na poziomie hardware'u, programowanie protokołów komunikacyjnych, programowanie systemów zespolonych (ang.: embedded systems), czy wreszcie systemów o wysokim poziomie bezpieczeństwa (ang.: safety critical systems), na przykład systemów sterowania elektrowniami.

Po drugie, uważamy iż zagadnienie poprawności oprogramowania należy do grupy problemów fundamentalnych, czyli tych z którymi programiści będą musieli zawsze się borykać. Problemy natury technologicznej będą odchodzić w niepamięć dzięki nowym technologiom --- tak jak problem oprogramowania graficznego interfejsu użytkownika odchodzi z wolna w zapomnienie dzięki technologii programowania graficznego w językach IV-generacji.

Liczymy również, że pewne zagadnienia optymalnościowe można będzie przedstawić i sformalizować w ramach tworzonego przez nas formalizmu jako problemy wyboru strategii dedukcyjnej.

Drugim, istotnym ograniczeniem jest przyjęcie założenia, iż w zagadnieniach typu konstruowania oprogramowania programista ma do czynienia z problemem precyzyjnie określonym i zapisanym w formie specyfikacji. Tym samym pomijamy problemy związane ze zbieraniem i analizą danych prowadzącymi do powstania specyfikacji. Wychodzimy tu z założenia, że sprawy te dają się oddzielić od interesujących nas problemów. Ponadto, wydaje się, że do ich rozwiązywania niezbędne byłoby interdyscyplinarne podejście charakterystyczne dla problemów powstających na styku człowiek-komputer.

Poważniejszą konsekwencją powyższego założenia jest statyczność rozpatrywanej przez nas sytuacji. W praktyce bowiem ulega zmianie środowisko w którym działa oprogramowanie, a tym samym modyfikowana być musi wyjściowa specyfikacja. Należałoby dążyć do tego, by zmieniając specyfikację można było w kontrolowany i ograniczony sposób zmieniać i program. Badania w tym kierunku pozostawiamy tymczasowo poza obszarem zainteresowań obecnego projektu.

Przesłanki i cele projektu

Proponowany przez nas projekt dotyczy opracowania praktycznych metodologii wspierających działania programistów w zakresie specyfikacji, konstrukcji i weryfikacji oprogramowania.

Punktem wyjścia projektu jest stwierdzenie, że działalność programistyczną opartą o kryterium poprawności w sposób naturalny opisuje się jako działaność o charakterze dedukcyjnym. Przyjęcie tej przesłanki sytuuje proponowany projekt w dziedzinie logiki stosowanej. Zamierzamy więc rozpatrywać zagadnienia programistyczne w takim formalizmie logicznym, który dobrze opisywałby zjawiska i mechanizmy występujące w procesie dedukcji.

W tym miejscu należy wyjaśnić, dlaczego uważamy tradycyjne podejście oparte o tak zwane logiki programistyczne za nieadekwatne. Otóż na ogół logiki programistyczne, takie jak logika Hoare'a, (hoa69), jak i modalne logiki takie jak logika algorytmiczna (BKMRS77, MS92) czy logika dynamiczna (Har79), mają ograniczoną stosowalność --- nadają się do wywodzenia twierdzeń, lecz nie nadają się do dowodzenia własności zrelatywizowanych obecnością założeń.

Otóż zwykła logika posiada wiele metod prezentacji. Prezentacja w stylu Hilberta koncentruje się na poszukiwaniu faktów prawdziwych, czyli twierdzeń. Hilbertowska prezentacja oferuje minimalną liczbę reguł wnioskowania i wiele aksjomatów charakteryzujących spójniki logiczne. Gentzenowskie prezentacje z kolei, zwłaszcza rachunek sekwentów, kładą nacisk na formalizację relacji konsekwencji logicznej, czyli faktów zrelatywizowanych prawdziwością przyjętych założeń.

Sprawą kluczową jest, że te różne prezentacje są wzajemnie równoważne. W prezentacji hilbertowskiej dowody mają postać ciągów, w których kolejne elementy są bądź instancjami aksjomatów, bądź założeniami, albo też powstały w wyniku zastosowania jakiejś reguły do wcześniejszych elementów ciągu. Relację konsekwencji |- definiuje się poprzez odwołanie się do pojęcia dowodu: Γ|-ψ jeśli istnieje dowód, którego ostatnim elementem jest ψ, oraz w którym jedynymi założeniami są elementy ciągu Γ. Powyższy, wyglądający naturalnie sposób usekwentowienia logiki w przypadku każdej z wyżej wymienionych logik zawodzi (nie znaczy to, że próba budowy rachunku sekwentów dla tych logik skazane jest na niepowodzenie. W MS92 znaleźć można całkiem naturalny rachunek sekwentów dla logiki algorytmicznej).

Poniżej przedstawione dwa ciągi demonstrują to na przykładzie logiki algorytmicznej, choć można je zaadoptować do obu pozostałych. W każdym przypadku źródło problemu jest takie samo --- każda z logik jest rozszerzeniem klasycznej logiki o nową klasę formuł zbudowanych ze zwykłych formuł i programów. W przypadku logiki algorytmicznej owe nowe formuły mają postać πψ, gdzie π jest programem, a ψ formułą logiki pierwszego rzędu. Upraszczając nieco można powiedzieć, że πψ jest prawdziwe, jeśli każde obliczenie π jest skończone, a jego wynik spełnia ψ.

	Dowód poprawny	Dowód wątpliwy	Uzasadnienie
1	x^2>=0	x=0	twierdzenie/założenie
2	x^2>=0	x=0
	==> (true ==> x^2>=0)	==> (true ==> x=0)	tautologia
3	true ==> x^2>=0	true ==> x=0	z 1 i 2, Modus Ponens
4	(x:=1)true	(x:=1)true	reguła R2 z MS92, str. 94
	==> (x:=1)x^2>=0	==> (x:=1)x=0	zastosowana do 3
5	(x:=1)true	(x:=1)true	aksjomat Ax18 z MS92, str. 94
6	(x:=1)x^2>=0	(x:=1)x=0	z 4 i 5, Modus Ponens

W pierwszym przypadku dowodzimy twierdzenie |- (x:=1)x^2>=0, a po drodze twierdzeń: |- x^2>=0, |- true, |- true ==> x^2>=0, |- (x:=1)true, itd.

W drugim przypadku dowodzimy konsekwencji x=0|-(x:=1)x=0, a mimochodem: x=0|- x=0, x=0|- true, x=0|- true ==> x=0, x=0|- (x:=1)true, itp.

O ile w pierwszym przypadku nie ma problemów, to drugi budzi wątpliwości. Źródłem problemów jest danie możliwości użycia założeń dotyczącego własności indywidum ukrywającego się pod zmienna x, w trakcie wnioskowania o skutkach programu, który wartość x może zmienić. Próby naprawienia tej sytuacji, np.: poprzez dodanie warunków ubocznych o nieinterferencji założeń z programami do reguł logiki Hoare'a są raczej zniechęcające. Dotychczasowe niepowodzenia zdają się sugerować, iż logik programistycznych nie należy budować jako rozszerzeń logiki klasycznej. Problem wskazany powyżej jest szczególnie kłopotliwy przy próbach zakodowania którejś z tych logik w komputerowych systemach kodowania logik i dowodzenia twierdzeń. Systemy takie z reguły wspierają wnioskowanie w stylu naturalnej dedukcji, patrz hm94.

Naszym celem jest konstrukcja formalizmu logicznego, który będzie rozgraniczał świat własności programów od świata własności indywiduów. Uważamy, że takim dobrze rokującym formalizmem jest formalizm etykietowanych systemów dedukcyjnych. Zamierzamy wykorzystać ten formalizm do prezentacji zagadnień programistycznych i do ich studiowania. Planujemy też wykorzystanie gotowych systemów komputerowych służących do kodowania logik i automatyzacji dowodzenia w zakodowanych logikach, do przeprowadzenia eksperymentów weryfikujących prace teoretyczne. W szczególności zamierzamy kontynuować nasze eksperymenty z systemem Isabelle i podobnymi systemami.

Już w tej chwili bliscy jesteśmy sytuacji, w której generyczny system kodowania logik i dowodzenia twierdzeń służy jako środowisko programistyczne, to znaczy przestrzeń w której powstają, są specyfikowane i weryfikowane programy. Znaczną część wysiłku poświęcić pragniemy na wykazanie, że środowisko to może już teraz służyć produkcji oprogramowania na małą skalę. W tym kierunku zmierzają prowadzone przez nas zajęcia z wybraną grupą studentów Instytutu Matematyki Uniwersytetu Gdańskiego.

W ramach prowadzonego obecnie seminarium magisterskiego studenci będą eksperymentować w wykorzystaniu zakodowanych przez nas logiki. Istotą tych eksperymentów będzie rozwiązywanie zagadnień programistycznych poprzez wykonywanie czynności związanych z krokami dedukcyjnymi występującymi w trakcie produkcji oprogramowania.

Formalizm Etykietowanych Systemów Dedukcyjnych (ang.: Labelled Deductive Systems) wprowadził Dov Gabbay, patrz monografia gab94, jako wygodną formalizację pojęcia ,,logiki''. Problem bowiem w tym, że w rozmaitych sytuacjach spotykanych w rozmaitych dziedzinach filozofii, matematyki, sztucznej inteligencji i informatyki istotne są różnorodne, często odmienne aspekty ,,logik''. Prace Gabbay'a demonstrują jak owe różne aspekty można opisywać przy pomocy etykietowanych systemów dedukcyjnych.

W dużym uproszczeniu powiedzieć można, iż podstawą formalizmu etykietowanych systemów dedukcyjnych jest przyjęcie następujących założeń.

• Elementy deklaratywne. Obiektem studiów są elementy deklaratywne, czyli pary postaci: λ:A, gdzie λ jest etykietą, a A formułą.

  Klasyczny, czysto logiczny przykład otrzymamy przyjmując, iż etykietami są dowody, zaś λ:A znaczy iż λ jest dowodem A. Inny przykład: w semantyce Kripke'go logik modalnych można przyjąć iż etykietami są światy, a element deklaratywny opisuje sytuację w której formuła A jest prawdziwa w świecie λ. W zastosowaniach informatycznych, zwłaszcza tych w których my jesteśmy zainteresowani, rolę światów pełnią programy.

  Inny przykład informatyczny, z dziedziny systemów reprezentacji wiedzy, otrzymamy biorąc jako etykiety liczby rzeczywiste opisujące stopień prawdopodobieństwa prawdziwości formuły A. Z kolei w dziedzinie dedukcyjnych baz danych role etykiet pełnić będą obiekty, zaś formułami będą atrybuty tychże obiektów.

• Bazy danych. Elementy deklaratywne łączone są w bazy danych. W najprostszej sytuacji baza danych Γ to ciąg elementów deklaratywnych. W wielu praktycznych sytuacjach bazy mają bardziej skomplikowaną strukturę. Na przykład struktura porządku częściowego bywa wykorzystywana w formalizacjach wnioskowania z domyślnymi założeniami odnośnie struktury opisywanego świata. W naszych zastosowaniach wystarczą, na razie, najprostsze liniowe struktury baz danych, czyli ciągi.

  Istotnym założeniem jest, iż bazy danych można modyfikować poprzez zastąpienie wyróżnionego elementu deklaratywnego jednej bazy inną bazą. W bardziej skomplikowanych sytuacja operacje takie mogą zniszczyć integralność bazy.

• Relacja konsekwencji. Podstawowym obiektem studiów jest binarna relacja łacząca bazy danych z pojedyńczymi elementami deklaratywnymi zwana relacją konsekwencji. Pisząc Γ||- λ:A formalizujemy podstawową, powtarzającą się we wszystkich logikach sytuację, gdy (etykietowana) formuła jest konsekwencją założeń formalizowanych przez Γ.

Zadania badawcze

W ramach projektu pragniemy zająć się dwoma sytuacjami w których formalizm Etykietowanych Systemów Dedukcyjnych znajduje naturalne zastosowanie. Prawdę mówiąc już raz wykorzystaliśmy ten formalizm do syntetycznego opisu podstawowych zagadnień programistycznych w części Tematyka projektu niniejszego opisu.

W obu sytuacjach programy spełniać będą rolę etykiet. Różnica polegać będzie na funkcji jaką przypisywać chcemy formułom. W pierwszym przypadku będziemy traktować je jako specyfikacje, w drugim zaś jako typy.

A. Programy imperatywne specyfikowane formułami logiki predykatów z jawnymi zastąpieniami.

Podstawowym wyróżnikiem proponowanego podejścia, w porównaniu do prac innych zespołów pracujących w dziedzinie metodologii programowania i komputerowego wsparcia procesu konstruowania oprogramowania, z polskich należy wymienić djlm94a, djlm94b, st95, jest wybór formalizmu logicznego jako podstawowego języka opisu.

Punktem startu jest przyjęcie, że interesują nas nie tylko gotowe programy, ale również programy niedokończone. Wygodnym sposobem mówienia o takich programach jest przyjęcie, iż dysponujemy klasą zmiennych przebiegających programy. Zmienne takie pełnią rolę parametrów w konstruowanych programach.

Z punktu widzenia formalizmu Etykietownych Systemów Dedukcyjnych jest już jasne jakie będzimy mieli elementy deklaratywne. Są to pary postaci λ:A, gdzie λ jest parametrycznym programem imperatywnym, zaś A jest formułą logiki predykatów z równością i jawnymi zastąpieniami, ozn.: LP_σ⁼. Formuły logiki LP_σ⁼, patrz bed95-opis, bed96-opis interpretowane są w dziedzinie transformat predykatów. Dlatego jednym z elementów projektu będzie badanie związków pomiędzy naszym formalizmem, a formalizmami opartymi na interpretacji programów jako transformat predykatów, dij76, ds90. Szczególnie interesujące wydaje się porównanie z opracowaną przez J-R. Abriala metodą B, patrz abr96, która jest również oparta na formaliźmie wykorzystującym jawne specyfikacje do specyfikowania programów.

Interesujące nas bazy mają postać ciągu (a właściwie zbioru) założeń na temat własności parametrów, tzn na temat własności zmiennych programowych używanych w konstrukcjach sparametryzowanych programów.

Zatem relacja konsekwencji

p₁:A₁,..., p_n:A_n ||- λ(p₁,..., p_n): A

formalizuje intuicję, iż program λ, w którym pojawiać się mogą jako parametry zmienne p₁, ..., p_n, spełnia specyfikację A, jeśli tylko parametry spełniają p₁:A₁, ..., p_n:A_n. Warto zwrócić uwagę na fakt, że obecnie koegzystują dwie relacje konsekwencji. Prócz ||- drugą jest relacja konsekwencji związana z logiką specyfikacji LP_σ⁼.

Przyjęcie powyższej perspektywy powoduje, że proces konstruowania, weryfikowania oraz specyfikowania oprogramowania sytuuje się w domenie logiki. Możemy więc, w przeciwieństwie do alternatywnych metodologii, by wymienić tylko djlm94a, djlm94b, kst94, st95, z krajowego podwórka, myśleć o implementacji proponowanej metodologii w generycznych systemach kodowania logik i dowodzenia twierdzeń w rodzaju Isabelle siłami pracowników projektu. Oczywiście tracimy w ten sposób nadzieję na dorównanie w efektywności systemom specjalizowanym, w rodzaju CAProDel, djlm94a, djlm94b, czy EML, kst94, st95. Zyskujemy w zamian narzędzie pozwalające przetestować w praktyce przydatność teoretycznych pomysłów bez konieczności zatrudniania profesjonalnych programistów.

Chcemy kontynuować dotychczasowe osiągniecia, bb95-opis, bb96-opis, w zakresie programów imperatywnych. W szczególności zamierzamy rozszerzyć prosty dotychczas język programistyczny o nowe konstrukcje: procedury z parametrami, funkcje, deklaracje lokalne, itp.

Użyteczność formalizmu etykietownaych systemów dedukcyjnych zamierzamy zademonstrować wykazując, że pewne konstrukcje programistyczne znajdują adekwatny opis dopiero w tym formaliźmie. W szczególności, moduły odpowiadają spójnikowi implikacji związanemu z relacją konsekwencji ||-.

Zamierzamy zademonstrować użyteczność proponowanego formalizmu poprzez przeprowadzenie eksperymentów obejmujących konstruowanie, weryfikowanie i specyfikowanie na prostych, ale nietrywialnych przykładach.

Zamierzamy też wykorzystać system Isabelle do zweryfikowania matematycznej poprawności badanych przez nas logik programistycznych, podobnie jak dowiedziono zdrowości Logiki Hoare'a w pracy sok88-opis.

Plan prowadzonych działań w tej grupie tematycznej przedstawia się następująco. Zadania, których sukces zależny jest od zakupu silnej stacji roboczej opatrzono stosownym komentarzem.

• [A1] Opracowanie i kodowanie taktyk i strategii upraszczania i dowodzenia formuł logiki predykatów z jawnymi zastąpieniami.

  Jest to połączenie pracy koncepcyjnej z pracami programistycznymi wymagającymi oprogramowania, które posiadamy, oraz sprzętu o który występujemy.

• [A2] Rozszerzenie logiki pLSD o procedury i funkcje.

• [A3] Rozszerzenie logiki pLSD o moduły wyższych rzędów.

• [A4] Przeprowadzenie eksperymentów obejmujących konstruowanie, weryfikowanie i specyfikowanie na prostych, ale nietrywialnych przykładach.

  Jest to praca której sukces w istotny sposób zależy od przyznania funduszy na zakup sprzętu.

• [A5] Weryfikacja matematycznej poprawności badanych przez nas logik programistycznych w formie przeprowadzenia formalnego dowodu zdrowości pod kontrolą Isabelle lub innego edytora dowodów.

  Jest to praca której sukces w istotny sposób zależy od przyznania funduszy na zakup sprzętu.

W chwili obecnej pod kierunkiem Marka Bednarczyka prowadzone są w Instytucie Matematyki Uniwersytetu Gdańskiego prace magisterskie dotyczące wykorzystania zakodowanej już wersji logiki pLSD do konstrukcji i weryfikacji oprogramowania, patrz krytenko97, kolejne w przygotowaniu. Liczymy, że w zadaniach A1 oraz A4 będą mogli również uczestniczyć magistranci IM UG.

B. Wnioskowanie o procesach reaktywnych

Wnioskowanie o procesach reaktywnych może być w znacznym stopniu zautomatyzowane w przypadku systemów o skończonej liczbie stanów, patrz ces86, bcetc90. Procesy przekazujące wartości nie spełniają na ogół tego warunku, gdyż zakłada się zwykle, że dziedzina tych wartości jest (z praktycznego punktu widzenia) nieskończona. Oznacza to, że całkowita automatyzacja procesów przekazujących wartości nie jest możliwa.

Nawet w przypadku procesów skończonych, typowy dla współbieżności kombinatoryczny wzrost komplikacji problemów wnioskowania wraz ze wzrostem wielkości problemu (wielkość problemu mierzy się zazwyczaj liczbą stanów procesu) powoduje, że i w tym przypadku automatyczne techniki nie radzą sobie z problemami występującymi w praktyce.

W związku z powyższym istotnego znaczenia nabierają techniki pozwalające, choćby częściowo, zautomatyzować weryfikację, a zwłaszcza wspierać modularne techniki konstruowania procesów.

Jednym z obiecujących podejść jest takie sformułowanie metod weryfikacji, które pozwoliłoby na zakodowanie zagadnienia weryfikowania w edytorach dowodów ogólnego zastosowania, np.: HOL, LEGO, ALF czy Isabelle. Taki punkt startu odróżnia naszą propozycję od zbliżonej tematycznie pracy nad budową dedykowanych systemów wspomagania wnioskowania o własnościach procesów współbieżnych, lin95. Jedną z zalet naszej propozycji jest eliminacja kosztownego procesu implementowania dedykowanego systemu.

Jako punkt wyjścia wyjścia przyjmujemy prace infinity96-opis, lin96, w których podana jest charakteryzacja silnej bisymulacji dla pewnej reprezentacji procesów przekazujących wartości. Silna bisymulacja jest jedną ze standardowych równoważności rozważanych na procesach. Różne warianty tego pojęcia wykorzystuje się zwykle do wykazania, że jakiś bardzo skomplikowany proces implementuje inny proces traktowany jako abstrakcyjna specyfikacja tego pierwszego.

Charakteryzacja silnej bisymulacji podana w infinity96-opis stanowić będzie podstawę techniki dowodzenia silnej bisymulacji. Próba implementacji tej techniki w generycznym edytorze logik i dowodów, wraz z opracowaniem mechanizmów upraszczania i autoamtyzacji takich dowodów stanowić ma jedno z zadań tego obszaru projektu.

Z drugiej strony, celowe jest podjęcie prób zautomatyzowania procesu generowania formuł charakteryzujących bisymulację pojawiających się w infinity96-opis, lin96. Interesującym kierunkiem badań jest tu poszukiwanie zastosowań logiki predykatów z równością i jawnymi zastąpieniami LP_σ⁼.

Procesy reaktywne badane przez Olderoga, patrz old91, studiowane już były przez nas w formaliźmie zbliżonym do formalizmu Etykietowanych Systemów Dedukcyjnych, patrz pps96-opis. Pragniemy połączyć dotychczasowe osiągnięcia teoretyczne, z pomysłami na implementacje logik modalnych prezentowanych w formalizmie Etykietowanych Systemów Dedukcyjnych, bmv95.

W podobnym kierunku idą prace dotyczące wykorzystania µ-rachunku pierwszego rzędu do specyfikowania procesów przekazujących wartości, patrz rh96. Mamy zamiar uczestniczyć w tych badaniach.

Reasumując, plan prowadzonych działań w tej grupie tematycznej przedstawia się następująco. Zadania, których sukces zależny jest od zakupu silnej stacji roboczej opatrono stosownym komentarzem.

• [B1] Opracowanie mechanizmów kodowania silnej bisymulacji symbolicznej w edytorze dowodów.

  Jest to połączenie pracy koncepcyjnej z pracami programistycznymi wymagającymi oprogramowania, które posiadamy, oraz sprzętu o który występujemy.

• [B2] Badanie zastosowań logiki LP_σ⁼ do specyfikowania procesów.

• [B3] Zakodowanie zmodyfikowanej logiki Olderoga w edytorze dowodów.

• [B4] Opracowanie mechanizmów kodowania słabej bisymulacji symbolicznej na prostych, ale nietrywialnych przykładach.

• [B5] Przeprowadzenie eksperymentów obejmujących konstruowanie i weryfikowanie procesów na prostych, ale nietrywialnych przykładach.

  Jest to praca której sukces w istotny sposób zależy od przyznania funduszy na zakup sprzętu.

C. Programy jako etykiety, formuły jako typy

Jedną z uznanych metod kontroli zachowania programu jest jego typowanie. Można je traktować jako bardzo głęboką analizę składniową: statycznie, a więc jeszcze przed wykonaniem programu, przypisuje mu się pewien typ. Sprowadza się to do wywodu twierdzenia postaci p:tp w pewnym logicznym systemie wnioskowania (systemie typów) --- p jest tu rozpatrywanym programem, tp oznacza typ. Programy, którym nie da się przypisać żadnego typu (ew. pożądanego typu) uznaje się za niepoprawne a o programach z przypisanym typem można powiedzieć, że przeszły przez pierwsze sito kontroli. ,,Gęstość'' tego sita zależy od konkretnie przyjętego systemu typów. Systemy rozpatrywane w konstruktywnej teorii typów (patrz np. MartinLoef) są tak bogate, że typy mogą służyć jako pełne specyfikacje programów a program poprawnie się typujący jest po prostu poprawny. Ceną za to są bardzo poważne trudności w konstruowaniu programu żądanego typu a w pewnych podejściach również w wyprowadzaniu twierdzeń p:tp dla danych p i tp. Na drugim końcu skali znajduje się klasyczny system Hindleya-Milnera Mil78, w którym przypisywanie typów programom jest w pełni automatyczne, do każdego typu łatwo znaleźć (trywialny) program tego typu, ale z tego, że program jest danego typu, nie wynikają żadne dalej idące wnioski odnośnie jego semantycznej poprawności lub własności stopu.

Jak zwykle w takich przypadkach potrzebna jest jakaś pragmatycznie uzasadniona droga pośrednia. Jednak nietrywialne wzbogacenia systemu Hindleya-Milnera prowadzą do systemów, w których automatyczne typowanie jest niewykonalne. Stąd pomysł, żeby analiza statyczna produkowała listę warunków, od których prawdziwości zależy poprawność przypisanego typu.

Praca SW95 powstała we współpracy z Uniwersytetem w Glasgow (grant EPSRC nr GR/K 26608) proponuje taki właśnie system typów zawierający funkcyjne typy zależne oraz pewną postać typów podzbiorowych (programy są tu termami rozszerzonego w odpowiedni sposób λ-rachunku). Z tego, że p:tp₁--> tp₂, wynika m.in., że p jest całkowity na tp₁ (czyli zatrzymuje się dla wszystkich danych z tp₁) --- a więc omawiany system typów nie może być rozstrzygalny. Jednak cała tkwiąca w nim nierozstrzygalność sprowadza się do nierozstrzygalności teorii logicznej będącej niezależnym parametrem systemu. Wygenerowane warunki, od których zależy poprawność typowania są tezami twierdzeń w tej teorii, do których trzeba znaleźć dowody. Może to uczynić ręcznie człowiek, albo jakiś program dowodzenia twierdzeń matematycznych, albo człowiek wspomagany przez program. W SW95 przedstawiono algorytm typowania z generowaniem warunków oraz udowodniono jego poprawność, zupełność i typologiczną zamkniętość redukcji (własność subject reduction). Wcześniejsza wersja algorytmu została zaimplementowana.

W trakcie realizacji Projektu będącego przedmiotem niniejszego wniosku chcielibyśmy zaimplementować doskonalszą wersję algorytmu typującego oraz podłączyć go do jakiegoś programu wspomagającego dowodzenie twierdzeń takiego jak Isabelle. Spodziewamy się, że spośród wielu warunków wygenerowanych przez algorytm typujący program dowodzenia twierdzeń zdoła sam dowieść niektóre i ułatwi programiście udowodnienie pozostałych. Udowodnienie wszystkich daje pewność, że program jest poprawny.

Programy dowodzenia twierdzeń sprawują się tym lepiej im ciaśniej zostanie opisana klasa hipotez, z którymi mogą one mieć do czynienia. Dlatego naszym zadaniem będzie przeanalizowanie warunków poprawnego typowania generowanych przez algorytm dla konkretnych konstrukcji programistycznych (np. dla różnych postaci rekursji). Prawdopodobnie doprowadzi to do zaprogramowania wewnątrz programu dowodzenia twierdzeń pewnej ilości strategii wyspecjalizowanych do dowodzenia twierdzeń, od których zależy typowanie programów. Równolegle będą prowadzone prace mające na celu włączenie do systemu typów nowych dotąd nierozpatrywanych konstrukcji programistycznych. Takim rozszerzeniom systemu typów musi każdorazowo towarzyszyć wzbogacanie algorytmu typowania i udowadnianie poprawności, zupełności i zamkniętości redukcji jego kolejnych wersji.

Tak więc planujemy zrealizowanie w Projekcie następujących zadań:

• [C1] Zakodowanie istniejącego algorytmu typowania z generowaniem warunków dla rozpatrywanego rozszerzenia λ-rachunku.

  Jest to praca programistyczna wymagająca oprogramowania, które posiadamy, oraz sprzętu o który występujemy.

• [C2] Opracowanie nowego języka programowania opartego na tej wersji λ-rachunku.

• [C3] Rozszerzenie algorytmu na wszystkie konstrukcje nowego języka wraz z dowodem poprawności, zupełności i zamkniętości redukcji. Przypuszczamy, że zadania C2 i C3 będą wykonywane kilkakrotnie dla coraz to nowych wersji powstającego języka programowania.

• [C4] Przybliżona klasyfikacja warunków generowanych przez algorytm dla typowych programów. Z powodu nierozstrzygalności problemu typowania nie można się tu spodziewać pełnej klasyfikacji.

• [C5] Oprogramowanie sprzęgu między algorytmem typowania a programem dowodzenia twierdzeń. W ten sposób wygenerowane warunki poprawności typowania będą przejmowane przez program dowodzący twierdzenia jako hipotezy wymagające dowodu. Posiadamy kilka różnych systemów komputerowego dowodzenia twierdzeń, a także możliwość łatwego sprowadzenia i osadzenia innych podobnych programów. Spośród nich najlepiej przez nas rozpoznany jest system kodowania logik i dowodzenia twierdzeń Isabelle. Działanie takich programów jak Isabelle wymaga dużych mocy obliczeniowych. Dlatego realizacja tego punktu w istotny sposób zależeć będzie od dostępności sprzętu o który występujemy. Prace programistyczne w ramach zadań C1, C5 będą wykonywane głównie przez studentów i pracowników Uniwersytetu Gdańskiego i staną się tematem prac magisterskich oraz wejdą w skład powstających tam prac doktorskich. Liczymy ponadto na żywą współpracę z profesorami Philem Wadlerem (Bell-Labs) i Tomem Melhamem (Uniwersytet w Glasgow) oraz z prof. Davidem Schmidtem (Kansas State University, USA). Prof. Wadler jest światowej klasy specjalistą w dziedzinie programowania funkcyjnego. Prof. Melham jest autorytetem od automatycznych systemów dowodzących twierdzenia. Prof. Schmidt to fachowiec od problemów semantycznych oraz analizy statycznej języków programowania oraz od programowania funkcyjnego. Łączy nas z nimi wieloletnia współpraca odświeżona w lecie 1995 dwumiesięcznym pobytem Stefana Sokołowskiego na uniwersytecie w Glasgow oraz planowaną na okres sierpień 98--maj 2000 wizytą Stefana Sokołowskiego w Kansas State University.

D. Książka

Zwyczajowo stosowane sposoby rozliczenia realizacji projektu (publikacje konferencyjne i w czasopismach, oprogramowanie) zamierzamy wzbogacić o książkę. W trakcie prac ze studentami konieczne będzie sporządzenie przewodnika opisującego zarówno podstawy stosowanej metodologii, sposoby kodowania logik jak i automatycznego dowodzenia. Zamierzamy zebrać te notatki i doświadczenia, a następnie zredagować i opublikować calość w postaci ksiązki.