SpecVer: Różnice pomiędzy wersjami

Aktualna wersja na dzień 12:16, 16 mar 2020

Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej.

Zagadka. Spróbuj swych sił -- czy potrafisz sformułowac tezę o programie PawelG i podać dowód.

Proponujemy realizację projektu w którym będą współistnieć dokumenty co najmniej 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ł.Zobacz Analiza przykładu
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 biblioteki 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]K[/math],
• weryfikacja czyli dowód tego, że klasa [math]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^[1] niezobowiązująco powiedział "stworzenie większego systemu programistycznego to praca podobna do zbudowania wielu teorii matematycznych". Dziś potrafimy myśl tę precyzyjnie uzasadnic.. Dokładniej mamy 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 zilustrować 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.

Przykład analizy przeprowadzonej z wykorzystaniem rachunku programów

Jeden z lepiej przez nas udokumentowanych programów to program symulacji banku. Prezentację omawiającą zasadę faktoryzacji zadania programistycznego na podzadania polegające na specyfikowaniu klas, ich implementacji i późniejszej weryfikacji tj dowodzeniu poprawności skonstruowanej klasy z jej specyfikacją możesz znaleźć tutaj.Jeśli chcesz to obejrzyj pełny tekst programu symulacja oddziału banku. Istotną część tego programu stanowi klasa Simulation i dwie klasy pomocnicze dla Symulacji. Klasa Symulacja jest implementacją języka wspomagającego zadanie symulacji i jest wielokrotnie stosowana. Z tego względu zadaliśmy sobie trud podania specyfikacji tej klasy. Dzięki temu programista wykorzystujący klasę Simulation nie musi jej czytać, ani poznawać szczegóły implementacyjne. W pracy "Proving Simulation class" udowodniliśmy, ze klasa ta poprawnie implementuje specyfikację. Warto zwrócić uwagę na fakt, że klasa Simulation i dwie klasy pomocnicze to razem ponad 250 linii programu w Loglanie. Zalecamy też przeczytanie 2 prac o technologii SpecVer i o dowodzie poprawności implementacji pomocniczej klasy PriorityQueues.

Algorytmiczna teoria stosów

Algebraiczna czy algorytmiczna specyfikacja stosów? Przypomnijmy, inspiracja do tworzenia algebraicznych 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.Por. książka Barbary Liskov i Johna Guttaga Abstraction and Specification in Program development, MIT Press, 1986

Tymczasem okazało się, że np.:

• 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ę następującą 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 kolejek FIFO

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

Uważam, że należy rozwijać teorię, która połączy w jedną całość kilka różnych teorii: teorię liczb naturalnych, teorię funkcji rekurencyjnych, analizę algorytmów wykonujących obliczenia w dziedzinie liczb naturalnych (tzw. algorytmiczna teoria liczb naturalnych. arytmetykę teoretyczną
Aksjomaty algorytmicznej teorii liczb naturalnych
A1) [math]\forall x\, \{y:=0;\,\textbf{while }\neg x=y \textbf{ do }y:=y+1 \textbf{ od} \}(x=y) [/math]
A2) [math]\forall x\, \neg x+1=0 [/math]
A3) [math]\forall x \forall y\, (x+1=y+1)\rightarrow{x=y} [/math]
Z tych trzech aksjomatów potrafimy wyprowadzić wszystkie aksjomaty teorii Peano, w tym schemat indukcji.

Rozpatrzmy kilka przykładów:

1. algorytm Euklidesa - jak udowodnić poprawność tego algorytmu? Nie wynika ona z aksjomatów Peano. Natomiast z algorytmicznego aksjomatu być liczbą naturalną wynika algorytmiczna formuła [math]\forall x \{\textbf{while }\neg x=0 \textbf{ do }y:=y-1 \textbf{ od} \}(x=0) [/math]. Z tej algorytmicznej formuły - wynika formuła algorytmiczna wyrażająca własnośc stopu algorytmu Euklidesa.
2. problem Collatza - ten prosty algorytm może mieć obliczenia nieskończone w niestandardowym modelu liczb naturalnych z dodawaniem,
3. ostatnie (wielkie) twierdzenie Fermata mówi m. in. że pewien dość prosty program ma obliczenie nieskończone. Dowód Andrew Wilesa ma ponad 200 stron.
4. Wiele hipotez pozostaje wciąż nierozstrzygniętych. Wiadomo jednak, że jeśli są prawdziwe to ich dowody mogą być oparte na trzech aksjomatach i na systemie dedukcyjnym logiki algorytmicznej.

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

Uwagi

Przypisy

Bibliografia

1. (MSS 2007 ↓)Grażyna Mirkowska, Andrzej Salwicki, Oskar Świda. Algorithmic Logic + SpecVer = the methodology for high integrity programming. „Fundamenta Informaticae”, s. 1-17, 2008. 
2. (MSS 2008 ↓)Grażyna Mirkowska, Andrzej Salwicki, Oskar Świda. Verifying a Class: combining Testing and Proving. „Fundamenta Informaticae”, 2009. 
3. (MS 2015 ↓)Grażyna Mirkowska, Andrzej Salwicki. Proving simulation class. , 2015. 
4. (MS 2018 ↓)Grażyna Mirkowska, Andrzej Salwicki: Światły programista. 2018.