CSE503, Software Engineering
Spring 1996
D. Notkin
Assignment #5
2 May 1996
Due: 16 May 1996

1. Verify the following program:

   {x > 0 and y > 0}
   div := 0;
   rem := x;
   while rem >= y do
       div := div + 1;
       rem := rem - y;
   end;
   {x = div * y + rem and 0 <= rem < y}
   

2. The departmental Sun's have a program called tcov, which provides some support for whitebox testing. There is a man page for tcov. The code for agrep, a version of grep, is found on the Sun's in /uns/src/agrep2.04. Write 50 test cases that, using tcov, cover as many of agrep's statements as you can.

3. Identify two weaknesses of your test set.