Oefenopgaven axiomatische semantiek
Halveringsalgoritme
Maak het bewijs af.
{ x=n ∧ n>0 } { x+0=n ∧ n>0 } { x+0=n ∧ n>0 ∧ x>0 } { x+0=n ∧ n>0 ∧ x≥0 } { x+0=n ∧ n>0 ∧ 0≤x } y := 0; { x+y=n ∧ n>0 ∧ y≤x } while y < x-1 do { y<x-1 ∧ x+y=n ∧ n>0 ∧ y≤x } { y<x-1 ∧ x+y=n ∧ n>0 } { x+y=n ∧ n>0 ∧ y≤x-2 } { x+y=n ∧ n>0 ∧ y+1≤x-1 } { x-1+y+1=n ∧ n>0 ∧ y+1≤x-1 } y := y + 1; { x-1+y=n ∧ n>0 ∧ y≤x-1 } x := x - 1 { x+y=n ∧ n>0 ∧ y≤x } { ¬(y<x-1) ∧ x+y=n ∧ n>0 ∧ y≤x } { y≥x-1 ∧ x+y=n ∧ n>0 ∧ y≤x } { x-1≤y ∧ x+y=n ∧ n>0 ∧ y≤x } { x-1≤y ∧ x=n-y ∧ n>0 ∧ y≤x } { n-y-1≤y ∧ x=n-y ∧ n>0 ∧ y≤n-y } { n-y-1≤y ∧ x=n-y ∧ n>0 ∧ 2y≤n } { n≤2y+1 ∧ x=n-y ∧ n>0 ∧ 2y≤n } { n<2y+2 ∧ x=n-y ∧ n>0 ∧ 2y≤n } { n<2(y+1) ∧ x=n-y ∧ n>0 ∧ 2y≤n } { n<2(y+1) ∧ 2y≤n } { 2y≤n ∧ 2(y+1)>n }
Delingsalgoritme
Maak het bewijs af.
{ x=m ∧ y=n ∧ m≥0 ∧ n>0 } { x=m ∧ y=n ∧ m≥0 ∧ n>0 x≥0 } { 0+x=m ∧ y=n ∧ x≥=0 } { 0*n+x=m ∧ y=n ∧ x≥0 } z := 0; { z*n+x=m ∧ y=n ∧ x≥0 } while y≤x do { y≤x ∧ z*n+x=m ∧ y=n ∧ x≥0 } { y≤x ∧ (z+1)*n+x-n=m ∧ y=n ∧ x≥0 } { y≤x ∧ (z+1)*n+x-y=m ∧ y=n ∧ x≥0 } { y≤x ∧ (z+1)*n+x-y=m ∧ y=n ] { (z+1)*n+x-y=m ∧ y=n ∧ x≥y } { (z+1)*n+x-y=m ∧ y=n ∧ x-y≥0 } { (z+1)*n+x-y=m ∧ y=n ∧ x-y≥0 } z := z + 1; { z*n+x-y=m ∧ y=n ∧ x-y≥0 } x := x - y { z*n+x=m ∧ y=n ∧ x≥0 } { ¬(y≤x) ∧ z*n+x=m ∧ y=n ∧ x≥0 } { y>x ∧ z*n+x=m ∧ y=n ∧ x≥0 } { n>x ∧ z*n+x=m ∧ y=n ∧ x≥0 } { x<n ∧ z*n+x=m ∧ y=n ∧ x≥0 } { x<n ∧ z*n+x=m ∧ y=n ∧ 0≤x } { z*n+x=m ∧ y=n ∧ 0≤x ∧ x<n } { z*n+x=m ∧ 0≤x ∧x<n } { z=m div n ∧ x=m mod n }