V programu imamo nekje zanko.
Zancna invarjanta je neka izjava, tako da so pravilne trditve:
-iz pogojev pred vstopom v zanoko sledi ta invarijanta
-po iteraciji zanke iz zancne invariante se vedno sledi stavcna invarjanta
-iz stavcne invarjante sledi naprej koncni pogoj.
Recimo ce imas program:
int i=preberiOdUprorabnika()
int k=0;
int j=0;
do
{
k=k+1;
j=j+i;
}while (k<=i);
Vhodni pogoj: i>0;
Izhodni pogoj: j=k*(k-1)/2
Stavcna invarjanta je: j=k*(k-1)/2 in k <i in j >=0
Kako naj jo najdem?
Ta program racuna vsoto naravnih stevil od 1 pa do i.
Racuna ga tako, da zacne najprej z najmanjsim stevilom in mu pristeva vecje in
manjse dokler ne pristeje se i.
j je pa vsota stevil od 1 do k. Zato ker j-u program v vsaki iteraciji zanke
pristeje za 1 vecje stevilo, zacne pa z 1.
Zakaj pravim da je k<i?
Zato ker je pogoj na koncu po pristetju 1 za ponovitev zanke k<=i.
Zakaj j >0?
Zato ker vidim da se zmeraj pristeva pozitivno stevilo.
Upam da ti bo tole kaj pomagalo.
Marko
"..." <[EMAIL PROTECTED]> wrote: Morda tole vsaj malo pomaga:
http://en.wikipedia.org/wiki/Loop_invariant
lp
----- Original Message -----
From: "Sara"
To: "FRIClist"
Sent: Thursday, August 24, 2006 9:36 PM
Subject: [Friclist] PPJ
>
> A ma kdo zapiske od PPJ od dokazovanja pravilnosti in vstavljivosti
> programov? pa ce lahko poskenira in poslje na listo :)
> Cene ve kdo kaj je zancna invarianta??
>
> Lp
> Sara
>
>
---------------------------------
How low will we go? Check out Yahoo! Messengers low PC-to-Phone call rates.
