SW wykład 2 - Slajd23

<<powrót do strony wykładu

Składnia Składnia konkretna Składnia abstrakcyjna Przyjmowane założenia Przykład wiodący Kategorie składniowe Kategorie składniowe, c.d. Uwagi Indukcja strukturalna Definicje indukcyjne Kategorie semantyczne Wartościowanie zmiennych Semantyka wyrażeń Semantyka wyrażeń logicznych Semantyka instrukcji Prosty fakt Dowód Przezroczystość odwołań Semantyka operacyjna Obliczenia Semantyka operacyjna Tiny Własności Własności, c.d. Warianty definicji

Właśnie przez indukcję względem długości obliczenia można pokazać prostą własność obliczeń dla sekwencyjnego złożenia instrukcji, a dokładniej: obliczeń rozpoczynających się od konfiguracji, które zawierają sekwencyjne złożenie instrukcji jako instrukcję do wykonania.

Pokazujemy tu mianowicie, że każde obliczenie dla złożenia sekwencyjnego instrukcji można rozbić na dwie części: pierwszą, związaną z obliczeniem pierwszej składowej instrukcji, i drugą część, będącą obliczeniem dla drugiej jej składowej --- przy czym długości obliczeń pozostają ze sobą w oczekiwanym związku. Dowód przebiega przez indukcję względem długości obliczenia instrukcji. Początek jest trywialny: puste obliczenie nie może spełniać założeń. Dla niepustego obliczenia, rozważamy jego pierwszy krok. Zgodnie z definicją relacji przejścia, możliwe są dwa przypadki: albo ten pierwszy krok kończy obliczenie pierwszej składowej i wtedy teza zachodzi w sposób oczywisty, albo kolejna konfiguracja zawiera złożenie sekwencyjne "reszty" pierwszej składowej z całą drugą składową. W tym drugim przypadku korzystamy z założenia indukcyjnego (dla krótszego obliczenia, zaczynającego się jednak od konfiguracji zawierającej złożenie sekwencyjne instrukcji).

Prostą konsekwencją tego faktu jest to, że każde obliczenie dla danej instrukcji "generuje" obliczenie dla sekwencyjnego złożenia tej instrukcji z inną instrukcją --- ten dodany do instrukcji "ciąg dalszy" nie wpływa na przebieg obliczeń.