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.