For the record: Batcher’s Baffler

For the record: Batcher's Baffler

In this note we consider a special sorting routine for array $\rho \left( {i : 0 \leq i < N}\right)$ . The predicate ${OK}$ is given by ${OK}.{ij} \equiv {p}{i} < {p}{j}$

and in the following quantifications over it are im-. plicitly constrained by $0\leq i < j < N$ . The speci-. fication for Batcher's Baffler - the algorithm has been invented by K.E. Batcher and has been given this name by David Gries, presumably because he was baffled by it- is

$$ \mathrm {I I N : i n t} {N \geq 0 } $$

$$ ; \mathrm {I I} f (i: 0 \leq i < N) \mathrm {a r r a y o f i n t} {b a g. f = B } $$

$$ ; B a t c h e r s B a f p l e r $$

$$ {b a g. f = B \land (\underline {{A}} i: O K, i. (i + 1)) } $$

1

31

In the following we shall no longer mention the invariance of bag. $f = B$ ; it is trivially main- tained as the algorithm only interferes with the array $f$ with the operation

$$ \begin{array}{r l}{\mathrm {o r d . i . j}}&{= \underset {f} {\underset {\mathrm {i . j}} {\int}} 0 k. i. j \rightarrow s k i p}\&{\quad \int 1 0 k. i. j \rightarrow f: s w a p (i, j)}\&{\quad \underset {f} {\underset {\mathrm {i . j}} {\int}}}\end{array} $$

There are all sorts of ways of expressing our postcondition that $f$ is ascending, but this one is a nice starting point for the invariant

${P}_{0} : \;\left( {\exists i : {ak}.i\;\left( {i + t}\right) }\right)$

which suggests for Batcher's Baffler the form

“establish $t \geq N}$ ( ${P}_{0}$ )

$\therefore \underline{DO} \neq 1 \rightarrow {''decrease}$ t under invariance of ${PO}$ OD

Let the decrease of t under invariance of Po involve the transition from $t = t^{\prime}$ to $t = t^{\prime \prime}$ with $t'' < t'$ . It would be nice if we could exploit the precondition (Ai: OK.i.(i+1)) by keeping it invariant; we can only hope to do so provided it is implied by the postcondition (Ai: OK.i.(i+1)). On account of the transitivity of, this implication holds if t" is a factor of t'. Under that constraint the most modest decrease of t -i.e. the one that strengthens Po as little as possible- is halving t ; thus we suggest for the invariant P, given by

${P}{1} : \;{P}{0} \land t$ is a power of 2

and for Batcher's Baffler the form

$$ \begin{array}{l} t := 1; \underline {{d o}} t < N \rightarrow t := 2 \cdot t \underline {{o d}} {P _ {1} } \ ; \underline {{d o}} t \neq 1 \rightarrow t := t / 2 \quad {(\underline {{A}} i: o k. i. (i + 2 \cdot t)) } \ " r e s t o r e P _ {0} ^ {*} {(\underline {{A}} i: O K. i. (i + k)) } \ \end{array} $$

ad

The rest of this note is concerned with the

algorithm for "restore ${P}_{0}$ ",constrained by

$\left{ {P}_{2}\right. : \left( {A,i : O,k,i\left( {i + 2 - t}\right) }\right) }$

restore Po

$\left{ {P}_{0}\right. : \left( {\underline{\underline{A}}i : {OK}.i.\left( {i + t}\right) }\right) }$

