This paper presents a method by which functions can be incorporated into a programming logic. The logic is inspired by Hoare’s axiom system [1], but uses terms rather than predicates. Complex terms may involve logical operators and hence look like predicates; however, the important difference is the use of equality between term values rather than the traditional implication between predicates.

The method can be used to deal with the partial correctness of many, but not all, semantic features of programming languages by means of a relatively small set of inference rules. (In view of the limitations noted by the author, it is perhaps worth suggesting that other attempts to extend Hoare’s basic system [2,3] might be rationalized with the paper under review to extract greater benefit from the concepts introduced therein.

The paper includes a small, realistic language which is formally defined by means of its inference system and then used in the correctness proof of a tree traversal program. Two theorems concerning the completeness of the system and its relationship with partial correctness (specified with respect to predicates) are stated at the end of the paper.

The central thesis of the paper is valid and worthy of further study; however, the paper could have been made more approachable. Part of the presentation claims to follow the style of Gordon [4]; :9I are not used in the same way. Also, semantic evaluation functions are anonymous, [t] being used instead of :9I for example, which would be easier to read. There is also evidence of inconsistency in revision of the text; for instance: (1) while the right-hand side of an assignment is defined to be a program term there is a simpler form of inference rule given for use in cases when the right-hand side is a non-program term and (2) the example program uses painters despite the statement that the system cannot treat pointers. Despite my quibbles regarding presentation, this paper is to be recommended to the program logician.