SW wykład 3 - Slajd6

<<powrót do strony wykładu

Semantyka naturalna Semantyka naturalna Tiny Sens definicji Sens definicji, c.d. Dowody Indukcja po strukturze Własności Równoważność semantyczna Kongruencje Semantyka operacyjna a naturalna Semantyka operacyjna a naturalna, c.d. Semantyka operacyjna a naturalna, c.d. Semantyka "denotacyjna" Semantyka operacyjna a naturalna, c.d. Równoważność operacyjna Niedeterminizm Kilka równoważności Równoległość

Ostatni fakt wspomniany przy poprzednim slajdzie wymaga nowej techniki dowodzenia własności programów związanych z ich semantyką naturalną: indukcji po strukturze wyprowadzenia przejść (po strukturze drzewa dowodu, że dana konfiguracja prowadzi do danego stanu).

Aby pokazać, że jakaś własność łączy każdą konfigurację ze stanem końcowym, do którego ona prowadzi, wystarczy pokazać, że własność ta zachodzi dla konfiguracji i stanów końcowych, do których one prowadzą na mocy aksjomatów, oraz że zachodzi ona dla konfiguracji i stanów końcowych, do których one prowadzą na mocy poszczególnych reguł, o ile tylko zachodzi ona dla konfiguracji i stanów końcowych, do których one prowadzą, jak jest to wymagane w przesłankach danej reguły. Tak wypowiedzianą zasadę indukcji formułujemy na slajdzie powyżej dla semantyki naturalnej instrukcji języka TINY.