Witam , mam pewne zadanie do rozwiązania :X proszę o pomoc : (
Przeprowadzić dowód poprawności częściowej następującego programu:
ALFA :{n => 1}
x: =1; y:=0;
while x<n do
y:=y+ 2x;
x:= x+1
{y=2 ( n(n+1)/2 ) }
Z tego co wiem , mamy warunek początkowy(alfa) i warunek końcowy(beta) . Warunek poczatkowy musi sie zgadzac ,aby zachodziła poprawnosc czesciowa.
a więc:
Warunek alfa (n=>1) , X=1 , a warunek w pętli to x<n => 1<1 - FALSE
Proszę o pomoc : )!!