SpecVer: Różnice pomiędzy wersjami

Wersja z 15:05, 20 lut 2013

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^[1] 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

Algorytmiczna teoria kolejek FIFO

Algorytmiczna teoria drzew binarnych poszukiwań

Algorytmiczna teoria liczb naturalnych

Zobacz też

• Odśmiecanie pamięci

Uwagi

Przypisy

Bibliografia

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