SW wykład 10 - Slajd15

<<powrót do strony wykładu

Poprawność programów i weryfikacja Poprawność programów Dowodzenie poprawności Wyspecyfikowany program Logika Hoare'a Definicje formalne Definicje formalne, c.d. Semantyka logiki Hoare'a Reguły wnioskowania Przykład dowodu Przykład dowodu, c.d. Niezmiennik pętli Przykład dowodu, c.d. W pełni wyspecyfikowany program Teorie pierwszego rzędu

Warto jednak uświadomić sobie, że w dowodach częściowej poprawności programów w rachunku dowodowym zadanym regułami logiki Hoare'a, musimy poza te reguły wychodzić i posługiwać się twierdzeniami o wartościach, na których nasze programu operują. Dla naszego języka TINY chodzi tu po prostu o liczby całkowite z wykorzystywanymi w języku operacjami arytmetycznymi (stałe liczbowe oraz dodawanie, odejmowanie i mnożenie) i predykatami (nierówność). Twierdzenia o tym "typie danych" mogą być wykorzystywane w dowodach przy stosowaniu reguły wynikania. Co więcej, na ogół nie możemy się bez nich obejść: przypomnijmy szereg trywialnych operacji przekształcania formuł w powyższym przykładzie i przynajmniej jedną nietrywialną, korzystającą ze wzoru na kwadrat sumy liczb.

Tak więc wszelkie dowody prowadzone w systemie dowodzenia zadanym podanymi regułami logiki Hoare'a, w tym dowód w powyższym przykładzie, wyprowadzają stwierdzenia o częściowej poprawności programów w języku TINY względem podanych warunków wstępnego i końcowego ze zbioru wszystkich formuł prawdziwych w modelu liczb całkowitych z wykorzystywanymi w tym języku operacjami i predykatami. Zbiór ten nazywać będziemy teorią modelu danych naszego języka.