Semantyka i weryfikacja programów/Ćwiczenia 8

From Studia Informatyczne

Spis treści

Obliczanie funkcji semantycznych. Punkty stałe.

Obliczanie prostych funkcji semantycznych

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

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

Ćwiczenie 1

Pokaż jak wygląda obliczenie semantyki programu:

Rozwiązanie

Jeszcze nie ma

Stosowanie konstrukcji stałopunktowych

Ćwiczenie 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.

Rozwiązanie

Jeszcze nie ma

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

Obliczanie punktów stałych

Dany jest program

while 0 = 0 do skip

Ćwiczenie 3

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

Rozwiązanie

Jeszcze nie ma

Dany jest program

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

Ćwiczenie 4

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

Rozwiązanie

Jeszcze nie ma