procedure MULT2(in x, y; out z): z=x×y
var a
begin
(1) y-y=0 arithm.
(2) 0=x×(y-y) 1 arithm.
z := 0;
(3) z=x×(y-y) 2 ASSIGN
a := y;
(4) z=x×(y-a) 3 ASSIGN
while -(a=0)
5 (5) -(a=0) A
6 (6) z=x×(y-a) A
6 (7) z+x=(x×(y-a))+x 6 arithm.
6 (8) z+x=x×((y-a)+1) 7 arithm.
5,6 (9) z+x=x×(y-(a-1)) 5,8 arithm.
z := z+x;
5,6 (10) z=x×(y-(a-1)) 9 ASSIGN
a := a-1
5,6 (11) z=x×(y-a) 10 ASSIGN
endwhile
(12) (z=x×(y-a)) & --(a=0) 4,5,6,11 WHILE
(13) z=x×(y-a) 12 &E
(14) --(a=0) 12 &E
(15) a=0 14 DN
(16) z=x×y 13,15 arithm.
end
procedure DIV(in x, y; out q, r): -(y=0) -> (((q×y)+r=x) & (r<y))
begin
1 (1) -(y=0) A
(2) (0×y)+x=x arithm.
q := 0;
(3) (q×y)+x=x 2 ASSIGN
r := x;
(4) (q×y)+r=x 3 ASSIGN
while r>=y
5 (5) r>=y A
6 (6) (q×y)+r=x A
5,6 (7) ((q×y)+y)+(r-y)=x 5,6 arithm.
5,6 (8) ((q+1)×y)+(r-y)=x 7 arithm.
q := q+1;
5,6 (9) (q×y)+(r-y)=x 8 ASSIGN
r := r-y
5,6 (10) (q×y)+r=x 9 ASSIGN
endwhile
(11) ((q×y)+r=x) & -(r>=y) 4,5,6,10 WHILE
(12) ((q×y)+r=x) & (r<y) 11 arithm.
1 (13) ((q×y)+r=x) & (r<y) 1,12 SI(S) P,Q |- Q
(14) -(y=0) -> (((q×y)+r=x) & (r<y)) 1,13 CP
end
procedure P(in x, y; out z): (x-y<=z) & (z<=x)
var q, r
begin
if y=0
then
1 (1) y=0 A
1 (2) (x-y<=x) & (x<=x) 1 arithm.
z := x
1 (3) (x-y<=z) & (z<=x) 2 ASSIGN
else
4 (4) -(y=0) A
call DIV(x, y; q, r);
(5) -(y=0) -> (((q×y)+r=x) & (r<y)) SI(S) DIV
call MULT2(q, y; z)
(6) z=q×y SI(S) MULT2
4 (7) ((q×y)+r=x) & (r<y) 4,5 MPP
4 (8) (q×y)+r=x 7 &E
4 (9) z+r=x 6,8 arithm.
4 (10) z<=x 9 arithm.
4 (11) r<y 7 &E
4 (12) x<=z+y 9,11 arithm.
4 (13) x-y<=z 12 arithm.
4 (14) (x-y<=z) & (z<=x) 10,13 &I
endif
(15) (x-y<=z) & (z<=x) 1,3,4,14 IF
end
procedure DIV(in x, y; out q, r): ((q×y)+r=x) & (r<y)?Is it totally correct with respect to this specification?
(2 points) An examination of the proof given in 1(b) shows that the assumption -(y=0) is not really used---it is only introduced at the bottom by the assumption-adding trick (one version of which is the indicated use of the sequent P,Q |- Q). Indeed, if the proof were terminated at line (12) then it would serve as a (partial) correctness proof for the modified specification; therefore, the code is partially correct.
The code is not totally correct because the specification no longer excludes the case where the input y is zero. Tracing the execution of the code for y=0 reveals that the test in the while statement will always be true, so the program will loop forever; therefore, although the program is partially correct, it is not totally correct.
procedure FAC(in x; out y): y=x!where x! is the usual factorial function, defined inductively by 0!=1 and (n+1)!=n!×(n+1). Also identify a termination expression which will support a total correctness proof for your code (you don't need to give the proof, just the expression).
(4 points, extra credit)
procedure FAC(in x; out y): y=x!
var a
begin
(1) 1×x!=x! arithm.
y := 1;
(2) y×x!=x! 1 ASSIGN
a := x;
(3) y×a!=x! 2 ASSIGN
while a>0
4 (4) a>0 A
5 (5) y×a!=x! A
4 (6) a!=a×(a-1)! 4 arithm.
4,5 (7) y×(a×(a-1)!)=x! 5,6 arithm.
4,5 (8) (y×a)×(a-1)!=x! 7 arithm.
y := y×a;
4,5 (9) y×(a-1)!=x! 8 ASSIGN
a := a-1
4,5 (10) y×a!=x! 9 ASSIGN
endwhile
(11) (y×a!=x!) & -(a>0) 3,4,5,10 WHILE
(12) y×a!=x! 11 &E
(13) -(a>0) 11 &E
(14) a=0 13 arithm.
(15) a!=1 14 arithm.
(16) y=x! 12,15 arithm.
end
A termination expression for the while loop is simply a, since at the beginning of each time through the body of the loop it is guaranteed to be greater than zero, and it will be strictly decreased (by one) by the end of the loop body.