M
o
t
y
w
a
c
j
a

Zastosowania

Teoria

Przemysł informatyczny dostrzegł (po 35 latach od naszych pierwszych publikacji) potrzebę dostarczania programów wraz z dowodami ich poprawności. Utworzono normy ...

Wykład ma zachęcić do poznania rachunku AL w którym można wyrażać semantyczne własności algorytmów, struktur danych i klas, a także języków programowania. Bardzo byśmy chcieli by słuchacze wykorzystali zdobytą wiedzę i umiejętności w firmach (może własnych) oferujących usługi specyfikacji oprogramowania

lub w firmach dokonujących audytu gotowego produktu programistycznego.

W trakcie zajęć omówimy kilka otwartych problemów.

Oto parę z nich:

1. Podać aksjomaty instrukcji przypisania w języku programowania obiektowego. Wydaje się, że znany aksjomat instrukcji przypisania
[x:=w]Alpha = Alpha(x/w)
nie wystarcza. A może ...

2. Czy elementarna teoria kolejek jest rozstrzygalna? Nadal nie znam odpowiedzi na to pytanie.

3. Twierdzenie Fermata mówi, że pewien program w dziedzinie liczb naturalnych nie zatrzymuje się. Czy nie można by tego dowieść analizując ten program?

Logika Algorytmiczna wspomaganie specyfikacji i analizy oprogramowania

Logika Algorytmiczna
wspomaganie specyfikacji i analizy oprogramowania