Semantyka i weryfikacja programów/Ćwiczenia 4: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 1: | Linia 1: | ||
== Zawartość == | == Zawartość == | ||
| Linia 14: | Linia 13: | ||
Napisz semantykę dużych kroków dla języka wyrażeń, którego semantykę | Napisz semantykę dużych kroków dla języka wyrażeń, którego semantykę małokrokową napisaliśmy na jednych z poprzednich ćwiczeń: | ||
<math> | <math> | ||
| Linia 84: | Linia 83: | ||
Zmodyfikuj semantykę z poprzedniego zadania, aby uzyskać ''leniwą'' ewaluację wyrażeń, zgodnie z dyrektywą: nie obliczaj wyrażenia o ile jego wynik nie jest potrzebny (albo: obliczaj wartość wyrażenia dopiero wtedy, gdy jego wynik jest naprawdę potrzebny). | Zmodyfikuj semantykę z poprzedniego zadania, aby uzyskać ''leniwą'' ewaluację wyrażeń, zgodnie z dyrektywą: nie obliczaj wyrażenia, o ile jego wynik nie jest potrzebny (albo: obliczaj wartość wyrażenia dopiero wtedy, gdy jego wynik jest naprawdę potrzebny). | ||
Spójrzmy na przykład: | Spójrzmy na przykład: | ||
| Linia 119: | Linia 118: | ||
Czyli stan zawiera, dla każdej zmiennej, parę (wyrażenie definiujące, stan w momencie deklaracji). | Czyli stan zawiera, dla każdej zmiennej, parę (wyrażenie definiujące, stan w momencie deklaracji). | ||
Uważnego Czytelnika zapewne zaniepokoił fakt, że <math>\mathbf{State}</math> stoi zarówno po lewej jak i po prawej stronie równania | Uważnego Czytelnika zapewne zaniepokoił fakt, że <math>\mathbf{State}</math> stoi zarówno po lewej, jak i po prawej stronie równania | ||
<math> | <math> | ||
\mathbf{State} \, = \, \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \mathbf{State}. | \mathbf{State} \, = \, \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \mathbf{State}. | ||
</math> | </math> | ||
Również zapis <math>s[x \mapsto (e_1, s)]</math> może wzbudzić niepokój, gdyż sugeruje on, iż <math>s(x)</math> zawiera | Również zapis <math>s[x \mapsto (e_1, s)]</math> może wzbudzić niepokój, gdyż sugeruje on, iż <math>s(x)</math> zawiera jako jeden z elementów pary obiekt "tego samego typu" co <math>s</math>. | ||
Formalnego rozwiązania tego typu dylematów dostarcza teoria dziedzin. | Formalnego rozwiązania tego typu dylematów dostarcza teoria dziedzin. | ||
Natomiast na użytek semantyki operacyjnej wystarczy, jeśli uznamy, iż równanie | Natomiast na użytek semantyki operacyjnej wystarczy, jeśli uznamy, iż równanie | ||
| Linia 170: | Linia 169: | ||
Rozważmy teraz zupełnie inny mechanizm wiązania identyfikatorów | Rozważmy teraz zupełnie inny mechanizm wiązania identyfikatorów zwany ''wiązaniem dynamicznym''. | ||
Dla odróżnienia, dotychczasowy sposób wiązania (widoczności) identyfikatorów będziemy nazywać ''wiązaniem statycznym''. | Dla odróżnienia, dotychczasowy sposób wiązania (widoczności) identyfikatorów będziemy nazywać ''wiązaniem statycznym''. | ||
Oto przykładowe wyrażenie: | Oto przykładowe wyrażenie: | ||
| Linia 179: | Linia 178: | ||
które nie ma wartości w pustym stanie początkowym, według semantyk z poprzednich zadań, ponieważ odwołanie do zmiennej <math>x</math> w deklaracji <math>y = x+1</math> jest niepoprawne. | które nie ma wartości w pustym stanie początkowym, według semantyk z poprzednich zadań, ponieważ odwołanie do zmiennej <math>x</math> w deklaracji <math>y = x+1</math> jest niepoprawne. | ||
Tak samo jest nawet w semantyce leniwej, gdyż wartość zmiennej <math>y</math> będzie w końcu policzona | Tak samo jest nawet w semantyce leniwej, gdyż wartość zmiennej <math>y</math> będzie w końcu policzona i będzie wymagała odwołania do <math>x</math> w stanie pustym. | ||
Natomiast wyobrażmy sobie, że zmieniamy semantykę leniwą następująco: odwołanie do zmiennej <math>x</math> podczas obliczania wartości <math>y</math> będzie odnosiło się nie do stanu w momencie deklaracji <math>y</math>, ale do stanu w momencie ''odwołania'' do <math>y</math>. | Natomiast wyobrażmy sobie, że zmieniamy semantykę leniwą następująco: odwołanie do zmiennej <math>x</math> podczas obliczania wartości <math>y</math> będzie odnosiło się nie do stanu w momencie deklaracji <math>y</math>, ale do stanu w momencie ''odwołania'' do <math>y</math>. | ||
| Linia 193: | Linia 192: | ||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | ||
Teraz w stanie wystarczy przechowywać | Teraz w stanie wystarczy przechowywać "wyrażenie" definiujące wartość danej zmiennej: | ||
<math> | <math> | ||
| Linia 268: | Linia 267: | ||
</math> | </math> | ||
oblicza się również do pewnej wartość, która w tym przypadku powinna reprezentować jakoś ''funkcję'' identycznościową. Wystarczającą reprezentacją funkcji będzie trójka: | oblicza się również do pewnej wartość, która w tym przypadku powinna reprezentować jakoś ''funkcję'' identycznościową. Wystarczającą reprezentacją funkcji będzie trójka: | ||
<math>\langle x, e, s \rangle</math>, gdzie <math>x</math> jest nazwą parametru formalnego, <math>e</math> jest ciałem funkcji a <math>s</math> jest stanem, w którym należy obliczać wartość funkcji po zaaplikowaniu do jakiegoś parametru aktualnego. | <math>\langle x, e, s \rangle</math>, gdzie <math>x</math> jest nazwą parametru formalnego, <math>e</math> jest ciałem funkcji, a <math>s</math> jest stanem, w którym należy obliczać wartość funkcji po zaaplikowaniu do jakiegoś parametru aktualnego. | ||
Oto prosty przykład pokazujący, dlaczego powinniśmy pamiętać stan: | Oto prosty przykład pokazujący, dlaczego powinniśmy pamiętać stan: | ||
| Linia 276: | Linia 275: | ||
Funkcja <math>f</math> zwiększa parametr aktualny o <math>x</math>. | Funkcja <math>f</math> zwiększa parametr aktualny o <math>x</math>. | ||
Program oblicza się do wartości <math>17</math>, gdyż wystąpienie zmiennej <math>x</math> w ciele funkcji <math>f</math> wiąże statycznie a zatem odnosi się zawsze do deklaracji <math>x = 7</math>, mimo tego, że w momencie wywołania tej funkcji wartość zmiennej <math>x</math> wynosi <math>8</math>. | Program oblicza się do wartości <math>17</math>, gdyż wystąpienie zmiennej <math>x</math> w ciele funkcji <math>f</math> wiąże statycznie, a zatem odnosi się zawsze do deklaracji <math>x = 7</math>, mimo tego, że w momencie wywołania tej funkcji wartość zmiennej <math>x</math> wynosi <math>8</math>. | ||
Oto jedyna reguła, jakiej będziemy potrzebować dla lambda-abstrakcji: | Oto jedyna reguła, jakiej będziemy potrzebować dla lambda-abstrakcji: | ||
| Linia 284: | Linia 283: | ||
</math> | </math> | ||
Nie potrafimy zrobić z funkcją <math>\lambda x. e</math> nic innego jak zapamiętać informację niezbędną do obliczania jej wartości w | Nie potrafimy zrobić z funkcją <math>\lambda x. e</math> nic innego jak zapamiętać informację niezbędną do obliczania jej wartości w przyszłości. | ||
Zatem zbiór wartości | Zatem zbiór wartości będzie następujący: | ||
<math> | <math> | ||
| Linia 343: | Linia 342: | ||
Zaproponuj ''leniwą'' semantykę języka <math>F</math> z mechnizmem przekazywanie parametru | Zaproponuj ''leniwą'' semantykę języka <math>F</math> z mechnizmem przekazywanie parametru "przez nazwę". | ||
Mechanizm ten stanowi leniwy odpowiednik przekazywania przez wartość: nie obliczamy wyrażenia będącego parametrem aktualnym, a zamiast jego wartości przekazujemy do funkcji to wyrażenie wraz ze | Mechanizm ten stanowi leniwy odpowiednik przekazywania przez wartość: nie obliczamy wyrażenia będącego parametrem aktualnym, a zamiast jego wartości przekazujemy do funkcji to wyrażenie wraz ze | ||
stanem z miejsca wywołania funkcji. | stanem z miejsca wywołania funkcji. | ||
| Linia 354: | Linia 353: | ||
który w stanie pustym (wszystkie zmienne nieokreślone) | który w stanie pustym (wszystkie zmienne nieokreślone) | ||
nie ma wartości przy przekazywaniu parametru przez wartość | nie ma wartości przy przekazywaniu parametru przez wartość | ||
(bo odwołanie do zmiennej <math>y</math> jest niepoprawne) a oblicza się | (bo odwołanie do zmiennej <math>y</math> jest niepoprawne), a oblicza się | ||
do wartości <math>7</math> jeśli wybierzemy mechanizm przekazywania przez | do wartości <math>7</math> jeśli wybierzemy mechanizm przekazywania przez | ||
nazwę. | nazwę. | ||
| Linia 405: | Linia 404: | ||
* ma wartość w semantyce statycznej i dynamicznej, ale w każdej inną | * ma wartość w semantyce statycznej i dynamicznej, ale w każdej inną | ||
* ma wartość w semantyce leniwej a nie ma w dynamicznej | * ma wartość w semantyce leniwej, a nie ma w dynamicznej | ||
* ma wartość w semantyce dynamicznej a nie ma w leniwej. | * ma wartość w semantyce dynamicznej, a nie ma w leniwej. | ||
}} | }} | ||
| Linia 436: | Linia 435: | ||
* przez nazwę | * przez nazwę | ||
Ten drugi mechanizm rozumiemy teraz następująco | Ten drugi mechanizm rozumiemy teraz następująco: parametr aktualny nie jest obliczany w momencie zaaplikowania do niego funkcji, | ||
a do ciała funkcji przekazuje się wyrażenie będące parametrem aktualnym. | a do ciała funkcji przekazuje się wyrażenie będące parametrem aktualnym. | ||
W momencie odwołania do parametru formalnego w ciele funkcji, wyrażenie | W momencie odwołania do parametru formalnego w ciele funkcji, wyrażenie | ||
| Linia 446: | Linia 445: | ||
</math> | </math> | ||
Przy przekazywaniu przez wartość | Przy przekazywaniu przez wartość w stanie pustym program się nie obliczy, ponieważ nie da się obliczyć parametru aktualnego <math>x</math>. | ||
Natomiast przy przekazywaniu przez nazwę, parametr aktualny będzie obliczany dopiero w momencie odwołania do parametru formalnego <math>z</math>, czyli w momencie obliczania wartości wyrażenia <math>z + z</math>. | Natomiast przy przekazywaniu przez nazwę, parametr aktualny będzie obliczany dopiero w momencie odwołania do parametru formalnego <math>z</math>, czyli w momencie obliczania wartości wyrażenia <math>z + z</math>. | ||
W stanie tym zmienna <math>x</math> ma już wartość, a zatem wartością całego programu będzie 21. | W stanie tym zmienna <math>x</math> ma już wartość, a zatem wartością całego programu będzie 21. | ||
}} | }} | ||
Wersja z 13:34, 29 wrz 2006
Zawartość
Napiszemy semantykę naturalną języka wyrażeń, rozważymy strategię gorliwą (jak na wcześniejszych zajęciach, w semantyce małych kroków) i leniwą. Rozważymy i statyczne i dynamiczne wiązanie identyfikatorów. Następnie rozszerzymy ten język o lambda-abstrakcję i aplikację, otrzymując prosty język funkcyjny.
Różne semantyki naturalne wyrażeń
Ćwiczenie 1 (semantyka gorliwa)
Napisz semantykę dużych kroków dla języka wyrażeń, którego semantykę małokrokową napisaliśmy na jednych z poprzednich ćwiczeń:
Rozwiązanie
Ćwiczenie 2 (semantyka leniwa)
Zmodyfikuj semantykę z poprzedniego zadania, aby uzyskać leniwą ewaluację wyrażeń, zgodnie z dyrektywą: nie obliczaj wyrażenia, o ile jego wynik nie jest potrzebny (albo: obliczaj wartość wyrażenia dopiero wtedy, gdy jego wynik jest naprawdę potrzebny).
Spójrzmy na przykład:
Według semantyki z poprzedniego zadania wyrażnie to nie ma wartości, bo w deklaracji jest odwołanie do niezainicjowanej zmiennej. Natomiast w semantyce leniwej wyrażenie to obliczy się do wartości , gdyż wyrażenie nie będzie wogóle obliczane. Będzie tak dlatego, że w wyrażeniu nie ma odwołań do zmiennej .
Rozwiązanie
Ćwiczenie 3 (semantyka dynamiczna)
Rozważmy teraz zupełnie inny mechanizm wiązania identyfikatorów zwany wiązaniem dynamicznym.
Dla odróżnienia, dotychczasowy sposób wiązania (widoczności) identyfikatorów będziemy nazywać wiązaniem statycznym.
Oto przykładowe wyrażenie:
które nie ma wartości w pustym stanie początkowym, według semantyk z poprzednich zadań, ponieważ odwołanie do zmiennej w deklaracji jest niepoprawne. Tak samo jest nawet w semantyce leniwej, gdyż wartość zmiennej będzie w końcu policzona i będzie wymagała odwołania do w stanie pustym.
Natomiast wyobrażmy sobie, że zmieniamy semantykę leniwą następująco: odwołanie do zmiennej podczas obliczania wartości będzie odnosiło się nie do stanu w momencie deklaracji , ale do stanu w momencie odwołania do . Jest to dość rewolucyjna zmiana, zapewne sprzeczna z intuicjami programisty (statyczne reguły widoczności zamieniamy na dynamiczne). W szczególności powyższe wyrażenie policzy się w semantyce dynamicznej do wartości 11, ponieważ stan w momencie odwołania do zmiennej przypisuje zmiennej wartość 10 !
Napisz semantykę naturalną dla wiązania dynamicznego.
Rozwiązanie
Prosty język funkcyjny
Ćwiczenie 4 (przekazywanie parametru przez wartość)
Rozważmy prosty język funkcyjny rozszerzający język wyrażeń z poprzednich zadań następująco:
Lambda-abstrakcja reprezentuje anonimową (nienazwaną) funkcję jednoargumentową, natomiast wyrażenie to aplikacja do (wyrażenie powinno zatem obliczać się do funkcji). Np.
Przyjmijmy statyczną widoczność identyfikatorów. Możliwe są różne mechanizmy przekazywania parametrów. Na razie wybierzmy mechanizm przekazywania przez wartość, zapewne doskonale znany Czytelnikowi: wyrażenie będące parametrem aktualnym jest obliczane przed wywołaniem funkcji, czyli w stanie, w którym jesteśmy z momencie wywołania funkcji.
Zaproponuj semantykę naturalną dla tego języka dla obydwu mechanizmów przekazywania parametrów.
Rozwiązanie
Ćwiczenie 5 (przekazywanie parametru przez nazwę)
Zaproponuj leniwą semantykę języka z mechnizmem przekazywanie parametru "przez nazwę".
Mechanizm ten stanowi leniwy odpowiednik przekazywania przez wartość: nie obliczamy wyrażenia będącego parametrem aktualnym, a zamiast jego wartości przekazujemy do funkcji to wyrażenie wraz ze
stanem z miejsca wywołania funkcji.
To ten stan bedzie brany pod uwagę, gdy obliczana będzie wartość parametru, tzn. przy odwołaniu w ciele funkcji do parametru formalnego. Oto przykład programu:
który w stanie pustym (wszystkie zmienne nieokreślone) nie ma wartości przy przekazywaniu parametru przez wartość (bo odwołanie do zmiennej jest niepoprawne), a oblicza się do wartości jeśli wybierzemy mechanizm przekazywania przez nazwę.
Rozwiązanie
Zadania domowe
Ćwiczenie 1
Podaj przykład wyrażenia takiego, które:
- ma wartość w semantyce statycznej i dynamicznej, ale w każdej inną
- ma wartość w semantyce leniwej, a nie ma w dynamicznej
- ma wartość w semantyce dynamicznej, a nie ma w leniwej.
Ćwiczenie 2
W semantyce leniwej wyrażeń, jeśli jest wiele odwołań do jakiejś zmiennej, to obliczenie wartości tej zmiennej nastąpi za każdym razem od nowa. Zmodyfikuj tę semantykę tak, aby wartość ta była obliczana co najwyżej raz. Zatem po pierwszym odwołaniu do zmiennej, jej obliczona wartość powinna zostać umieszczona w stanie, zastępując parę (wyrażenie, stan).
Ćwiczenie 3
Zaproponuj dynamiczne odpowiedniki obydwu statycznych semantyk dla języka funkcyjnego . Czyli zakładamy, że widoczność identyfikatorów, m.in. w ciele funkcji, jest dynamiczna. Oto przykład programu, który w semantyce statycznej oblicza się do wartości , a w dynamicznej do wartości (parametr przekazywany przez wartość):
Rozważ dwa mechanizmy przekazywania parametrów:
- przez wartość
- przez nazwę
Ten drugi mechanizm rozumiemy teraz następująco: parametr aktualny nie jest obliczany w momencie zaaplikowania do niego funkcji, a do ciała funkcji przekazuje się wyrażenie będące parametrem aktualnym. W momencie odwołania do parametru formalnego w ciele funkcji, wyrażenie będące parametrem aktualnym jest obliczane w bieżącym stanie (a nie w stanie z miejsca wywołania funkcji). Jako przykład pozważmy program:
Przy przekazywaniu przez wartość w stanie pustym program się nie obliczy, ponieważ nie da się obliczyć parametru aktualnego . Natomiast przy przekazywaniu przez nazwę, parametr aktualny będzie obliczany dopiero w momencie odwołania do parametru formalnego , czyli w momencie obliczania wartości wyrażenia . W stanie tym zmienna ma już wartość, a zatem wartością całego programu będzie 21.
