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 }