# Level B CONSTRUCTING CORRECT PROGRAMS EXERCISES FOR THE LESSONS

Disclaimer: The programs below are not necessarily the "best" ones for the given specifications.

## Exercise 1: Array Sorting

### Specification 1

Given an integer-array A[1..N]
such that N >= 0 (1),
program sort modifies A
such that A[1..N] is the non-decreasingly ordered permutation of its original contents (2).

Examples: sort([3,1,2,3],[1,2,3,3]), sort([],[]).

Counter-example: sort([3,1,2,3],[1,2,3]).

### Program 1

K := N ;
while K <> 0 do
I := 1 ;
while K <> I do
order(A[I],A[I+1]) ;
I := I + 1
od ;
K := K - 1
od

Prove by computational induction that Program 1 is totally correct with respect to Specification 1, assuming that order(X,Y) exchanges the values of integers X and Y if X > Y.

## Exercise 2: Binary Search in an Ordered Array

### Specification 2

Given an integer-array A[1..N] and an integer E
such that N >= 0 (1) and A[1..N] is non-decreasingly ordered (2),
program ord-search returns an integer I
such that I is the smallest index in A[1..N] where A[I] >= E if it exists, and N+1 otherwise (3)
(in other words, I is the leftmost index in A[1..N] where E exists or where E should be inserted to preserve the ordering),
without modifying A[1..N] or E.

Examples:
ord-search([2,2,3,4,5,10,12], 1,1),
ord-search([2,2,3,4,5,10,12], 5,5),
ord-search([2,2,3,4,5,10,12],11,7),
ord-search([2,2,3,4,5,10,12],13,8) (note that N = 7 for each of these four examples),
ord-search([],5,1).

Construct by computational induction a program that is totally correct with respect to Specification 2, using the binary search principle.

## Exercise 3: Division by Subtraction

### Specification 3

Given two integers A and B
such that A >= 0 (1) and B > 0 (2),
program div returns two integers Q and R
such that Q is the quotient of the division of A by B, and R is the remainder of that division,
that is A = Q * B + R (3) and 0 <= R < B (4),
without modifying A or B.

Examples: div(22,5,4,2), div(22,11,2,0).

Counter-example: div(22,5,3,7).

### Program 3

Q := 0 ; R := A ;
while R >= B do
Q := Q + 1 ;
R := R - B
od

Prove by computational induction that Program 3 is totally correct with respect to Specification 3.

## Exercise 4: Moving the Maximum of an Array

### Specification 4

Given an integer-array A[1..N] and an integer K
such that 1 <= K <= N (1),
program moveMax modifies A[1..K]
such that A[1..K] is a permutation of its original contents (2) and A[K] = max(A[1..K]) (3),
without modifying A[K+1..N] or K.

Examples:
moveMax([3,2,1,4,5],3,[1,2,3,4,5]) or moveMax([3,2,1,4,5],3,[2,1,3,4,5]),
moveMax([2,1,3,4,5],2,[1,2,3,4,5])
(note that N = 5 for each of these two examples).

### Program 4

I := 1 ;
while K <> I do
order(A[I],A[I+1]) ;
I := I + 1
od

Prove by computational induction that Program 4 is totally correct with respect to Specification 4, assuming that order(X,Y) exchanges the values of integers X and Y if X > Y.

## Exercise 5: Sequential Search in an Array

### Specification 5

Given an integer-array A[1..N] and an integer E
such that N >= 0 (1),
program search returns an integer P
such that P is the smallest index in A[1..N] where A[P] = E if it exists, and N+1 otherwise (2),
without modifying A[1..N] or E.

Examples:
search([4,1,3,4],1,2),
search([4,1,3,4],2,5),
search([4,1,3,4],3,3),
search([4,1,3,4],4,1) (note that N = 4 for each of these four examples),
search([],5,1).

Counter-example: search([4,1,3,4],4,4).

Construct by computational induction a program that is totally correct with respect to Specification 5, using sequential search.

## Exercise 6: Array Compression

### Specification 6

Given an integer-array A[1..N]
such that N >= 1 (1) and A[1..N] is non-decreasingly ordered (2),
program compress returns an integer-array B[1..N] and an integer M
such that B[1..M] has all the elements of the set {A[1],...,A[N]} (3) and B[1..M] is increasingly ordered (4),
without modifying A[1..N].

