\documentclass[runningheads,envcountsame,envcountsect]{llncs}
\usepackage{alltt}
\usepackage{graphicx}
\usepackage{array}
%\usepackage[a4paper,margin=1.5cm]{geometry}
%\usepackage[symbol]{footmisc}
%\pagestyle{empty}
\usepackage[hidelinks,bookmarks=false]{hyperref}
\raggedbottom

\hyphenation{Turing}

\begin{document}
\title{A large routine}
\author{Freek Wiedijk}
\date{}
\institute{
Institute for Computing and Information Sciences \\
Radboud University Nijmegen \\
Toernooiveld 212, 6525 EC Nijmegen, The Netherlands}
\maketitle
%\thispagestyle{empty}

\begin{abstract}
\noindent
This is a short text that I wrote for the \emph{Liber Amicorum}
for Jan Bergstra \cite{bet:bre:pon:16}, presented at his retirement in December 2016.
It speculates about a program that Alan Turing wrote in 1949.

The version for the \emph{Liber} used a tiny font and very
long lines to fit everything on the two pages I had available.
This is a version with a more reasonable layout.
It also has references, and an added appendix with the source code
of the program.
\end{abstract}

\noindent
It is not widely known, but already in June 1949\footnote{%
Two years before Jan Bergstra was born.%
} Alan Turing
had the main concepts that
still are the basis for the best approach to program verification known today,
and for which Tony Hoare developed a
logic in 1969 \cite{jon:14}.
In his three page paper \emph{Checking a large
routine} \cite{mor:jon:84,tur:49}, Turing describes how to verify the correctness
of a program that calculates the factorial function by
repeated additions.  He both shows how to use \emph{invariants}
to establish the correctness of this program, as well as
how to use a \emph{variant} to establish termination.

In the paper the program is only presented as a flow chart.
A modern C rendering is:
\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
int fac (int n)
\{
  int s, r, u, v;
  for (u = r = 1; v = u, r < n; r++)
    for (s = 1; u += v, s++ < r; )
      ;
  return u;
\}
\end{alltt}
\endgroup
\noindent
Turing's paper seems not to have been properly appreciated at
the time.  At the EDSAC conference where Turing presented
the paper, Douglas Hartree criticized that the correctness
proof sketched by Turing should not be called inductive.
From a modern point of view this is clearly absurd.

