SW wykład 10 - Slajd4

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

Zajmować się tu będziemy jedną z najprostszych form specyfikacji programów: ich poprawnością względem podanych warunku wstępnego (założeń o danych wejściowych programu) i warunku końcowego (wymagań dotyczących jego wyników). Na początek rozpatrywać będziemy tzw. poprawność częściową (przy czym owa "częściowość" to tylko zwyczajowe określenie wykorzystywanej tu wersji pojęcia poprawności --- z pewnością nie chodzi tu o to, że program może być "częściowo poprawny, a częściowo nie"). Warunki wstępny i końcowy dla poprawności częściowej danego programu zapisywać będziemy jako formuły w nawiasach klamrowych przed i po programie, odpowiednio.

Na slajdzie podajemy prosty przykład programu (w najprostszej wersji języka TINY) i takiej jego właśnie specyfikacji, wymagającej częściowej poprawności względem podanych warunku wstępnego i końcowego. Tak zapisane stwierdzenie o poprawności programu, na razie nieco nieformalnie można odczytać jak w podwójnej ramce na dole slajdu.