\\ \heq {simplify} \f E = \<\mx i : i < \bigl((n+1/2)*Q - N\bigr)*10 : i \>\\ \heq {Corollary 1} \f \bigl((n+1/2)*Q - N\bigr)*10 - 1 \le E < \bigl((n+1/2)*Q-N\bigr)*10 \\ We observe: \f 0 \le E \\ \heq {trick, 0 and $E$ are integers} \df -1 < E \\ E < 10 \\ \dh\ff {above, left end} \ff {above, right end} \df -1 < \bigl((n+1/2)*Q - N\bigr)*10 - 1 \\ \bigl((n+1/2)*Q - N\bigr)*10 \le 10 \\ \dh \eq {simplify} \eq {simplify} \df N < (n+1/2)*Q\\ (n+1/2)*Q \le N + 1\\ \dh \eq {$P0$, right end} \eq {$P0$, left end} \df true\\ true\\ \filbreak So far so good! Now $F$. We show $0 \le F < 10$ in the state before ``$d:hiext.F$'', where $wp.``d:hiext.F".R2C$ holds. \f wp.``d:hiext.F".R2C \\ \heq {$N, Q \:= 10*N+F, 10*Q$} \f (n*Q-N)*10 - 1/2 < F \le (n*Q-N)*10 + 1/2\\ \filbreak We observe: \df 0 \le F \\ F < 10 \\ \dh \eq {trick, 0 and $F$ are integers} \ff {see above, right end} \df -1 < F\\ (n*Q-N)*10 + 1/2 < 10\\ \dh \ff {see above, left end} \eq {heading for $P0$, left end} \df -1 \le (n*Q-N)*10 - 1/2\\ (n*Q-1)*10 + 1/2 < N*10\\ \dh \eq {simplify} \ff {$P0$, left end} \df -1/2 \le (n*Q-N)*10\\ (n*Q-1)*10 + 1/2 < (n+1/2)*Q*10-10\\ \dh \ff {arithmetic} \eq {simplify} \df N < n*Q\\ 1/2 < (1/2)*Q*10\\ \dh\eq {$G1$} \eq {$\neg G2$} \df true\\ true\\ \filbreak Now that \out\ is proved correct---lucky as we are, $R3$ holds---, we reduce the expressions to integer arithmetics. We start with \nf G2: 10*Q \le 1\\ \heq {$Q=10^L\!/q$} \f 10^{L+1} \le q\\ \heq {new variable $u$ with invariant $u = 10^{L+1}$} \f u \le q\\ The invariant of $u$ is established by $u \:= 10$ and maintained by $u \:= 10*u$. \filbreak Next, we reduce \nf G1: N < (n-1/2)*Q \\ \heq {expand with $q$, reuse $u$} \f N*q*10 < (n-1/2)*u\\ \heq {think positive} \f u/2 < n*u - N*q*10\\ \heq {$u = 10^{L+1}$ is even} \f u \div 2 < n*u - N*q*10\\ \heq {new variable $v$ with invariant $v=n*u-N*q*10$} \f u \div 2 < v\\ \filbreak The expressions $n*u$ and $N*q*10$ might take large values. To avoid integer overflow, we store their difference in $v$. The invariant of $v$ is established by $v \:= 10*n$. We calculate $V$ such that $v$'s invariant is maintained by $v \:= V$. \f wp.``d:hiext.E; u, v \:= 10*u, V".(v = n*u - N*q*10)\\ \heq {semantics of the semicolon} \f wp.``d:hiext.E".\bigl(wp.``u, v \:= 10*u, V".(v = n*u - N*q*10)\bigr)\\ \heq {semantics of the assignment} \f wp.``d:hiext.E".(V = n*10*u - N*q*10)\\ \heq {array semantics: $N \:= 10*N+E$} \f V = n*10*u - (10*N+E)*q*10\\ \heq {simplify} \f V = (n*u - 10*N*q-E*q)*10\\ \heq {invariant for $v$} \f V = (v-E*q)*10\\ \filbreak Reducing $E$ and $F$ to $\div$ is straight forward by the well known Corollary 2 and the slightly less well known Corollary 3. \dnf E: \<\mx i : i < \bigl((n+1/2)*Q - N\bigr)*10 : i \>\\ F: \<\mx i : i \le (n*Q - N)*10 + 1/2 : i \>\\ \dh= {expand with $q$} = {expand with $q$, reuse $u$} \df \<\mx i : i*q < (n+1/2)*10^{L+1} - N*q*10 : i \>\\ \<\mx i : i*q \le n*u - N*q*10 + q/2 : i \>\\ \dh= {reuse $u$} = {reuse $v$} \df \<\mx i : i*q < n*u+ u/2 - N*q*10 : i \>\\ \<\mx i : i*q \le v + q/2 : i \>\\ \dh= {reuse $v$ , $u$ is even} = {see (*)} \df \<\mx i : i*q < v + u \div 2 : i \>\\ \<\mx i : i*q \le v + q \div 2 : i \>\\ \dh= {Corollary 3} = {Corollary 2} \df (v + u \div 2 - 1) \div q\\ (v + q \div 2) \div q\\ \filbreak The equation at (*) holds when $q$ is even, since then $q/2 = q \div 2$. And when $q$ is odd, we have $q/2 = q \div 2 + 1/2$ and we observe \f i*q \le v + q/2\\ \heq {$q$ is odd} \f i*q \le v + q \div 2 + 1/2\\ \heq {$i*q$ and $v + q \div 2$ are integers} \f i*q \le v + q \div 2\\ \filbreak This ends the reduction of \out\ to integer arithmetic and the construction of our program. \bblock \out\; \[\glocon n, q; \virvar d \co {0 \le n < q} ; \privar u, v ; d \vir int \array, u \vir int, v \vir int \:= (1), 10, n*10 ; \do u \div 2 < v \mand u \le q \->\&% d:hiext.\bigl((v + u \div 2 - 1) \div q\bigr) ; u, v \:= 10*u, (v - d.high*q)*10 \decind \od ; \IF u \div 2 < v \-> d:hiext.\bigl((v + q \div 2) \div q\bigr) \| u \div 2 \ge v \-> skip \FI \] \co {R0 \mand R1 \mand R2 \mand R3} \eblock That's it. The program is only proved correct, not tested. The proof and/or the program might contain errors. Please don't hesitate to contact me if you found one, or if you know a better way to apply Dijkstra's technique to a problem that turned out to be surprisingly hard. \vfill \bi Wolfgang Helbig\hfill {\tt helbig@lehre.ba-stuttgart.de}\qquad\bi Stauferstr. 22\hfill {\tt wwwlehre.ba-stuttgart.de/\~{}helbig/}\qquad\bi 71334 Waiblingen\hfill October 2008\qquad\hfill \eject \end