Marc Schoolderman first told me about this paper (and in his
master's thesis \cite{sch:16} used the modern Why3 tool \cite{why:16} of Jean-Christophe
Filli\^atre to make Turing's paper fully precise; he also wrote
the above C version of Turing's program).
He then
challenged me to speculate what specific computer Turing had in mind
in the paper, and what the actual program for that computer might
have been.

My answer is that
the `EPICAC'\footnote{%
EPICAC is a fictional computer from the short story
\emph{`EPICAC'} \cite{von:50} by Kurt Vonnegut, which was published November 1950,
only one year after Turing's paper
(and filmed for television in 1974 \cite{bad:74}, 1992 \cite{von:92} and 2008 \cite{tul:08}).
The EPICAC computer also occurs in Vonnegut's 1952 debut
novel \emph{Player Piano} \cite{von:52}, which is about the effects of robotisation on society.
The name EPICAC is a play on ENIAC (the first general-purpose electronic computer, operational February 1946;
computers of that era had names in this style:
%ENIAC,
%(Philadelphia, 1943-1946, 10 digit)
EDSAC,
%(Cambridge 1946-1949, 36-bit)
BINAC,
%(Philadelphia, 1949, 31-bit)
CSIRAC,
%(Sydney, 1949, 20-bit)
SEAC,
%(Gaithersburg, 1949, 45-bit)
SWAC,
%(Los Angeles, 1950, 37-bit)
EDVAC,
%(Aberdeen, 1949/1951, 44-bit)
UNIVAC,
%(Suitland, 1951/1952, 11 digit + sign)
ILLIAC,
%(Illinois, 1952, 40-bit)
%ORDVAC,
%(Aberdeen, 1951/1952, 40-bit)
MANIAC
%(Los Alamos, 1952)
%AVIDAC
%FLAC
%JOHNNIAC
--
the suffix `AC' generally stands for `Automatic Computer')
and
ipecac (a syrup with roots of the \emph{ipecacuanha} plant, used to
induce vomiting in case of poisoning).
In the story, a man and a
woman get romantically involved while working late at night
with the EPICAC computer, and at the end of the story the computer
provides the man with a lifetime support of love poems.
This story matches real life in some respects:
Conway Berners-Lee and Mary Lee Woods worked late at night
with the Ferranti Mark~1 computer in 1953 and married in
1954 (their son invented the World Wide Web in 1991), while
for this same computer in 1952 a program was developed by
Christopher Strachey that produces love letters \cite{str:54}.
(Strachey also
wrote the first program for the game of draughts \cite{lin:12}, and
the first program for computer music; in 1965
he became the first director of the Programming
Research Group in Oxford, where he
developed denotational semantics in collaboration with Dana Scott.)
The
`love letters' program has been revived as an art project
by David Link in 2009 \cite{lin:06,lin:09,lin:11}.
} of this paper probably was
the Manchester Mark~1.
Given that Turing
at that time was Deputy Director of the Computing Laboratory
in Manchester,
this is not very surprising.
Further arguments for this are that the
paper talks about 40-bit words, and that it uses storage locations
27--31 called `lines' for the variables.

Of the computers at that time only the ones
in development in Manchester and at
the IAS in Princeton had 40-bit
words.  Turing had written his PhD thesis in Princeton, and
undoubtedly knew about the IAS machine,
but he was much more closely involved with the Manchester
machines.
Also, in 1949 the Manchester machines already were
operational, while the IAS machine only became operational
in 1951.  The Manchester machines had three generations:
the \textbf{Manchester SSEM} (Small-Scale Experimental Machine)
`baby' (32-bit, operational June 1948),
the \textbf{Manchester Mark~1} (40-bit, operational April 1949)
and the commercial \textbf{Ferranti Mark~1}
(40-bit, operational February 1951).
Turing wrote in 1950 a very nice and surprisingly modern manual \cite{nap:10,tur:50,tur:tha:00} for this last
machine (which unlike Ferranti he calls `Mark II',
as in his opinion `Mark I' already had been used).
This manual also describes the earlier Manchester Mark~1
in an appendix, where it is called the `Pilot machine'.

The question then is which of the two 40-bit Manchester
computers Turing had in mind in his `large routine' paper.
These machines are very similar, but in 1949 the newer
machine was not yet operational.
%
There is another argument for the earlier machine:
in both machines the addresses are \emph{twice} the `storage locations'
that Turing uses in his paper (there is no space to fit a full word between two consecutive addresses),
which means that Turing is \emph{not}
talking about addresses.
The storage of the
Ferranti machine on a Williams tube consists of two columns next to each other,
where `words' are two successive half-lines in a single column.
But the older machine has the 40-bit words spanning the whole
width of the tube, which means that in that case Turing just numbered the five bottom-most of those `lines' in his paper.
For this reason it seems more natural to consider
a program for the earlier Manchester Mark~1.

The architecture of the Manchester Mark~1 has 40-bit
words, but the accumulator has 80 bits, and the memory is
addressed in 20-bit `bytes' (when
fetching a full word from memory the lowest address bit is ignored,
hence addresses are always aligned).
The `nibbles' of the machine are 5-bit, and are written
using the ITA2 variant from 1924 of the Baudot punched tape
code patented in 1874
(where additional symbols \texttt{/}, \texttt{@},
\texttt{:}, \raise2pt\hbox{\scriptsize $\frac{\tt 1}{\tt 4}$}, \texttt{"} and \texttt{\pounds} represent
the `non-printing characters').
Turing does not use
symbolic syntax for machine code and just writes each 20-bit instruction as
four ITA2 characters.
See for nice examples of programs written in this style the listings linked from \cite{pri:sum:53}.

The Manchester Mark~1 instruction set is very simple.
An instruction has an opcode -- of the 32 opcodes, our reconstructed program
only uses seven -- and an address field.
The instruction layout (in little endian bit order) is:
%\vspace{-1em}
\begin{center}
\vspace{.1cm}%
\tabcolsep=0.2cm
$\hspace{-8cm}$
\begin{tabular}{m{9cm}m{9cm}}
%\begin{alltt}\small
% 0       4 5       9 10     14 15     19
%|---------+-----|---+---------|---------|
%|    address    |   unused    | opcode  |
%|---------+-----|---+---------|---------|
% 0             7 8          14 15     19
%\end{alltt} &
\strut\raise-4pt\hbox{\begingroup
\linethickness{.3pt}
\setlength{\unitlength}{.4cm}
\begin{picture}(20,2)
\put(0.014,0){\framebox(19.972,2){}}
\put(0,0){\makebox(8,2){\strut address}}
\multiput(1,.05)(0,.3){7}{\line(0,1){.1}}
\put(8,0){\line(0,1){2}}
\put(8,0){\makebox(7,2){\strut unused}}
\put(15,0){\line(0,1){2}}
\put(15,0){\makebox(5,2){\strut opcode}}
\put(0,2){\line(0,1){.3}}
\put(5,2){\line(0,1){.3}}
\put(10,2){\line(0,1){.3}}
\put(15,2){\line(0,1){.3}}
\put(20,2){\line(0,1){.3}}
\put(.5,2.5){\makebox(0,0)[c]{\scriptsize\strut 0}}
\put(4.5,2.5){\makebox(0,0)[c]{\scriptsize\strut 4}}
\put(5.5,2.5){\makebox(0,0)[c]{\scriptsize\strut 5}}
\put(9.5,2.5){\makebox(0,0)[c]{\scriptsize\strut 9}}
\put(10.5,2.5){\makebox(0,0)[c]{\scriptsize\strut 10}}
\put(14.5,2.5){\makebox(0,0)[c]{\scriptsize\strut 14}}
\put(15.5,2.5){\makebox(0,0)[c]{\scriptsize\strut 15}}
\put(19.5,2.5){\makebox(0,0)[c]{\scriptsize\strut 19}}
\put(.5,-.6){\makebox(0,0)[c]{\scriptsize\strut 0}}
\put(7.5,-.6){\makebox(0,0)[c]{\scriptsize\strut 7}}
\put(8.5,-.6){\makebox(0,0)[c]{\scriptsize\strut 8}}
\put(14.5,-.6){\makebox(0,0)[c]{\scriptsize\strut 14}}
\put(15.5,-.6){\makebox(0,0)[c]{\scriptsize\strut 15}}
\put(19.5,-.6){\makebox(0,0)[c]{\scriptsize\strut 19}}
\linethickness{1pt}
\put(19.5,1){\vector(1,0){3}}
\end{picture}
\endgroup} &
\tabcolsep=.5em
$\left\{
\mbox{\begin{tabular}{lll}
\texttt{H} & \texttt{00101} & $A \leftarrow [a]$ \\
\texttt{M} & \texttt{00111} & $A \leftarrow A + [a]$ \\
\texttt{X} & \texttt{10111} & $A \leftarrow A - [a]$ \\
\texttt{D} & \texttt{10010} & $[a] \leftarrow A$ \\
\texttt{R} & \texttt{01010} & skip next instruction if $A \ge 0$ \\
\texttt{L} & \texttt{01001} & go to instruction at address $a + 2$ \\
\texttt{N} & \texttt{00110} & halt
\end{tabular}}
\right.$
\end{tabular}
$\hspace{-10cm}$
\vspace{.1cm}%
\tabcolsep=0.2cm
\end{center}
\noindent
In this, $A$ is the accumulator, $a$ is the address, and $[a]$
the 40-bit word at that address in memory.  After an instruction
is executed, the program counter (where
the lower bit is \emph{not} ignored) is increased by \emph{two},
so execution will proceed on the same side on the tube.

Here then, is a reconstruction of Turing's `large routine'
for the Manchester Mark~1, both the source code in paper tape
format, and the resulting state of the machine as seen on a Williams tube:
\begin{center}
\includegraphics[width=12cm]{pics/tape.jpg}
\end{center}
\begin{center}
\vspace{-.4cm}
\includegraphics[width=9cm]{pics/tube.jpg}
\vspace{-.4cm}
\end{center}
\noindent
The program is in the top half of the tube, in two columns, and the variables 
are at the bottom.
The input $n = 10 = \mbox{\small$1010$}_2$ is in line~29, while the
output $u = 10! = \mbox{\small$1101110101111100000000$}_2$ is in line~30.

\bibliographystyle{plain}
\bibliography{janb}

\newpage
\appendix
\section*{Source code of the routine}
For this paper, I wrote
an emulator for a relevant small fragment of the Manchester Mark~1.
The source code for this emulator can be found on the web at:
\begin{center}
\url{http://www.cs.ru.nl/~freek/pilot/pilot.c}
\end{center}
Marc Schoolderman extended this with the feature that if
it is compiled with the symbol \texttt{VT100} defined,
then the emulator
will insert terminal escape codes to make the output look
like a Williams tube.

The input for this emulator corresponding to Turing's program
as reconstructed in this paper, is:
\begin{alltt}\small
//   G/ /H  // //       ;     A' = [1]                              E/
@/   ME /D  VE /M       ;     [u]' = A          F: A' = A + [v]     A/
:/   OE /D  ME /D       ;  B: [r]' = A             [u]' = A'        S/
I/   ME /H  PE /H       ;     A' = [u]             A' = [s]         U/
8/   VE /D  G/ /M       ;     [v]' = A             A' = A + [1]     D/
R/   OE /H  PE /D       ;     A' = [r]             [s]' = A         J/
N/   GE /X  OE /H       ;     A' = A - [n]         A' = [r]         F/
C/   // /R  PE /X       ;     skip if A < 0        A' = A - [s]     K/
T/   // /N  // /R       ;     halt                 skip if A < 0    Z/
L/   G/ /H  V/ /L       ;     A' = [1]             C' = [E]         W/
H/   PE /D  OE /H       ;     [s]' = A             A' = [r]         Y/
P/   ME /H  G/ /M       ;  E: A' = [u]             A' = A + [1]     Q/
O/   G/ /L  M/ /L       ;     C' = [F]             C' = [B]         B/

G/   E/ //  // //       ;    1 = F - 2
M/   @/ //  // //       ;    2 = B - 2
V/   H/ //  // //       ;   20 = E - 2

PE   // //  // //       ;   s
OE   // //  // //       ;   r
GE   R/ //  // //       ;   n = 10
ME   // //  // //       ;   u
VE   // //  // //       ;   v
\end{alltt}
This input also can be found on the web at:
\begin{center}
\url{http://www.cs.ru.nl/~freek/pilot/fac.pi}
\end{center}
Finally the two pictures from this paper (processed versions
of the input and output described here) are on the web
at:
\begin{center}
\url{http://www.cs.ru.nl/~freek/pilot/tape.pdf} \\
\url{http://www.cs.ru.nl/~freek/pilot/tube.pdf}
\end{center}

\end{document}