Example: compress([1,2,2,2,3,3,7],[1,2,3,7,?,?,?],4).

Construct by computational induction a program that is totally correct with respect to Specification 6.

## Exercise 7: Array Partitioning

### Specification 7

Definition: An integer-array A[L..U] is zero-partitioned if its negative elements constitute a prefix and its non-negative elements constitute the corresponding suffix of A[L..U].
Examples: [-2,-1,0,3], [-2,-1,3,0], [-1,-2,0,3], [-1,-2,3,0].
Counter-example: [-1,0,-2,3].

Given an integer-array A[1..N]
program part0 modifies A[1..N]
such that A[1..N] is a zero-partitioned permutation of its original contents (1).

Examples: part0([],[]),
part0([-2,3,0,-1],[-2,-1,0,3])
or part0([-2,3,0,-1],[-2,-1,3,0])
or part0([-2,3,0,-1],[-1,-2,0,3])
or part0([-2,3,0,-1],[-1,-2,3,0]).

Counter-example: part0([-2,3,0,-1],[-1,0,-2,3]).

### Program 7

I :=1 ; J := N ;
while I < J do
if A[I] < 0 then
I := I + 1
else
swap(A[I],A[J]) ;
J := J - 1
fi
od

Prove by structural induction that Program 7 is totally correct with respect to Specification 7, assuming that swap(X,Y) exchanges the values of integers X and Y.

## Exercise 8: Binary Search in an Ordered Array

### Specification 8 = Specification 2

Construct by structural induction a program that is totally correct with respect to Specification 8, using the binary search principle.

## Exercise 9: Permutation Inversion

### Specification 9

Given an integer-array A[1..N]
such that A[1..N] is a permutation of 1..N (1),
program permInvert returns an integer-array B[1..N]
such that for every J in 1..N, we have B[A[J]] = J (2)
(in other words, B[1..N] is the inverse permutation of A[1..N]),
without modifying A[1..N].

Examples: permInvert([5,1,3,2,4],[2,4,3,5,1]), permInvert([],[]).

Counter-example: permInvert([5,1,3,2,4],[4,2,3,1,5]).

### Program 9

I := 0 ;
while I < N do
I := I + 1 ;
B[A[I]] := I
od

Prove by structural induction that Program 9 is totally correct with respect to Specification 9.

## Exercise 10: Indian Power

### Specification 10

Given two integers X and Y
such that X = x0 >= 0 (1) and Y = y0 >= 0 (2),
program power returns an integer Z
such that Z is x0 to the power of y0, that is Z = x0 ^ y0 (3).

Examples: power(2,3,8), power(3,2,9), power(0,0,1).

Counter-examples: power(2,3,4), power(2,3,6).

### Program 10

Z := 1 ;
while Y <> 0 do
if odd(Y) then
Z := Z * X
fi ;
X := X * X ;
Y := Y div 2
od

Prove by structural induction that Program 10 is totally correct with respect to Specification 10, assuming that odd(A) returns true if integer A is odd, and assuming that A div B returns the integer quotient of the division of integer A by integer B.

## Exercise 11: Finding an Increasing Slope in an Array

### Specification 11

Given an integer-array A[1..N]
such that A[1] < A[N] (1),
program findSlope returns an integer I
such that A[I] < A[I+1] (2),
without modifying A[1..N].

Example: findSlope([5,3,2,4,7,1,22],3) or findSlope([5,3,2,4,7,1,22],4) or findSlope([5,3,2,4,7,1,22],6).

Counter-examples: findSlope([5,3,2,4,7,1,22],5), findSlope([5,3,2,4,7,1,22],7).

Construct by structural induction a program that is totally correct with respect to Specification 11, using the binary search principle.

## Exercise 12: Decimal Representation of an Integer

### Specification 12

Given two integers M and N
such that M = m0 >= 0 (1) and the decimal representation of m0 has at most N digits (2),
program decRepr returns an integer-array A[1..N]
such that A[1..N] is the right-aligned decimal representation of m0, with leading zeroes (3),
without modifying N.

Examples: decRepr( 0,3,[0,0,0]), decRepr(522,7,[0,0,0,0,5,2,2]).

Counter-examples: decRepr(522,7,[5,2,2,0,0,0,0]), decRepr(522,7,[?,?,?,?,5,2,2]).