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 }