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