Quotient and remainder: proof

c go java js lua py vbs rkt scm pro

Consider the following C code that you are to prove correct, given the loop invariant inv.

int q1 = 0; int r1 = a1; while (r1 >= d1) { q1 = q1 + 1; r1 = r1 - d1; }

Here is the code in a C program. Here is the C code.

#include <stdio.h>

void process(int a1, int d1) {
	printf("before: a1=%d d1=%d\n",a1,d1);
	// begin here
	int q1 = 0;
	int r1 = a1;
	while (r1 >= d1) {
		q1 = q1 + 1;
		r1 = r1 - d1;
		}
	// end here
	printf("after: q1=%d r1=%d\n",q1,r1);
	printf("\n");
	}

int main() {
	// What does the routine process do?
	process(25,7);
	process(18,5);
	process(33,6);
	return 0;
	}

Here is the output of the C code.

before: a1=25 d1=7
after: q1=3 r1=4

before: a1=18 d1=5
after: q1=3 r1=3

before: a1=33 d1=6
after: q1=5 r1=3

Below are the proof steps for the above code fragment.

The pre and post conditions and the loop invariant(s) are provided.

To provide continuity between the parts, all of the required proof lines are included in all steps and filled in from step to step. Step 1. given pre and post conditions and invariant

// 1:{ pre: a1 >= 0 and d1 > 0 }

// 5c:

// 5b:

// 5a:

int q1 = 0;

// 4:

int r1 = a1;

// 1:{ inv: (a1 = q1*d1+r1) and (r1 >= 0) }

while (r1 >= d1) {

// 2:

// 3:

// 8c:

// 8b:

// 8a:

q1 = q1 + 1;

// 7:

r1 = r1 - d1;

// 2:

}

// 2:

// 3:

// 6:

// 1:{ post: a1=q1*d1+r1 and r1=0..d1-1}

Step 2. copy invariant to begin and end of loop body and after loop

// 1:{ pre: a1 >= 0 and d1 > 0 }

// 5c:

// 5b:

// 5a:

int q1 = 0;

// 4:

int r1 = a1;

// 1:{ inv: (a1 = q1*d1+r1) and (r1 >= 0) }

while (r1 >= d1) {

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:

// 8c:

// 8b:

// 8a:

q1 = q1 + 1;

// 7:

r1 = r1 - d1;

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

}

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:

// 6:

// 1:{ post: a1=q1*d1+r1 and r1=0..d1-1}

Step 3. copy loop condition and negated loop condition

// 1:{ pre: a1 >= 0 and d1 > 0 }

// 5c:

// 5b:

// 5a:

int q1 = 0;

// 4:

int r1 = a1;

// 1:{ inv: (a1 = q1*d1+r1) and (r1 >= 0) }

while (r1 >= d1) {

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ r1 >= d1 }

// 8c:

// 8b:

// 8a:

q1 = q1 + 1;

// 7:

r1 = r1 - d1;

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

}

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ ! (r1 >= d1) => r1 < d1 }

// 6:

// 1:{ post: a1=q1*d1+r1 and r1=0..d1-1}

Step 4. work from begin of loop backwards to pre-condition

// 1:{ pre: a1 >= 0 and d1 > 0 }

// 5c:

// 5b:

// 5a:

int q1 = 0;

// 4:{ a1 = q1*d1+a1 and a1 >= 0}

int r1 = a1;

// 1:{ inv: (a1 = q1*d1+r1) and (r1 >= 0) }

while (r1 >= d1) {

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ r1 >= d1 }

// 8c:

// 8b:

// 8a:

q1 = q1 + 1;

// 7:

r1 = r1 - d1;

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

}

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ ! (r1 >= d1) => r1 < d1 }

// 6:

// 1:{ post: a1=q1*d1+r1 and r1=0..d1-1}

Step 5. work backwards to pre-condition (no contradictions)

// 1:{ pre: a1 >= 0 and d1 > 0 }

// 5c:{ a1 >= 0}

// 5b:{ a1 = a1 and a1 >= 0}

// 5a:{ a1 = 0*d1+a1 and a1 >= 0}

int q1 = 0;

// 4:{ a1 = q1*d1+a1 and a1 >= 0}

int r1 = a1;

// 1:{ inv: (a1 = q1*d1+r1) and (r1 >= 0) }

