Semantyka i weryfikacja programów 2014/15.
Zadanie 3.
Dany jest następujący program w języku TINY.
{n>0}
{ }
s:=0;
{ }
i:=1;
{ }
j:=n;
{ }
while {γ : }
i<j do (
{ }
s:=s+i+j;
{ }
i:=i+1;
{ }
j:=j-1;
{ }
)
{ }
{ }
if i=j then s:=s+i else skip;
{ }
w:=s+s-n;
{ }
{w = n2}
Udowodnij częściową poprawność programu względem podanej specyfikacji tj.
1. Podaj niezmiennik pętli γ.
2. Wstaw odpowiednie formuły w nawiasy {, } tak, aby powstałe anotacje umożliwiały przeprowadzenie dowodu częściowej poprawności. Jeśli w dwóch sąsiednich wierszach występują nawiasy {,}, to pomiędzy wstawionymi tam anotacjami powinna zachodzić implikacja. Można też dostawić dodatkowe nawiasy.
1
