Vraagstelling
post	:er_is = (Ei:p<=i<=q:i**2=z)
R	:er_is = (Ei:p<=i<=q:i**2=z)
I(k)	:er_is = (Ei:p<=i<=k:i**2=z)

Strategie

Formele probleemspecificatie
	pre: p=P ^ q=Q ^ z=Z ^ q>p
	post:er_is = (Ei:p<=i<=q:i**2=z)

* Eindrelatie
	R:er_is = (Ei:p<=i<=q:i**2=z)

* Invariant
	I(k):er_is = (Ei:p<=i<=k:i**2=z) ^ p-1<=k<=q

* Stopcriterium
	k==q v er_is

Initialisatie
	k=p-1;
	er_is = false;

Stap richting stopcriterium
	k++;

Actie herstel invariant
	er_is = (Ei:p<=i<=k-1:i**2=z) v (Ei:i=k:i**2=z)

Algoritme

public boolean worteltest(int p, int q, int z){
//pre: p=P ^ q=Q ^ z=Z ^ q>p
	int k=p-1;
	boolean er_is = false;
//P1: I(k) ^ k=p-1 ^ er_is = false <=> I(p-1)
	while(k!=q && !er_is){
//P2: I(k)
		k++;
//P3: I(k-1)
		er_is = (er_is || k*k==z);
//P4: I(k)
	}
//P5: I(k) ^ (k==q v er_is) -> R
	return er_is;
}