Instytut Informatyki Uniwersytetu Warszawskiego 

 

wykład monograficzny 

 

 

Logika Algorytmiczna
wspomaganie specyfikacji i analizy oprogramowania

 

semestr letni 2006 

wtorki g.12:15 - 14  
sala 3160

 

 

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? 

 

 


 

ostatnia modyfikacja tej strony: 11.01.06