SpecVer: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 15: Linia 15:
 
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. Potzrebne 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.
 
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. Potzrebne 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...
 +
 
 +
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.
 +
* uważamy, że
  
 
[[Category:SpecVer]]
 
[[Category:SpecVer]]

Wersja z 14:36, 3 lut 2013

Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej.


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. Potzrebne 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.

  • uważamy, że