This section is a warm-up for the next section.

We introduce the ``programming languages'' Algol 48 and Algol 50 to illustrate in a simpler setting some ideas to be used in Elephant 2000. These are the explicit use of time in a programming language and the representation of the program by logical sentences. The former permits a direct expression of the operational semantics of the language, and the latter permits proofs of properties of programs without any special theory of programming. The properties are deduced from the program itself together with axioms for the domain.

We use these names, because the languages cover some of the ground of Algol 60 but use only a mathematical formalism-- old fashioned recursion equations--that precedes the development of programming languages. They are programming languages I imagine mathematicians might have created in 1950 had they seen the need for something other than machine language. Algol 48 is a preliminary version of Algol 50 just as Algol 58 was a preliminary version of Algol 60.

Consider the Algol 60 fragment.

The program computes the product *mn* by initializing a
partial product *p* to 0 and then adding *m* to it *n* times.
The correctness of the Algol 60 program is represented by the
statement that if the program is entered at *start* it will reach
the label *done*, and when it does, the variable *p* will have
the value *mn*. Different program verification formalisms
represent this assertion in various ways, often not entirely
formal.

Its partial correctness is conventionally proved by
attaching the invariant assertion *p*=*m*(*n*-*i*) to the label *loop*.
Its termination is proved by noting that the variable *i* starts
out with the value *n* and counts down to 0. This proof is
expressed in various ways in the different formalisms for
verifying programs.

Fri Nov 6 21:37:30 PST 1998