Dany jest poniższy algorytm obliczajacy sume kwadratow pierwszych n liczb naturalnych dla ustalonej liczby naturalnej n.
int m,i,s;
read(m);
i:=1; s:=1;
while(i<=m){
s:=s+i*i;
i:=i+1;
}
print(s);
end;
W celu udowodnienia poprawności semantycznej algorytmu wykonaj poniższe polecenia.
- Zdefiniuj warunek początkowy alfa oraz warunek końcowy beta, potrzebne do dowodu semantycznej poprawności.
- Udowodnij własność częsciowej poprawnosci programu
- Udowodnij własność określoności programu
- Udowodnij własność stopu programu
Czy ktoś może mi rozwiązać to zadanie z opisem do każdego rozwiązywanego problemu?
