Semantyka i weryfikacja programów/Ćwiczenia 7
Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne.
Pętle while i repeat
Ćwiczenie 1
Zdefiniuj semantykę denotacyjną następującego języka:
Pętla
polega na wykonaniu instrukcji i, a następnie wyliczeniu warunku logicznego b. Jeśli warunek jest prawdziwy wykonanie pętli kończy się, w przeciwnym razie powracamy do wykonania instrukcji i.Powyższy język to tak naprawdę Tiny z wykładu rozszerzony o jedną konstrukcję: pętlę repeat. Spróbuj wykonać to ćwiczenie nie sięgając do notatek z wykładu. Jeśli napotkasz trudności, odkrywaj kolejne elementy poniższego opisu.
Kategorie składniowe występujące w tym języku to:
- wyrażenia Exp
- wyrażenia logiczne BExp
- instrukcje Stmt
- oraz, jak zwykle, stałe liczbowe Num
Zaczynamy jak zwykle od opisu dziedzin semantycznych. Nie przejmujemy się na razie szczegółami związanymi z konstrukcjami stałopunktowymi oraz umieszczeniem pineski we właściwych dziedzinach. Zakładamy, że wszystkie zmienne są zainicjowane na zero.
Użyjemy elementarnych dziedzin z wykładu:
- Int = ..., -1, 0, 1, ... zawierający denotacje stałych
liczbowych
- Bool = {tt}, {ff} zawierający wartości logiczne
- Var zawierający wszystkie dozwolone identyfikatory
Przypomnijmy, że wartość wyrażenia arytmetycznego
zależy odWartości te są "pamiętane" w stanie, który jest funkcją ze zbioru Var w zbiór Int. Zbiór wszystkich stanów to:
Zdefiniujmy następnie niezbędne funkcje semantyczne.
- Dla wyrażeń mamy
- Dla wyrażeń logicznych:
- Dla instrukcji:
- Oraz oczywistą funkcję dla stałych całkowitych:
Funkcji {Z} nie definiujemy, przyjmując jak zwykle, że jej wynikiem jest wartość stałej liczbowej.
Rozpocznijmy od funkcji semantycznej dla wyrażeń. Musimy zdefioniować znaczenie (wartość) wyrażenia
w pewnym stanie . Ową wartość zapisujemy jako , czyli wartość funkcji E zastosowanej do dwóch argumentów: wyrażenia oraz stanu . Przypomnijmy, że taka "dziwna" notacja z nawiasami służy oddzieleniu składni od elementów z metajęzyka.Funkcje semantyczne definiujemy dla każdej postaci wyrażenia, odpowiadając na standardowe pytania:
- Co jest wartością wyrażenia w stanie , Odpowiedź: wartość
zmiennej
w tym stanie, czyli wartość uzyskana przez zastosowanie funkcji do identyfikatora . Zapisujemy to następującoCzęsto będziemy powijać nawiasy przy aplikacji funkcji pisząc po prostu
zamiast . To samo można zapisać stosując notację "lambda":Pętla for
Ćwiczenie 2
Rozszerzmy język z poprzedniego zadania o instrukcję:
Wykonanie takiej pętli polega na:
- Wyliczeniu wartości wyrażenia .
- Przypisaniu wartości na zmienną .
- Wyliczeniu wartości wyrażenia .
- Jeśli , to pętla kończy się.
- W przeciwnym razie:
- Wykonujemy instrukcję .
- Zwiększamy zmienną o 1.
- Powracamy do punktu 3.
Zauważmy, że wyrażenie
jest tu wyliczane tylko raz, ale oblicza się przy każdym obrocie pętli.Rozwiązanie
Ćwiczenie 3
Zmieńmy semantykę instrukcji for z poprzedniego zadania tak, aby oba wyrażenia obliczały się tylko raz. Tym razem wyliczenie pętli polega na:
- Wyliczeniu wartości wyrażenia .
- Przypisaniu wartości na zmienną .
- Wyliczeniu wartości wyrażenia .
- Jeśli , to pętla kończy się.
- W przeciwnym razie:
- Wykonujemy instrukcję .
- Zwiększamy zmienną o 1.
- Powracamy do punktu 4.
Rozwiązanie
Ćwiczenie 4
Rozwiązanie
Ćwiczenie 5
W języku C pętla for ma następującą postać:
Jej wykonanie polega na:
- Wykonaniu instrukcji .
- Wyliczeniu wartości wyrażenia .
- Jeśli wyrażenie wylicza się do fałszu, to pętla kończy się.
- W przeciwnym razie:
- Wykonujemy instrukcję .
- Wykonujemy instrukcję .
- Powracamy do punktu 2.
Rozwiązanie