it treats $t$ as a constant (for which its being a

with $\;\mathrm{e}.\mathrm{i} = \left( {\mathrm{i}\;\operatorname{mod}\;2 \cdot \mathrm{t}}\right) < \mathrm{t}$

we observe $e.i \equiv 7 \cdot e.(i + t)$

and rewrite ${P}{0}$ as ${P}{3} \land {P}_{4}$ with

P3: (h: e.i.: OK. i. (i+1)) and ${P}{4} : \;\left( {{A}{i} : 7 \in i : {0k}.i\left( {i + t}\right) }\right) \;$ or,equivalently ${PA}\text{、}\;\left( {{Ai} : e.i : {OK}.}\right) \left( {i + k.\left( {i + 2 - t}\right) }\right)$

The above dichotomy of the desired OK-relations is of interest because the argument pairs $i, (i + t)$ in $P_3$ and also those in $P_4$ - are disjoint on ac-count of e.i.e. $(i + t)$ . Hence $P_3$ or $P_4$ can be established by a whole bunch of Ord-operations that could be performed concurrently. (It is the potential for concurrency that makes Batcher's Baffler of interest.) Using II to denote the po- tentially concurrent combination, we have

[\left{ \begin{array}{l} \text{true}} \left( {\left| i : e.i : \operatorname{Ord}.i.\left( {i + t}\right) }\right) \left{ {P}_{3}\right} \end{array}\right. ]

and similarly

$\left{ \begin{array}{l} \text{ true } \ \end{array}\right. \left( {1 : {e}{i} : {\operatorname{Ord}}{i}\left( {i + b}\right) .\left( {i + 2 - t}\right) }\right) \;\left{ P \subset A\right.$

But one cannot achieve $P3 \land P4$ by executing the above two consecutively: the second operation

would in general destroy what the first one has accom- plished. Let us therefore investigate a strengthening of its precondition such that (1) does not falsify $P3$ . For our analysis we generalize (1) by replacing the constant 2 by the parameter v, restricted to even values so as to ensure that all pairs i,(i+v.t) with e.i are disjoint. That is, we consider the operation

(2) $\left( {\left\lbrack \begin{matrix} i : e.i : & \text{Ord.}\left( {i + t}\right) .\left( {i + v \cdot t}\right) \end{matrix}\right) }\right)$

and would like it not to falsify the OK- relations that constitute $P3$ . In our analysis we shall use the lemmata and -grudgingly - the notation of EWD932.

(i) Ok-relations with no argument involved in an Ord-operation are maintained on account of EWD932, Lemma 0. (ii) Of OK-relations with one argument involved in an Ord-operation we have two types:

neither of which, however, is a lemma. However

represent EWD932, Lemma 3. Note that, $v$ being even, the two OK relations added are implied by ${P}_{2}$ . (Here we are getting our first glimpse of how

to exploit precondition ${P}_{2}$ .)

(iii) Finally we investigate the OK-relation with both arguments involved in an Ord-operation:

This, again, is not a lemma , but we can recognize

Two of the added OK-relations are again implied

$$ (\underline {{A}} i: e. i: O K, (i + t), (i + 2 \cdot v \cdot t) $$

has to be implied by the precondition of (2), which, besides then leaving ${P}_{3}$ invariant,establishes

$$ (\underline {{A}} i: e. i: O K. (i + t). (i + v. t)) $$

i.e. the same formula after $v \mathrel{\text{:=}} v/2$ . We have found the invariant

P5: (A i: e.i.: OK. (i+1). (i+v.v)) A v 2 A v is a power of 2

for "restore ${P}_{0}$ "; it can be initialized by seeing

We are left with the duty to demonstrate that 10 and 2) maintain $P_{2}$

$$ E W D 9 3 5 - 5 $$

For invariance under (0) we have OK - relations

(i) with 0 arguments involved

$$ i \longrightarrow i + 2 \cdot t $$

EWD932, Lemma 0

(ii) with 1 argument involved

$$ \begin{array}{l} \underset {i + t} {\overset {i} {\longrightarrow}} i + 2 \cdot \frac {1}{t} \ \end{array} $$

EWD932, Lemma 1

(iii) with 2 arguments involved

$$ i \rightarrow i + 2. t i + t \rightarrow i + 3. t $$

EWD932, Lemma 2

For invariance under (2) we have $O\pi$ -relations

(i) with 0 arguments involved

$$ i \rightarrow i + 2. t $$

EWD 932, Lemma 0

$$ i + t \rightarrow i + 3 \cdot t $$

(ii) with 1 argument involved

$$ \begin{array}{l} {i + v \cdot t - 2 \cdot t \longrightarrow i + v \cdot t} \ {i + t ^ {- - - - - - - -}} \end{array} $$

EWD932, Lemma 1

$$ i + t ^ {- \dots - \dots - \dots} i + 3 \cdot t $$

(iii) with 2 arguments involved

$$ i + t \xrightarrow {i + v \cdot t} \longrightarrow i + v \cdot 2 + 2 \cdot t \quad E W D 9 3 2, L e m m a 2 $$

EWD935-6

And now we are ready for the final version of

[\left\lbrack {t,{vo} : {int}}\right\rbrack ]

$$ \begin{array}{l} ; t := 1; \underline {{d o}} t < N \rightarrow t := 2 \cdot t \underline {{o d}}; v _ {0} := 1 {P _ {1} \wedge t \cdot v _ {0} \geqslant N } \ ; \underline {{d o}} t \neq 1 \rightarrow t, v _ {0} := t / 2, 2 * v _ {0} {P _ {2} \wedge t \cdot v _ {0} \geq N } \ ; (\parallel i: e. i: O r d. i. (i + t)) {P _ {2} \wedge P _ {3} \wedge f \cdot v o \geq N } \ ; \llbracket v: i n t }; v := v 0 \left{P _ {2} \wedge P _ {3} \wedge P _ {5} \right} \ ; \underline {{\underline {{d o}}}} v \neq 2 \rightarrow v := v / 2 \ i (\parallel i: e. i: O r d. (i + t). (i + v \cdot t)) \ o d \ \triangledown \ \end{array} $$

ad

]

Remark For $N = 4$ , Battacher's Baffler generates the operations described on EWD932-2. (End of Remark.)

I am endebt to David Gries and the members of the EtAC (= Eindhoven Tuesday Afternoon Club).

Austin, 9 September 1985

prof. dr. Edsger W. Dgkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, Texas, 78712-1188

United States of America