Semantyka i weryfikacja programów/Ćwiczenia 8

Obliczanie funkcji semantycznych. Punkty stałe.

Zadanie 1

Rozpatrzmy język z pierwszego zadania poprzednich ćwiczeń. Przypuśćmy, że w stanie początkowym wszystkie zmienne mają wartość zero. Pokaż jak wygląda obliczenie semantyki programu:

 x := 5;
 if x + 1 + 8 then
   x := x + 4
 else
   x := x + 10

Zadanie 2

Równania semantyczne dla konstrukcji iteracyjnych, które zapisaliśmy w poprzednich ćwiczeniach nie są do końca poprawne. Występuje w nich rekurencja, która nie musi się kończyć, więc w pewnych sytuacjach (programów zapętlających się) równania te nie definiują poprawnie żadnej wartości. Zmienimy to teraz posługując się konstrukcją punktu stałego.

Tutaj definicje stałopunktowe dla kolejnych konstrukcji stałopunktowych po uprzednim przykładzie dla while

Zadanie 3

Korzystając z konstrukcji punktu stałego z dowodu twierdzenia o punkcie stałym, oblicz semantykę programu:

while 0 = 0 do skip

Zadanie 4

Korzystając z konstrukcji punktu stałego z dowodu twierdzenia o punkcie stałym, oblicz semantykę programu:

x := 1;
while not x = 3 do y := y + x;