SpecVer: Różnice pomiędzy wersjami
| Linia 1: | Linia 1: | ||
| − | Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej. | + | Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej [{{odn|odn=b|ref=nie|Kreczmar|1977|s=11}}]. |
| Linia 13: | Linia 13: | ||
Materiały jakie tu zamieszczamy mają pokazać nasz sposób myślenia i kierunki poszukiwań. | 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. | + | 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... | Postaramy sie tę myśl zilustrowac kilkoma przykładami... | ||
| Linia 25: | Linia 25: | ||
::ale nie jest to dokładnie to co proponujemy. W ksiazkach tych znajdujemy algorytmy i ich analiże, twierdzenia dotyczące algorytmów. Wszystko to jednak jest formułowane w tradycyjny sposób, w jezyku pierwszego rzedu. | ::ale nie jest to dokładnie to co proponujemy. W ksiazkach tych znajdujemy algorytmy i ich analiże, 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 | * uważamy, że teorie algorytmiczne powinny | ||
| + | == Zobacz też == | ||
| + | * [[Odśmiecanie pamięci]] | ||
| + | {{Uwagi}} | ||
| + | |||
| + | {{Przypisy}} | ||
| + | <references/> | ||
| + | == Bibliografia == | ||
| + | # ({{odn|odn=a|ref=nie|Kreczmar|1977}}) {{cytuj pismo |odn=tak |odn=a | nazwisko = Kreczmar | imię = Antoni | tytuł = Effectivity problems of Algorithmic Logic | czasopismo = Fundamenta Informaticae | rok = 1977 }} | ||
[[Category:SpecVer]] | [[Category:SpecVer]] | ||
Wersja z 18:48, 3 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 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 nieskromna:
- 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 analiże, 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
Spis treści
Zobacz też
Uwagi
Przypisy
Bibliografia
- (Kreczmar 1977a ↓) Antoni Kreczmar. Effectivity problems of Algorithmic Logic. „Fundamenta Informaticae”, 1977.
