Streszczenie pracy: Donald Sannella, Andrzej Tarlecki, Essential Concepts of Algebraic Specification and Program Developement. Celem referatu będzie prezentacja tematów do zreferowania w drugim semestrze.

Na seminarium zamierzam opowiedziec o koalgebrach - obiektach dualnych do algebr. Wprowadze ich definicje, a potem na przykladach pokaze jak mozna wykorzystac pojecie koalgebry. Postaram sie opowiedziec rowniez o indukcji i koindukcji jako o sposobach definiowania funkcji i dowodzenia rownosci, a takze o ich zwiazku z istnieniem i wlasnosciami algebr poczatkowych i koalgebr koncowych.

Postaram sie delikatnie naszkicowac dziedzine specyfikacji algebraicznych, opierajac sie na pierwszym rozdziale pracy: Donald Sannella, Andrzej Tarlecki - "Essential Concepts of Algebraic Specification and Program Developement". Bazujac na podanych przykladach i zasugerowanych intuicjach, zaprezentuje teorie instytucji, jako najbardziej ogolne ujecie pola, na ktorym mozna uzywac lub uprawiac specyfikacje algebraiczne.

Zostana zaprezentowane proste przyklady zastosowania operacji budujacych specyfikacje. Naszym celem bedzie zilustrowane ogolnych definicji podanych w pierwszej czesci referatu.

Punktem wyjsciowym w procesie tworzenia systemu informatycznego jest stworzenie specyfikacji wymagan. Jest ona dokladna (sic!) definicja tego co system powinien robic, w jakim zakresie, jakie powinien miec wlasciwosci. Specyfikacja dotyczy zarowno systemu jako calosci (moze wtedy sluzyc jako glowny element kontraktu miedzy klientem a wykonawca) jak i komponentow systemu (biedny programista nie musi czytac dlugich listingow by zobaczyc jak dziala komponent, wystarczy (sic!^2) ze przeczyta specyfikacje; dodatkowo mozna wykorzystac w dowodach poprawnosci komponentow opierajac sie na poprawnosci komponentow skladowych).

Oczywiscie z procesem tworzenia specyfikacji zwiazane sa rozne problemy: (coz, swiat bylby nudny bez problemow) - jak stworzyc specyfikacje, jesli klient sam nie wie czego chce - jak stworzyc specyfikacje spojna i pelna - jak zapisac specyfikacje, by jej ciagle zmiany byly latwo wprowadzalne (i w ogole problem ewolucji specyfikacji) - problemy z walidacja, czyli sprawdzeniem czy to co napisalismy w specyfikacji na pewno jest tym, "co tygrysy lubia najbardziej" - problemy z weryfikacja, vzyli czy nasz program na pewno odpowiada specyfikacji (tzn. ja spelnia)

Juz w czwartek opowiem wiecej o powyzszych problemach, sposobach ich rozwiazywania i kolejnych problemach rodzacych sie z rozwiazan.

Pierwszym krokiem w kierunku budowania specyfikacji w sposob strukturalny jest stworzenie formalnego jezyka sluzacego do opisu tychze. Drugim krokiem jest nadanie formulom tego jezyka precyzyjnej semantyki. W tym miejscu pojawiaja sie pytania:

• czy specyfikacja gwarantuje, ze specyfikowany program bedzie mial konkretna wlasnosc,
• czy jedna specyfikacja stanowi ,,doprecyzowanie'' (refinement) drugiej specyfikacji,
• czy dany program jest poprawna realizacja specyfikacji.

Dotychczas prezentowane dziedziny semantyczne D byly czesciowymi porzadkami , zas programy odpowiadaly funkcjom f: D -> D ( morfizmom) miedzy dziedzinami. To znaczy jezeli program wystartowal w stanie x z dziedziny D i

• jesli obliczenie konczylo sie to koncowy stan byl reprezentowany przez f(x)
• jesli obliczenie bylo nieskonczone to f(x) bylo specjalnym elementem dziedziny.

Postaram sie naszkicowac mechanizmy potrzebne do specyfikacji programow sparametryzowanych. Taka specyfikacja jest opisem (np. sygnatury z aksjomatami w EML) programu wejsciowego i wyjsciowego. Implementacja konstruktorowa, przy zastosowaniu funktorow wyzszego rzedu, moze zostac zastosowana do tworzenia takich specyfikacji.

Kolejny referat poswiecony procesowi implementacji specyfikacji algebraicznej.

Pomysl ,,behawioralnej'' semantyki specyfikacji opiera sie na bardzo naturalnym zalozeniu, ze specyfikacja powinna opisywac tylko zewnetrze (obserwowalne) zachowanie systemu (programu, modulu programistycznego, itd.) pozostawiajac swobode co do jego ukrytej (nieobserwowalnej) czesci. Takie podejscie jest bardzo przydatne w sytuacjach, gdy standardowe pojecie implementacji zbytnio ogranicza klase modeli.

Podczas referatu omowione zostanie pojecie semantyki behawioralnej, zilustrowane przykladami i porownane z implementacja konstruktorowa.

Referat na podstawie tekstow:

• "Specification Languages" D. Sannelli i M. Wirsinga, http://www.informatik.uni-bremen.de/~kreo/ifip-WG1.3/ifip_chapters/chapters.html,
• "The Formal Semantics of PVS" S. Owre i N. Shankara, http://www.csl.sri.com/sri-csl-fm.html.

1. Wymagania stawiane JBS

2. Niektore cechy wybranych JBS (Clear, OBJ3, ACT ONE/TWO, ASL, Larch, EML, SPECTRUM, PLUSS, PVS, VDM, Z, EHDM, HOL, TPS, Coq, Nuprl)

3. Cechy zalezne od otoczenia, w jakim wykorzystywany bedzie jezyk: zakres zastosowan; poziom abstrakcji; wspierany paradygmat programowania; wsparcie procesu wywarzania oprogramowania; dostarczane narzedzia

4. Ogolne decyzje projektowe: czytelnosc zrodel; decyzje zwiazane z semantyka; struktura definicji jezyka

5. Specyfikowanie "niskopoziomowe": instytucje; sygnatury i system typow; ekspresywnosc logiki; funkcje czesciowe, zapetlenia i wyjatki; atrybuty; wybor algebr

6. Specyfikowanie "wysokopoziomowe": odrebne mechanizmy jezykowe; niezaleznosc od instytucji; repertuar operacji tworzacych specyfikacje; wzbogacanie specyfikacji; dzielenie specyfikacji; ukrywanie konstrukcji pomocniczych; uzywanie roznych instytucji

7. Parametryzacja: implicite czy explicite; specyfikacje parametryzowane a specyfikacje modulow parametryzowanych; polimorfizm a parametryzacja; funkcje wyzszego rzedu a parametryzacja

8. Skladnia: skladnia wyrazen; widocznosc nazw

9. Wytwarzanie oprogramowania: metodyka tworzenia oprogramowania; wspierany paradygmat programowania; ulepszanie (refinement)