postcondition R and invariant P shown below. Note how P is R with the last con-
straint n<2 k+1 remove:
R: 1 ≤ 2 k ≤n<2 k+1
P: 1 ≤ 2k ≤ n
E4. Write a loop to calculate the quotient q and remainder r when x≥0 ) is divid-
ed by y(>0 ), using just addition and subtraction (no multiplication or division).
The four variables are related by this formula:
x / y = q + r / y where 0≤r<y
i.e. x = y * q + r where 0≤r<y
Use the loop invariant P:
P: x = y * q + r* and 0≤r
which arises from the formula by deleting the constraint r<y .
E5. Given is x>0 and y>0, both integers. Find the greatest common divisor of
x and y, written as x gcd y . This is the largest integer that divides both. Use these
properties of gcd:
x gcd y = (x-y) gcd y
x gcd y = x gcd (y-x)
x gcd x = x
Use two fresh variables b and c and the following postcondition and invariant:
R: b = x gcd y
P: b gcd c = x gcd y
E6. Write code to delete all the vowels in String t . Here is the outline:
StringBuffer s= new StringBuffer(t);
Delete the vowels in s .
Answer the four loopy questions to develop the loop using the following invari-
ant and postcondition:
invariant: s[0..k-1] contains no vowels and k != s.length() .
// postcondition R: s[0..s.length()-1] contains no vowels
Hint: Use StringBuffer method deleteCharAt . Also, be wary of your
increment: you can make progress in two different ways.
E7. Deoxyribonucleic acid, or DNA for short, is the building block of all life.
Each strand of DNA consists of two strings of bases twisted together to form a
double helix. There are four bases, which are represented by the letters G, A, T
and C. In a double helix, the letters A and T bond together, as do the letters C and
G. The two sequences in a helix, then, are complements of each other. For exam-