SpecVer

Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej.

Chcemy zaproponować realizację projektu w którym będą współistnieć dokumenty conajmniej trzech typów:

• specyfikacje,
• moduły klas, procedur, funkcji, etc.,
• dokumenty zawierające argumenty rozstrzygające o poprawności modułu względem specyfikacji.

Projekt SpecVer jest niewątpliwie projektem trudnym. Ale sądzę, że mamy oryginalny pomysł.
Zanim przejdziemy do dalszych szczegółów:

• będziemy rozwijać algorytmiczne teorie rozmaitych struktur i badać ich związki z odpowiednimi klasami,
• jako test naszego podejścia proponujemy zbudowanie biblioteki klas podobnej do znanej bibioteki STL. Różnica ma polegać na tym, że w produkcie końcowym dla każdej klasy mają znaleźć się:

• specyfikacja klasy [math]K[/math] - lub inaczej mówiąc sygnatura i aksjomaty algorytmicznej teorii [math]T_K[/math] opisujące nie tylko interfejs operacji, lecz także własności operacji na obiektach opisywanych przez klasę,
• implementacja czyli klasa [math]T_K[/math],
• weryfikacja czyli dowód tego, że klasa [math]T_K[/math] zapewnia prawdziwość wszystkich własnośności wymienionych w aksjomatach teorii [math]T_K[/math]

Dziś na pewno jest za wcześnie by myśleć o kompletnym opisie tego projektu.

Materiały jakie tu zamieszczamy mają pokazać nasz sposób myślenia i kierunki poszukiwań.

Kiedyś profesor Józef Winkowski powiedział "stworzenie większego systemu programistycznego to praca podobna do zbudowania wielu teorii matematycznych". Dziś jesteśmy o tym przekonani. Dokładniej mam na myśli to, że nie wystarczy tworzyć moduły oprogramowania, ani interfejsy. Potrzebne sa specyfikacje. O specyfikacjach trzeba myśleć w ten sam sposób jak o aksjomatyzacjach teorii sformalizowanych i w związku z tym badać problemy niesprzeczności, pełności, kategoryczności. Co więcej podczas tworzenia werdyktów weryfikujących poprawność tworzymy teorie algorytmiczne i z twierdzeń tych teorii korzystamy podczas dalszej pracy nad kolejnymi programami.

Postaramy sie tę myśl zilustrowac kilkoma przykładami...

Propozycja:

• Od lat postulujemy tworzenie i rozwijamie (sformalizowanych lub nie) teorii algorytmicznych zob. praca Algorithmic theory of stacks, rozdział IV ksiązki Algorithmic Logic, ...
• może wydawać się, że nasze sugestie napotkały pozytywny odzew gdy zauważysz, że powstają monografie:

• Algorithmic theory of Graphs,
• Algorithmic theory of numbers
• Algorithmic theory of ...

Ale nie jest to dokładnie to co proponujemy. W książkach tych znajdujemy algorytmy i ich analizę, twierdzenia dotyczące algorytmów. Wszystko to jednak jest formułowane w tradycyjny sposób, w jezyku pierwszego rzedu.

• Uważamy, że teorie algorytmiczne powinny używać języka w którym oprócz formuł pierwszego rzędu występują programy (algorytmy) i formuły algorytmiczne. Nie jest źle gdy w zbiorze aksjomatów teorii algorytmicznej znajdują się formuły algorytmiczne. Twierdzeniami teorii algorytmicznej są formuły algorytmiczne, które maja dowód w logice algorytmicznej. Aksjomatyzacje teorii algorytmicznych mogą wiele zyskać gdy wsród aksjomatów znajdzie się jedna lub więcej formuł algorytmicznych. Zobacz ksiązki Algorithmic Logic str. ... oraz Logika Algorytmiczna dla Programistów str.

Algorytmiczna teoria stosów

Algebraiczna czy algorytmiczna specyfikacja stosów? Przypomnijmy, inspiracja do tworzenia lgebraicznych specyfikacji struktur danych wypływała z potrzeby upraszczania przekształcania wyrażeń boolowskich występujacych w instrukcjach warunkowych if oraz iteracyjnych while. Szkoda, że badacze nie zadali sobie podstawowych pytań: czy specyfikacja jest pełna? czy tworzy teorię rozstrzygalną? Zamiast tego sformułowano pojęcie specyfikacji wystarczająco zupełnej. Co się okazało:

• Teoria stosów pierwszego rzędu jest rozstrzygalna, zob.
• Teoria ta posiada modele programowalne niestandardowe! Tzn. można napisać program w którym klasa stosy jest napisana w taki sposób, że pewne obiekty tej klasy tzn. pewne stosy zachowają się jak stosy nieskończone.
• Algorytmiczna teoria stosów cieszy się własnością bliską kategoryczności.

Twierdzenie o reprezentacji

Każde dwa modele algorytmicznej teorii stosów w których występuje ten sam zbiór elementów są izomorficzne.

Algorytmiczna teoria drzew binarnych poszukiwań

O tej teorii pisaliśmy w "Logika Algorytmiczna dla programistów". Okazało się, że można podać inną aksjomatyzację. Udowodniliśmy, własność

[math]BST\, \vdash\, (\forall n \in Node)(\forall e \in Elem)\ [call\ insert(e,n)]member(e, n) [/math]

zob. Dowód powyższej własności

Algorytmiczna teoria liczb naturalnych

Język = <Alfabet, Wyrażenia Poprawnie Zbudowane>

Wyrażenia Poprawnie Zbudowane to

- termy,

- formuły pierwszego rzędu, zawierają podzbiór formuł otwartych tzn. formuł bez kwantyfikatorów,

- programy,

- formuły algorytmiczne.

Aksjomaty specyficzne tej teorii

Aksjomaty Logiki Algorytmicznej

Reguły wnioskowania logiki algorytmicznej

przejdź do strony Arytmetyka Algorytmiczna

Narzędzia

Praca osoby dokonującej weryfikacji danego oprogramowania P wzgledem danej specyfikacji S powinna być wspomagana przez wiele narzędzi. Jednym z wielu (nieistniejących jak dotąd) jest

edytor dowodów

Innym narzędziem, które powinno powstać jest proof-checker. Znany mi system Mizar nie nadaje się jednak do naszych celów. Mizar posługuje się językiem pierwszego rzedu tj. językiem predykatów. W naszej pracy posługujemy sie jezykiem formuł algorytmicznych <<PRZYKŁAD>>

Jakie cechy ma mieć nowy proof-checker? przede wszystkim, powinien być skonstruowany nad językiem formuł algorytmicznych. (Może nad klasą języków algorytmicznych). Po drugie, w dowodach uzywać będziemy reguł wnioskowania logiki algorytmicznej. Aksjomaty specyficzne tych teorii w jakich przeprowadzac będziemy dowody mogą być formułami zawierajacymi programy <<PRZYKŁAD>>

Podobno wiele zadań weryfikacji oprogramowania jest dość łatwe by pokusić się o automatyczne dowodzenie (lub konstrukcję kontrprzykładu). Do takich celów powinniśmy posiadać prover lub systemy o podobnych możliwościach.

Zobacz też

• Odśmiecanie pamięci

Bibliografia

1. (Kreczmar 1977b ↓) Antoni Kreczmar. Effectivity problems of Algorithmic Logic. „Fundamenta Informaticae”, 1977.