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