while (r1 >= d1) {

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ r1 >= d1 }

// 8c:

// 8b:

// 8a:

q1 = q1 + 1;

// 7:

r1 = r1 - d1;

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

}

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ ! (r1 >= d1) => r1 < d1 }

// 6:

// 1:{ post: a1=q1*d1+r1 and r1=0..d1-1}

Step 6. work from end of loop forwards to post-condition (post-conditions achieved)

// 1:{ pre: a1 >= 0 and d1 > 0 }

// 5c:{ a1 >= 0}

// 5b:{ a1 = a1 and a1 >= 0}

// 5a:{ a1 = 0*d1+a1 and a1 >= 0}

int q1 = 0;

// 4:{ a1 = q1*d1+a1 and a1 >= 0}

int r1 = a1;

// 1:{ inv: (a1 = q1*d1+r1) and (r1 >= 0) }

while (r1 >= d1) {

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ r1 >= d1 }

// 8c:

// 8b:

// 8a:

q1 = q1 + 1;

// 7:

r1 = r1 - d1;

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

}

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ ! (r1 >= d1) => r1 < d1 }

// 6:{ (a1 = q1*d1+r1) and (r1 >= 0) and r1 < d1 }

// 1:{ post: a1=q1*d1+r1 and r1=0..d1-1}

Step 7. work from end of loop body backwards towards begin of loop body

// 1:{ pre: a1 >= 0 and d1 > 0 }

// 5c:{ a1 >= 0}

// 5b:{ a1 = a1 and a1 >= 0}

// 5a:{ a1 = 0*d1+a1 and a1 >= 0}

int q1 = 0;

// 4:{ a1 = q1*d1+a1 and a1 >= 0}

int r1 = a1;

// 1:{ inv: (a1 = q1*d1+r1) and (r1 >= 0) }

while (r1 >= d1) {

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ r1 >= d1 }

// 8c:

// 8b:

// 8a:

q1 = q1 + 1;

// 7:{ a1 = q1*d1+(r1-d1) and ((r1-d1) >= 0) }

r1 = r1 - d1;

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

}

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ ! (r1 >= d1) => r1 < d1 }

// 6:{ (a1 = q1*d1+r1) and (r1 >= 0) and r1 < d1 }

// 1:{ post: a1=q1*d1+r1 and r1=0..d1-1}

Step 8. work backwards to begin of loop body (no contradictions)

// 1:{ pre: a1 >= 0 and d1 > 0 }

// 5c:{ a1 >= 0}

// 5b:{ a1 = a1 and a1 >= 0}

// 5a:{ a1 = 0*d1+a1 and a1 >= 0}

int q1 = 0;

// 4:{ a1 = q1*d1+a1 and a1 >= 0}

int r1 = a1;

// 1:{ inv: (a1 = q1*d1+r1) and (r1 >= 0) }

while (r1 >= d1) {

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ r1 >= d1 }

// 8c:{ a1 = (q1*d1 + r1 and (r1 >= d1) }

// 8b:{ a1 = (q1*d1 + d1 + r1 - d1 and (r1 >= d1) }

// 8a:{ a1 = (q1+1)*d1+(r1-d1) and ((r1 >= d1) }

q1 = q1 + 1;

// 7:{ a1 = q1*d1+(r1-d1) and ((r1-d1) >= 0) }

r1 = r1 - d1;

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

}

// 2:{ (a1 = q1*d1+r1) and (r1 >= 0) }

// 3:{ ! (r1 >= d1) => r1 < d1 }

// 6:{ (a1 = q1*d1+r1) and (r1 >= 0) and r1 < d1 }

// 1:{ post: a1=q1*d1+r1 and r1=0..d1-1}

Once the pre-conditions are met with no contradictions and the post conditions are met and the loop invariant(s) completed with no contradictions, the partial correctness proof is complete.

To show total correctness (omitted) one must show partial correctness (above) and some progress towards the goal for each loop at each step so that the loops and program fragment eventually complete.

The above has shown partial correctness - when the loop stops the goal is reached.

To informally show total correctness one observes (the math gets more involved) that progress is made towards the goal during each loop body iteration so that eventually the loop will stop.

Notice that we did not use d1 in the above partial correctness proof. The value of d1 is needed in the total correctness part of the proof. In particular, if d1 is zero or less than zero, the loop will never stop.