SW wykład 7 - Slajd7: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
Linia 1: | Linia 1: | ||
{{Semantyka i weryfikacja programów/Wykład 7}} | {{Semantyka i weryfikacja programów/Wykład 7}} | ||
[[Grafika:sw0706.png|center|frame]] | [[Grafika:sw0706.png|center|frame]] | ||
Spróbujmy teraz przeczytać dokładnie dwie przykładowe klauzule dla | |||
semantyki wyrażeń arytmetycznych. | |||
Znaczeniem wyrażenia będącego zmienną jest funkcja, która dla | |||
dowolnego środowiska zmiennych i kontynuacji dla wyrażeń (określającej | |||
potok wyjściowy całego programu dla wartości tego wyrażenia i stanu po | |||
jego obliczeniu) buduje kontynuację (dla instrukcji), która dla | |||
dowolnego stanu (sprzed obliczenia tego wyrażenia) poda potok | |||
wyjściowy całego programu, wykorzystując zadaną jako argument | |||
kontynuację dla wyrażeń. Mianowicie, ten potok wyjściowy to wynik | |||
aplikacji danej kontynuacji dla wyrażeń do wartości, określonej jako | |||
zawartość składu dla lokacji przypisanej danej zmiennej w środowisku | |||
zmiennych, i zadanego jako argument stanu. Oczywiście, jeśli ta | |||
lokacja lub ta wartość nie są dobrze określone, to odpowiedzią jest | |||
sygnał błędu (dokładniej: pusty potok wyjściowy zakończony sygnałem | |||
błędu); zauważmy, że zgodnie z intuicją, potok wyjściowy budowany | |||
przez podawaną jako argument kontynuację "po wyliczeniu wyrażenia" | |||
zostanie w tej "błędnej" sytuacji pominięty. | |||
Znaczeniem wyrażenia będącego sumą dwóch podwyrażeń jest funkcja, | |||
która dla dowolnego środowiska zmiennych i kontynuacji dla wyrażeń | |||
(określającej potok wyjściowy całego programu dla wartości tego | |||
wyrażenia i stanu po jego obliczeniu) buduje kontynuację (dla | |||
instrukcji) określaną jako wynik aplikacji znaczenia pierwszego | |||
podwyrażenia w tym samym środowisku zmiennych do kontynuacji dla | |||
wyrażeń, która przyjmując jako argument wartość (tego pierwszego | |||
podwyrażenia) zbuduje kontynuację określaną jako wynik aplikacji | |||
znaczenia drugiego podwyrażenia w tym samym środowisku zmiennych do | |||
kontynuacji dla wyrażeń, która przyjmując jako argument wartość (tego | |||
drugiego podwyrażenia) zbuduje kontynuację przez aplikację kontynuacji | |||
dla wyrażeń przekazanej jako argument dla znaczenia całego wyrażenia | |||
(sumy) do argumentu, który jest wynikiem dodawania kolejno | |||
otrzymywanych przez to złożone wyrażenie funkcyjne wartości liczbowych | |||
(a więc wartości pierwszego i drugiego podwyrażenia). Pomijamy tu | |||
oczywiscie możliwe wystąpienia sytuacji błędnych, które są | |||
propagowane. | |||
Pozostałe klauzule semantyczne dla wyrażeń arytmetycznych i | |||
wszystkie klauzule semantyczne dla wyrażeń logicznych są podobne; dla | |||
przykładu podajemy tylko dwie z nich, dla jednej ze stałych logicznych | |||
i dla nierówności. Zachęcamy Państwa do samodzielnego wypisania | |||
pozostałych klauzul. |
Wersja z 13:09, 28 wrz 2006
Kontynuacje Kontynuacje wyrażeń i deklaracji Tiny+++ Dziedziny semantyczne Funkcje semantyczne Przykłady klauzul [[SW_wykład_7_-_Slajd7|Przykłady klauzul, c.d.] Instrukcje Bloki Skoki Semantyka skoków Semantyka skoków, c.d. Semantyka skoków, c.d. Semantyka skoków, c.d. Semantyka "standardowa"

Spróbujmy teraz przeczytać dokładnie dwie przykładowe klauzule dla semantyki wyrażeń arytmetycznych.
Znaczeniem wyrażenia będącego zmienną jest funkcja, która dla dowolnego środowiska zmiennych i kontynuacji dla wyrażeń (określającej potok wyjściowy całego programu dla wartości tego wyrażenia i stanu po jego obliczeniu) buduje kontynuację (dla instrukcji), która dla dowolnego stanu (sprzed obliczenia tego wyrażenia) poda potok wyjściowy całego programu, wykorzystując zadaną jako argument kontynuację dla wyrażeń. Mianowicie, ten potok wyjściowy to wynik aplikacji danej kontynuacji dla wyrażeń do wartości, określonej jako zawartość składu dla lokacji przypisanej danej zmiennej w środowisku zmiennych, i zadanego jako argument stanu. Oczywiście, jeśli ta lokacja lub ta wartość nie są dobrze określone, to odpowiedzią jest sygnał błędu (dokładniej: pusty potok wyjściowy zakończony sygnałem błędu); zauważmy, że zgodnie z intuicją, potok wyjściowy budowany przez podawaną jako argument kontynuację "po wyliczeniu wyrażenia" zostanie w tej "błędnej" sytuacji pominięty.
Znaczeniem wyrażenia będącego sumą dwóch podwyrażeń jest funkcja, która dla dowolnego środowiska zmiennych i kontynuacji dla wyrażeń (określającej potok wyjściowy całego programu dla wartości tego wyrażenia i stanu po jego obliczeniu) buduje kontynuację (dla instrukcji) określaną jako wynik aplikacji znaczenia pierwszego podwyrażenia w tym samym środowisku zmiennych do kontynuacji dla wyrażeń, która przyjmując jako argument wartość (tego pierwszego podwyrażenia) zbuduje kontynuację określaną jako wynik aplikacji znaczenia drugiego podwyrażenia w tym samym środowisku zmiennych do kontynuacji dla wyrażeń, która przyjmując jako argument wartość (tego drugiego podwyrażenia) zbuduje kontynuację przez aplikację kontynuacji dla wyrażeń przekazanej jako argument dla znaczenia całego wyrażenia (sumy) do argumentu, który jest wynikiem dodawania kolejno otrzymywanych przez to złożone wyrażenie funkcyjne wartości liczbowych (a więc wartości pierwszego i drugiego podwyrażenia). Pomijamy tu oczywiscie możliwe wystąpienia sytuacji błędnych, które są propagowane.
Pozostałe klauzule semantyczne dla wyrażeń arytmetycznych i wszystkie klauzule semantyczne dla wyrażeń logicznych są podobne; dla przykładu podajemy tylko dwie z nich, dla jednej ze stałych logicznych i dla nierówności. Zachęcamy Państwa do samodzielnego wypisania pozostałych klauzul.