next up previous
Next: Elephant Programs as Sentences Up: Algol 48 and Algol Previous: Algol 48

Algol 50

 

However, by reifying variables, Algol 50 permits writing programs in a way that permits regarding programs in this fragment of Algol 60 as just sugared versions of Algol 50 programs.

Instead of writing var(t) for some variable var, we write tex2html_wrap_inline475 , where tex2html_wrap_inline477 is a state vector giving the values of all the variables. In the above program, we'll have tex2html_wrap_inline479 , tex2html_wrap_inline481 and tex2html_wrap_inline483 .

The variables of the Algol 60 program correspond to functions of time in the above first Algol 50 version and become distinct constant symbols in the version of Algol 50 with reified variables. Their distinctness is made explicit by the ``unique names'' axiom

displaymath485

In expressing the program we use the assignment and contents functions, tex2html_wrap_inline487 and tex2html_wrap_inline489 , of (McCarthy 1963) and (McCarthy and Painter 1967). tex2html_wrap_inline487 is the new state tex2html_wrap_inline493 that results when the variable var is assigned the value value in state tex2html_wrap_inline477 . tex2html_wrap_inline489 is the value of var in state tex2html_wrap_inline477 .

As described in those papers the functions a and c satisfy the axioms.

displaymath511

displaymath548

displaymath515

and

displaymath552

The following function definitions shorten the expression of programs. Note that they are just function definitions and not special constructs.

displaymath519

displaymath521

We make the further abbreviation loop = start+2 specially for this program, and with this notation our program becomes

displaymath159

In Algol 50, the consequents of the clauses of the conditional expression are in 1-1 correspondence with the statements of the corresponding Algol 60 program. Therefore, the Algol 60 program can be regarded as an abbreviation of the corresponding Algol 50 program. The (operational) semantics of the Algol 60 program is then given by the sentence expressing the corresponding Algol 50 program together with the axioms describing the data domain, which in this case would be the Peano axioms for natural numbers. The transformation to go from Algol 60 to Algol 50 would be entirely local, i.e. statement by statement, were it not for the need to use statement numbers explicitly in Algol 50.

Program fragments can be combined into larger fragments by taking the conjunction of the sentences representing them, identifying labels where this is wanted to achieve a go to from one fragment to another and adding sentences to make sure that the program counter ranges don't overlap.

The correctness of the Algol 50 program for multiplication by addition is expressed by

displaymath181

Note that we quantify over all initial state vectors. The last part of the correctness formula states that the program fragment doesn't alter the state vector other than by altering p, i and pc.

We have not carried the Algol 50 idea far enough to verify that all of Algol 60 is conveniently representable in the same style, but no fundamental difficulties are apparent. In treating recursive procedures, a stack can be introduced, but it would be more elegant to do without it by explicitly saying that the return is to the statement after the corresponding procedure call and variables are restored to their values at the time of the call. This requires the ability to parse the past, needed also for Elephant 2000.

We advocate an extended Algol 50 for expressing the operational semantics of Algol-like programming languages, i.e. for describing the sequence of events that occurs when the program is executed. However, our present application is just to illustrate in a simpler setting some features that Elephant will require. In particular, proper treatment of calling a function procedure with side-effects will require a state that can have a value during the evaluation of an expression.

Nissim Francez and Amir Pnueli (see references) used an explicit time for similar purposes. Unfortunately, they abandoned it for temporal logic. While some kinds of temporal logic are decidable, temporal logic is too weak to express many important properties of programs.


next up previous
Next: Elephant Programs as Sentences Up: Algol 48 and Algol Previous: Algol 48

John McCarthy
Fri Nov 6 21:37:30 PST 1998