Question 1-1

Prove the following using our axiomatic scheme.

{ i * k = n AND k mod 2 = 0 }
k := k / 2;
i := i * 2;
{i * k = n }

Solution

 
1.  i * k = n AND k mod 2 = 0 implies (i * 2) * (k / 2) = n (Math fact)

2.  { i * k = n AND k mod 2 = 0 }                           (Conseq: 1)
    { (i * 2) * (k / 2) = n }

3.  { (i * 2) * (k / 2) = n }                               (Assignment)
    k := k / 2;
    { (i * 2) * k = n }

4.  { i * k = n AND k mod 2 = 0 }                           (Seq: 2, 3)
    k := k / 2;
    { (i * 2) * k = n }

5.  { (i * 2) * k = n }                                     (Assignment)
    i := i * 2;
    {i * k = n }

6.  { i * k = n AND k mod 2 = 0 }                           (Seq: 4, 5)
    k := k / 2;
    i := i * 2;
    {i * k = n }

Back to Quiz 1