Oefenopgaven axiomatische semantiek

Halveringsalgoritme

Maak het bewijs af.

{ x=n ∧ n>0 }

	y := 0;

	while y < x-1
	do

		y := y + 1;

		x := x - 1


{ 2y ≤ n ∧ 2(y+1) > n }

Delingsalgoritme

Maak het bewijs af.

{ x=m ∧ y=n ∧ m≥0 ∧ n>0 }

	z := 0;

	while y≤x
	do


		z := z + 1;

		x := x - y


{ z=m div n ∧ x=m mod n }