Rotating a linear array

Rotating a linear array

In the following, $X$ and $Y$ will stand for string constants, $A, B, C, D$ and the linear array $f(i:0 \leq i < N)$ will stand for string variables, and concatenation will be denoted by just juxtaposition; $# X$ denotes the length of string $X$ . We are given the functional speci-

[\left| {N,K : \operatorname{int}{ 0 < K < N} }\right| ] $\therefore \mathbb{I}\left\lbrack {f\left( {i : 0 \leq i < N}\right) : \text{array}}\right\rbrack$

11

1

$$ \begin{array}{l} {f = X Y \wedge # X = K } \ ; R o t \ {f = Y X } \ \end{array} $$

What do we know about concatenation of strings? Well, that it is associative - i.e. $(AB)C = A(BC)$ and that it has the empty string, which we denote by $\varnothing$ , as identity element, -i.e. $A\varnothing = A \land \varnothing A = A$ .

The knowledge of the identity element is of im- portance because it enables us to insert into the postcondition a constant, which we can then replace by a variable, $B$ say. Without destruction of the symmetry between left and right we can re-write the postcondition as $f = Y\varnothing X$ and head for the invariant $f = YBx$ . But that won't do on account of the precondition. So what about

$$ E W D 9 4 1 - 1 $$

two more variables $A$ and $C$ ? With $f = {ABC}$ we can characterize the postcondition by $\left( {A,B,C}\right) = \left( {Y,\phi ,X}\right)$ and the precondition by $\left( {A,B,C}\right) = \left( {X,\phi ,Y}\right)$ . But this won't do the job either, because it would mean that the variable that replaced the constant in the postcondition has to be initialized with its final value!

That one empty string inserted in the postcondition did not give us enough freedom, but we are getting close because, again without destruction of the symmetry between left and right, two empty strings can be inserted in two different ways, "in between" and "around". That is, if we rewrite the postcondition as $f = Y \phi \phi X$ , we could rewrite the precondition as $f = \phi XY \phi$ . With

$$ P O: \quad f = A B C D $$

we would have to transform

$$ (A, B, C, D) = (\phi , X, Y, \phi) \quad (0) $$

$$ \mathrm {i n t o} \quad (A, B, C, D) = (Y, \phi , \phi , X) \tag {1} $$

Remark 0 Alternatively, we could have transformed

$$ (A, B, C, D) = (X, \phi , \phi , Y) $$

$$ \mathrm {i n t o} \quad (A, B, C, D) = (\phi , Y, X, \phi) $$

Our analysis so far gives no reason for strong preference. In our choice, we have upon completion $BC = \phi$ , the alternative would have AD = φ. In contrast to the string BC, the string AD

is not a substring of $f$ , the array the manipula-tions on which will eventually make up the algorithm. This is a reason for preferring the transition from (0) to (1). (End of Remark 0.)

Having chosen our initial and our final state, what would now be our invariant? A reasonable suggestion is

${P}_{1} : \;{AC} = Y\; \land {BD} = X$

Remark 1 There is the alternative

$$ C A = Y \wedge D B = X $$

that we shall look at later. We have chosen to in- vestigate Pi first because in it the concatenations occur in the order in which the strings occur in $f$ -see ${P}_{0} - .\left( {{End}\;{Remark}}\right)$ .

Let us now look for simple multiple assign- ment statements that reduce $# .\left( {CB}\right)$ under invariance of ${P}_{1}$ . The most effective one reduces $# .\left( {CB}\right)$ to zero at one fell swoop :

So: $A, C, B, D \coloneqq (A C), \phi, \phi, (B D)$ Let $f\left( = \text{front}\right)$ and $r\left( = \text{rear}\right)$ be used to denote the partitioning of a string such that $\left( {{f}{0}Z\;{r}{1}Z}\right) = Z$ for any string ${Z}^{y}$ . Then ${P}{1}$ is maintained by the assignment statements S1: $A,C\because \left( {A,f,c}\right) ,r.C$ $\mathbf{S}{2}$ ： $\mathbf{B},\mathbf{D}:= f_{\cdot}\mathbf{B},(r_{\cdot}\mathbf{B},\mathbf{D})$

The above statements, designed so as to maintain $\mathcal{P}$

[{P}_{0} : \;P = {ABCD}]

by manipulating $p$ and we now try,for reasons of efficiency,to confine those manipulations to swaps of disjoint array segments of equal length. To this purpose we investigate for our statements the weakest precondition with respect to $P_0$ .

(50) $\omega = \left( {{So},{P}_{0}}\right)$

$$ \begin{array}{l} = \left{ \begin{array}{l l} A x i o m o f A s s i g n m e n t 3 \ f = (A C) \phi \phi (B D) \end{array} \right. \ = {\mathrm {P r o p e r i e s o f C o n c a t e n a t i o n} } \ \end{array} $$

which, thanks to the initial validity of $P$ o can be achieved by swapping $B$ and $C$ . As we had decided to restrict swaps to array segments of equal length, for $# .B = # .C$ we are done.

$\left( {S}{1}\right) = {wp}\left( {{S}{1},{P}_{0}}\right)$

$$ = {A s s i g n m e n t a n d C o n c a t e n a t i o n } $$

which, thanks to the initial validity of $P_0$ , i.e.

$$ f = A B F C R C D $$

can be achieved by swapping $B$ and ${f}_{C}$ . The constraint $# .B = # \left( {P.C}\right)$ can be met if $# .B < # C$ .

$\left( {S}{2}\right) = {wp}\left( {{S}{2},{P}_{0}}\right)$

$$ = {A f B C r B D $$

$$ E W D 9 4 1 - 4 $$

which, thanks to the initial validity of $P_0$ , i.e.

$$ f = A f. B r. B C D $$

can be achieved by swapping $r.B$ and $C$ . The constrain of $# .\left( {r,B}\right) = # .C$ can be met if $# .B > # .C$

In terms of $A,B,C$ ,and $D$ this leads to

$A,B,C,D \mathrel{\text{:=}} \phi ,X,Y,\phi \;\left{ {# .B \geq 1 \land # .C \geq 1}\right}$

$$ \begin{array}{l} ; \underline {{\underline {{d o}}}} #. B < #. C \rightarrow S _ {1} \quad \square #. B > #. C \rightarrow S _ {2} \ ; \frac {o d}{s o} \ \end{array} $$

with the representational convention

$$ \begin{array}{l} A = f (i: 0 \leq i < k - b) \ B = f (i: k - b \leq i < k) \ c = f (i: k \leq i < k + c) \ D = p (i: k + c \leq i < N) \ \end{array} $$

we thus find for Rot

$$ \llbracket b, c, k: i n t; b, c, k := K, N - K, K $$

$$ \begin{array}{l} ; \underline {{d o}} b < c \rightarrow f: s e g s w a p. (k - b). k. b; k, c := k + b, c - b \ \mathrm {I I} b > c \rightarrow f: \mathrm {s e g s w a p}. (k - c). k. c; k, b := k - b, b - c \ \end{array} $$

$$ \begin{array}{l} \underline {{o d}} \ f: \mathrm {s e g s w a p}. (k - b). k. c \ \end{array} $$

$$ 3 1 $$

in which $f$ : segswap. x.y.z swaps the array segments

It looks as if we can now safely discard the sug- gestion of Remark 1 . The analogues to S0, S1, and S2 are straightforward enough, but the analysis of the requirement to maintain Po leads to manipula-tions of f , wilder than what the whole program is supposed to achieve.

A closer analysis of our solution reveals a curiosity. We have used that our postcondition $f = YX$ is implied by $P_0 \wedge P_1 \wedge BC = \phi$ but it is in fact implied by the weaker $P_0 \wedge P_1 \wedge (B = \phi \vee C = \phi)$ , the computation can already terminate as soon as one of the two is empty. An unexploitable feature as $B$ and $C$ turn empty simultaneously. The observation raises the question whether we can replace $P_1$ by a weaker invariant such that the last conjunct $BC = \phi$ is not stronger than necessary. A weaker $P_2$ would be

which, yet would be strong enough since

$$ \begin{array}{l} P _ {2}: \quad A C B D = Y X \ P _ {0} \wedge P _ {2} \wedge B C = \phi \ = {\text {d e f i n i t i o n s a n d c o n c a t e n a t i o n} } \ f = A B C D \wedge A C B D = Y X \wedge (B = \phi \wedge C = \phi) \ \Rightarrow^ {\prime} {L e i b n i z } \ f = A \phi \phi D \land A \phi \phi D = Y X \quad (\mathrm {N o t e :} V \mathrm {i n s t e a d o f} \land \ \Rightarrow {L e i b o n i z } \ f = Y X \ \end{array} $$

So maintains $P2$ as well as it maintains $P1$ , and I propose to keep it for dealing with the case that $# B = # C$ . But gives the weaker $P2$ freedom to replace $S1$ and $S2$ ? Let us try.

${P}_{2}$ is maintained by

S3: $A,C,B = \left( {AC}\right) ,f.B,r.B$ S4: $C,B,D = f.c,r.c,(B - D)$

which decrease #. (BC) by #.c and #.b respectively. We investigate as before their weakest pre- conditions with respect to ${P}_{0}$

$\left( {S}{3}\right) \;{wp}\left( {{S}{3},{P}_{0}}\right)$

$$ f = A C r. B f. B D $$

which, thanks to the initial validity of $P_0$ , i.e.

$$ f = A f. B r. B C D $$

can be obtained by swapping $f.B$ and $C$ ; S3 is applicable with $# .B > # .C$

(S4) ${wp}\left( {{S}{3},{P}{0}}\right)$

$$ = {\mathrm {A s s i g n m e n t a n d C o n c a t e n a t i o n} } $$

which, thanks to the initial validity of $P_0$ , i.e.

$$ f = A B P C R C D $$

can be obtained by swapping B and r.c ; s4 is applicable with #B < #C

Coding with the same representational convention as before we discover that k's initialization is the only assignment to k ; hence that variable is not needed and ,therefore, another solution for Rot is

$$ \llbracket b, c: \mathrm {i n t}; b, c := K, N - K $$

$$ \begin{array}{l} ; \underline {{d o}} b > c \rightarrow f: s e g s w a p. (K - b). K. c; b := b - c \ \mathrm {I I} b < c \rightarrow f: \operatorname {s e g s w a p}. (k - b). (k + c - b). b; c := c - b \ \end{array} $$

$$ \underline {{o d}} $$

$$ \begin{array}{l} ; f: s e g s w a p. (k - b). k. c \ \rbrack \ \end{array} $$

Note We only bothered to define $f$ : segswap. $x.y.z$ for natural $z$ . Had we extended for negative $z$ a swap of the array segments $f\left( {i : x + 2 \leq i < x}\right)$ and $f\left( {i : y + z \leq i < y}\right)$ ,then the last guarded command would have been

$$ b < c \rightarrow f: s e g s w a p. K. (K + c). (- b); c := c - b $$

It is probably proper to define $f$ : segswap. x.y.z

$$ \begin{array}{l} f (i: (x \min x + z) \leq i < (x \max x + z)) a n d \ f (i: (y \min y + 2) \leq i < (y \max y + 2)). \ \end{array} $$

(End of Note.)

We still have the suggestion of Remark 0. We could explore the invariant $P_0 \wedge P_3$ with

$$ P _ {3}: \quad A C = X \quad \wedge B D = Y $$

and now our target is to get $A = \phi \land D = \phi$ The situation is discouragingly different from that with the invariant P0 P1 , where the postcondition was already implied if either B= or C= φ . Further exploration shows that we do run

into trouble and that the suggestion of Remark 0 is not to be recommended. This is not surprising. Swapping two disjoint array segments is its own inverse, and Remark 0 in essence suggests to invert one of our earlier solutions (in the sense of playing them backwards). The earlier solutions perform on b and c Euclid's algorithm for the gcd(N,K) and inversion of Euclid's algorithm is not an attractive proposal. Hence we discard the sug- gestion of Remark 0 .

Concatenation is a simple dyadic operator on strings, nicely associative and all that. There is also a simple monadic operator on strings, nice because it is its own inverse, viz. the reverse of a string: if $# .2 \leq 1$ . rev. $Z = Z$ ,and furthermore $\operatorname{rev}.\left( {XY}\right) = \operatorname{rev}.Y$ rev. $X$

$$ \text {o r} \quad \operatorname {r e v}. (\operatorname {r e v}. X \operatorname {r e v}. Y) = Y X $$

which yields a very different solution for $R$ or

$$ 1 1 i, j: \mathrm {i n t} $$

$$ \begin{array}{l} i, j := 0, k - 1; \underline {{d o}} i < j \rightarrow f: s w a p. i. j; i, j := i + 1, j - 1 \underline {{o d}} \ i, j := K, N - 1; \underline {{d o}} i < j \rightarrow f: s w a p. i. j; i, j := i + 1, j - 1 \underline {{o d d}} \ i, j := 0, N - 1; d o i < j \rightarrow f: s w a p. i. j; i, j := i + 1, j - 1 o d \ \mathfrak {I} \ \end{array} $$

where $f$ : swap.ij interchanges the values of ${f}_{i}$ and

EWD941-9

For Rot we could have given the -equivalent-

$$ \begin{array}{l} \left| \left[ N, K: i n t {0 < K < N } \right. \right. \ ; \quad \left{\left(\underline {{A}} i: 0 \leq i < N: f _ {i} = F _ {i}\right) \right} \ ; R o t \ {(A i: 0 \leq i < N: f _ {i} = F _ {i} ((i + k) \mod N)) } \ \rbrack \rbrack \ \end{array} $$

J1

It is possible to develop all the above algorithms without the introduction of string variables, i.e. carrying out the whole derivation in terms of universally quantified equalities between elements of $f$ and of $F$ , as in the above functional specification. When you try it, you will discover that the exercise is an obfuscating pain in the neck. Had we started from the above functional specification, the invention of $X$ and $Y$ would probably have been our first duty.

(The above specification has often lead to yet another solution for Rot in which the required permutation is written as the product of cyclic permutations. In order to determine those, gcd(N,k) has to be computed.)

Austin, 28 September 1985

prop. dr. Edsger W. Dgiksha Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188, USA