SpecVer

Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej Kreczmar 1977b ↓, s. 11.

Dziś chcemy spróbować realizacji 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ł.

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 ksiazkach 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ą bliką 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

Zobacz też

• Odśmiecanie pamięci

Bibliografia

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