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

Task 1

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).

Task 2

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

Task 3

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

Task 4

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).

Task 5

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).

Task 6

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

Task 7

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

Task 8

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

Task 9

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

Task 10

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).

Task 11

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]).

Task 12

Construct by structural induction a program that is totally correct with respect to Specification 12.


(Back) To Pierre Flener's homepage.

Last updated 17 March 2000.