SW wykład 3 - Slajd4: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Mengel (dyskusja | edycje)
Nie podano opisu zmian
 
Dorota (dyskusja | edycje)
Nie podano opisu zmian
 
(Nie pokazano 2 wersji utworzonych przez 2 użytkowników)
Linia 1: Linia 1:
{{Semantyka i weryfikacja programów/Wykład 3}}
[[Grafika:sw0303.png|center|frame]]
[[Grafika:sw0303.png|center|frame]]
Z drugiej strony, możemy dosłownie potraktować terminologię
"aksjomat", "reguła", itd. i myśleć o prezentacji semantyki naturalnej
jako o formalnym systemie dowodzenia stwierdzeń postaci "dana
konfiguracja prowadzi do danego stanu". Wówczas przyjmiemy, że system
ten definiuje relację przejścia miedzy konfiguracjami i
odpowiadającymi im stanami końcowymi poprzez meta-warunek: dana
konfiguracja prowadzi do danego stanu końcowego, jeśli odpowiadające
temu faktowi stwierdzenie można udowodnić (wyprowadzić) w tym systemie
dowodzenia.
Tu oczywiście dobre określenie tej relacji nie budzi wątpliwości,
jeśli tylko wiemy, co to znaczy udowodnić stwierdzenie w danym
systemie dowodzenia.

Aktualna wersja na dzień 10:59, 29 wrz 2006

<<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ść

Z drugiej strony, możemy dosłownie potraktować terminologię "aksjomat", "reguła", itd. i myśleć o prezentacji semantyki naturalnej jako o formalnym systemie dowodzenia stwierdzeń postaci "dana konfiguracja prowadzi do danego stanu". Wówczas przyjmiemy, że system ten definiuje relację przejścia miedzy konfiguracjami i odpowiadającymi im stanami końcowymi poprzez meta-warunek: dana konfiguracja prowadzi do danego stanu końcowego, jeśli odpowiadające temu faktowi stwierdzenie można udowodnić (wyprowadzić) w tym systemie dowodzenia.

Tu oczywiście dobre określenie tej relacji nie budzi wątpliwości, jeśli tylko wiemy, co to znaczy udowodnić stwierdzenie w danym systemie dowodzenia.