SW wykład 4 - Slajd18

<<powrót do strony wykładu

Semantyka denotacyjna Dziedziny składniowe i semantyczne Funkcje semantyczne Kompozycjonalność Tiny. Semantyka denotacyjna Tiny. Semantyka denotacyjna, c.d. Pojęcia pomocnicze Pojęcia pomocnicze, c.d. |Tiny. Semantyka denotacyjna, c.d. Tiny. Semantyka denotacyjna, c.d. Problem z while Konstrukcje stałopunktowe Konstrukcje stałopunktowe, c.d. Konstrukcje stałopunktowe, c.d. Przykład Przykład, c.d. Dowód Dowód Zgodność semantyki denotacyjnej

A teraz dowód implikacji przeciwnej: jeśli któraś z iteracji związanego z pętlą operatora na funkcji pustej dla pewnego stanu początkowego jako argumentu jest określona, to jej wynik jest stanem końcowym obliczenia pętli rozpoczynającego się w tym stanie początkowym. Korzystać będziemy z założenia, że jeśli znaczenie ciała pętli jest funkcją, która dla pewnego stanu daje wynik, to wynik ten jest stanem końcowym obliczenia ciała pętli rozpoczynającego się w tym stanie.

Dowód przebiega przez indukcję względem "poziomu" iteracji operatora na funkcji pustej. Zauważmy, że nie może to być iteracja zerowa. Dla kolejnych iteracji, rozpiszmy ich wartość na dowolnym stanie początkowym, zgodnie z definicją iteracji i definicją operatora dla danej instrukcji pętli. Znów rozważamy dwa przypadki.

Po pierwsze, przypuśćmy, że wartością warunku pętli w stanie początkowym jest fałsz. Wówczas wynikiem każdej niezerowej iteracji operatora na funkcji pustej dla tego stanu jest tenże stan. Jednocześnie obliczenie pętli w tym stanie kończy się po jednym kroku w tymże stanie. Zamyka to dowód w tym przypadku.

Przypadek przeciwny: załóżmy, że wartością warunku pętli w stanie początkowym jest prawda. Wówczas wynikiem naszej iteracji operatora na funkcji pustej dla tego stanu początkowego jest wynik poprzedniej iteracji operatora na funkcji pustej dla stanu pośredniego, który jest wynikiem znaczenia ciała pętli dla stanu początkowego. Z założenia mamy zatem obliczenie ciała pętli w stanie początkowym prowadzące do tegoż stanu pośredniego, a z założenia indukcyjnego obliczenie pętli w tym stanie pośrednim prowadzi do wyniku poprzedniej iteracji operatora na funkcji pustej dla stanu pośredniego. Składając te obliczenia zgodnie z jednym z udowodnionych na wykładzie o semantyce operacyjnej faktów (patrz slajd 23 tegoż wykładu), z definicji semantyki operacyjnej dla pętli otrzymujemy obliczenie całej pętli, prowadzące od stanu początkowego do wyniku naszej iteracji operatora na funkcji pustej dla tego stanu początkowego.

Koniec dowodu.