Search

This article is an introduction to Professor Howard Barringer, in honor of his 60th birthday on December 20, 2011, which was celebrated by the HOWARD-60 workshop (Higher-Order Workshop on Automated Runtime verification and Debugging), held on the same day at University of Manchester. 1 A 60 Second Overview Howard Barringer was born on December 20, 1951, is married to Margaret, and has three children. This forms the concrete part of Howard’s life. Beyond this, Howard has had an abstract life centred around mathematics, physics, and computer science. At secondary school (1964-1969) Howard moved into the science stream and finished with ’A’ levels in mathematics (pure and applied) and physics. He went on to University of Manchester where he first received a B.Sc in Physics (1972), then an M.Sc in Computer Science (1973), and finally a Ph.D in Computer Science (1978). His adult academic life has been centred at University of Manchester. He became a Research Associate in Computer Science at Manchester in 1975, a Lecturer in 1977, a Senior Lecturer in 1986 and was then rapidly promoted to Professor in Computer Science in 1987. For the majority of his career, his research and teaching has been focussed around the development and application of logics, in particular temporal and modal logics, in the specification, design, and analysis of software and hardware systems. Howard insisted on the importance of past time logic in temporal logic, and hence got named “the man who invented the past”. He has taught classes in the theory of computation, compiling techniques, specification and verification, concurrency, modal and temporal logic, algorithms, and programming in Java. Howard also spent a significant portion of his career in senior and highly influential administrative positions at University of Manchester. He has been invited to present over 100 seminars and research lectures in Austria, Belgium, Canada, China (Beijing, Shanghai, Wuhan), Denmark, England, France, Germany, Greece, Israel, Italy, the Netherlands, Norway, Scotland, South Africa, Spain, Sweden, USA (Arizona, California, New York, Pennsylvania, Texas) and Wales. He was visiting professor at Kings College (2001 and 2006), and visited Silicon Valley numerous times including NASA Ames Research Center, Moffett Field, CA in 2002 and 2003, and the Computer Science Laboratory at SRI International, Menlo Park, CA in 2002. It has been observed that, temporally speaking, a series of Mars Rovers were launched after Howard visited NASA. Howard was one of the ∗The writing of this article was carried out at Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration. 1This title was assigned to Howard in connection with his 60th birthday by Andrei Voronkov. A. Voronkov, M. Korovina (eds.), HOWARD-60, pp. 1–12 1 Howard Barringer Klaus Havelund founding editors of the Journal of Logic and Computation in 1989 and is now Co-Chief Editor with Dov Gabbay. He is also Editor for Journal of Applied Logic. 2 Initial Research Phase Howard started his research activities in systems programming (1973–1979). The research for the M.Sc and Ph.D degrees was concerned with compiling techniques for the ALGOL 68 programming language. As a Research Assistant after his doctorate, his work involved the design and implementation of portable compiling systems, and resulted in a low-level target machine language (TML) (Barringer, Capon and Phillips, 1979) [20] and a simpler high-level systems implementation language (MUPL). This line of work continued during the first year in which he was employed as a lecturer within the Department of Computer Science and resulted in the implementation of an improved, higher level, intermediate target language (TL) that enabled straightforward implementation of an improved systems implementation languages (MUSL). During the end of the 1970s, Howard developed an interest in formal methods, causing a change of direction. This change coincided with Cliff Jones joining Manchester University as professor. Together with Howard’s Ph.D student Jen Cheng they worked on a logic for partial functions, see (Barringer, Cheng and Jones, 1984) [22]. During the first half of the 1980ties, his interest otherwise centred around compositional temporal logic, specifically techniques for specification and verification of parallel and distributed systems. Initially, results were obtained for the axiomatic verification of Ada tasks (Barringer and Mearns, 1982) [21] and (Barringer and Mearns, 1986) [23]. He became a member of the CEC Ada-Europe Working Group on Formal methods for Specification and Development (1983–1985), was chairman for this group from 1985–88, and was additionally member of the Ada UK Working Group on Formal Methods from 1984–87. In 1981-1982 he went on two three-week trips to 12 university and industrial research laboratories in the United States to have discussions with researchers about their verification methods. The research undertaken was published as a volume in the Springer-Verlag Lecture Notes in Computer Science series (Barringer, 1985) [1]. The study led to ideas on specifying systems in a modular and compositional fashion based on the use of temporal logics – including reasoning about the past – which were presented in (Barringer and Kuiper, 1983) [44]. As a result of this work, Howard spent a couple of weeks at the Weizmann Institute of Science, Israel, at the invitation of Professor Amir Pnueli in order to collaborate on developing compositional temporal proof systems for parallel languages (the goal of compositionality in temporal proof systems had been standing for approximately eight years). That visit marked the beginning of a strong collaboration with Pnueli, leading to general techniques for constructing compositional temporal proof systems for both shared variable and message based communication mechanisms in parallel programming languages (Barringer, Kuiper and Pnueli, 1984) [47], (Barringer, Kuiper and Pnueli, 1985) [49] and for fully abstract concurrency models (Barringer, Kuiper and Pnueli, 1986) [50]. Other researchers joined the work and visited Manchester, including Professors Willem-Paul de Roever and Zhou Chaochen. In 1986, at the invitation of Professor Zhou Chaochen, he presented a research lecture series on temporal logic and its applications in concurrency (a total of 32 hours of lectures was presented at the Academy of Sciences, Beijing, Wuhan University and Fudan University, Shanghai, over a four week period). Further work led, for example, to a temporal fixed point calculus (Banieqbal and Barringer, 1986) [104], as well as what was probably the first practical implementation of a decision procedure for checking validity of a linear temporal logic covering infinite past, present and infinite

In this article history of Algol 68, USSR research groups implementing this language and it's impact on the programming as a whole in USSR are described. Algol 68 Working Group headed by academician Andrey Ershov was organized. This group had meetings 4-5 times a year in different USSR cities where Russian terminology, practical questions of translation technique, etc were discussed. History of A68LGU translator development is described. This Algol 68 translator was very popular in USSR both in the universities and industrial enterprises. DSL (Domain Specific Languages) languages based on Agol 68 and their usage in the USSR are shown. Also some questions of Algol 68 use in education and it's role in new HLL (High Level Language) computers creation is mentioned.

ALGOL 68 is a language with a lot of “history”. The reader will hear of discord, resignations, unreadable documents, a minority report, and all manner of politicking. But although ALGOL 68 was produced by a committee (and an unruly one at that), the language itself is no camel. Indeed, the rigorous application of the principle of “orthogonality” makes it one of the cleanest languages around, as I hope to show. Moreover, when the language came to be revised, the atmosphere was quite different enabling a much more robust and readable defining document to be produced in a spirit of true cooperation. There are some lessons here for future language design efforts, but I am not optimistic that they have been learned.

Mössenböck proposes the argument block as a language construct for using statement sequences as arguments for procedures [Mös92]. Such a construct enables users to define their own control structures. Mössenböck is inspired by S MALLTALK -80 [GR83] and claims that most languages lack support of argument blocks but does not take into account a quality which in practice is crucial to their utilization. Stolz [Sto93] therefore falsely concludes the equivalence of argument blocks and anonymous procedures and points out that anonymous procedures were already supported in ALGOL 68 [vWMP + 76]. We show the difference between blocks and procedures and describe implementation patterns which are taken under consideration for the programming language A RISTARCH /L. A RISTARCH /L is supposed to support the distributed operating system A RISTARCH /OS which is under development in S AMOS , a project undertaken by the Operating Systems Research Group at the University of Karlsruhe.

Hanspeter Mössenböck has proposed [7] a language construct for treating statement sequences as block objects that can be passed to procedures as parameters. As these blocks are nothing else but parameterless procedures, a more orthogonal solution to Mössenböck's set of problems has long been available: in the programming language Algol 68, a routine-text can be specified, anonymously, in the place of an argument.The present contribution presents Mössenböck's example in Algol 68 notation, and demonstrates the versatility of anonymous routine-texts by transforming the given example to a neater solution.

We report on an investigation into the systematic errors made by a large group of programming language students over a period of two years. The investigation and the learner-centered longitudinal study of which it formed a part, were both inspired by recent research into second natural language acquisition. The results of the investigation demonstrate that students had major difficulties using the semicolon, the sequencing operator of the programming language ALGOL 68. We argue that this difficulty is due to the fact that students did not immediately understand a specific, simply stated rule of syntax, introduced in a decontextualized way, but rather that their understanding of the rule developed with their increasing experience of using it in different contexts. We suggest that such systematic low-level syntactic errors may be indicative of higher-level misconceptions regarding the structure of the language.

This paper, one of a simultaneously published set on ten years of activity in programming language standards, describes the developments in standardization of the programming languages Algol 60, Algol 68 and Simula which have taken place in the period 1983–1993.

The aim of this paper is to provide an introduction or guide to the Revised ALGOL 68 Report [15]. The earlier revised ALGOL 60 Report[12] constituted one of the first attempts at formally defining a programming language. This was a major advance and opened up new areas of interest and research in computer science. But there were some deficiencies in both the language and in its formal definition. In the course of time other attempts were made at improving and correcting the earlier oversights. Our intention here is to begin by considering the formal definition of ALCOL 60 [12] and to show how these early ideas gradually evolved to produced the method of formally defining ALGOL 68. The discussion will, for the most part, be restricted to the ALGOL movement. But over the years other advances have been made in formally defining languages. The most notable of these is probably the development from McCarthy's LIPS [7–11] through to the Vienna Definition Language [5, 6, 16, 17] and beyond. But see also [4]. In discussing formal definition of programming languages one must distinguish between the programming language itseld and its method of formal definition. These are quite separate. Yet they tend to be confused since new methods of formal definition often accompany new programming languages. And a formlal definition tends to provide a vocabulary of terms by which various constructions become known. It will be assumed that the reader has a certain knowledge of the programming languages ALGOL 60, ALGOL W and ALGOL 68. Moreover it would be convenient if he had available a copy of the formal definition of each language. Although it should be possible to proceed without these documents frequent references are made to them.

A large subset of the language Algol 68 has been implemented on a small computer—the TESLA 200 with a 64 Kbyte store. In this paper, the general structure of the compiler and organization of the program at run-time are described. Especially, the original methods and devices are mentioned that cause a considerable enhancement of the speed of compilation and program run. These concern the syntax analysis (consistent notation, error recovery), the organization of the resulting program (procedure organization, algorithms of work with multiple values) and the techniques of code generation. We try to show that Algol 68 is a suitable programming language for small as well as large computers and that it can successfully compete with traditional programming languages.

A segmentation scheme for ALGOL-like programs is presented. This scheme, based on the separate compilation facility of the language ALGOL 68C, enables the programmers to use a branch-and-merge (lattice) structure in segmenting their programs, besides the tree which is the only one structure usable in ALGOL 68C programming. The necessity of this scheme is explained and the way of its implementation is described. The effectiveness of this scheme compared with tree structure segmentation is shown in terms of the recompilation cost of an example program of reasonably large size which has been resegmented from the tree to the lattice structure with no addition or duplication of codes.

Early results of a project on compiling stylized recursion into stackless iterative code are reviewed as they apply to a target environment with multiprocessing. Parallelism is possible in executing the compiled image of argument evaluation (collateral argument evaluation of Algol 68), of data structure construction when suspensions are used, and of functional combinations. The last facility provides generally, concise expression for all operations performed in Lisp by mapping functions and in APL by typed operators; there are other uses as well.

An attempt is made to assess some static and dynamic properties of ALGOL 68 programs, which are useful for optimization decisions. The results indicate that slicing and assignation are the most important candidates for optimization, and that optimization efforts need to be directed to the simple cases only.

The implementation of graph-theoretic algorithms using the facilities of standard algorithmic languages is not easy since data structures and operations natural to the subject are not readily available. GRAAP (GRaph Algorithmic Applications Package) is a new system designed to solve this problem. Written in ALGOL 68-R it consists of about 150 operators and procedures which perform operations natural to graph theory and essential to the implementation of graph algorithms. These operators and procedures manipulate information representing graphs and related objects stored in suitably defined structures. GRAAP exists as an album of precompiled segments to minimise compilation time. The operations provided and the transparent internal representations of graphs of different kinds are discussed. The ease with which algorithms can be implemented is demonstrated by examples.

An Algol 68 implementation of a LISP‐like list processing package is described. Emphasis is placed upon the importance of Algol 68 as a teaching tool and upon the need for proving the correcTMESs of the programs.

The relative merits of LL and LR parsing methods are compared, particular reference being made to ALGOL 68. The fact that LR methods can be applied to a wider class of languages does not seem to give them a significant advantage in practice.

This paper puts forward a proposal for an ALGOL 68 binding to GKS. It is hoped that this can be the basis for producing an internationally accepted binding of GKS to ALGOL 68, after discussion and review, in order that programs which use graphics from ALGOL 68 may easily be transported between different computer systems.

M. H. Halstead has argued that all computer programs are composed entirely of operators and operands. By counting these entities the software science theory then enables program properties such as vocabulary, length, volume, program level and language level to be calculated. For well written, or so-called ‘pure programs’, one would expect, according to the theory, good agreement between certain observed and predicted values. Also, one might expect an intuitive ordering of language levels to be confirmed by the theory, with for example, Algol 68 having a higher language level than Fortran. In this paper two different counting strategies have been applied to one implementation of the Numerical Algorithms Group (NAG) Algol 68 library. The results do not entirely match expectation.

This paper describes a system of library segments which have been written to help in the teaching of programming to undergraduates at Nottingham. Each segment contains input for a number of problems in a very specific area of programming, together with checks that the student has solved the problems satisfactorily. The system is implemented in Algol 68-R.

The problems concerning SIZETY definitions in an Unabridged Machine-Independent Standard Prelude for ALGOL 68 are examined and tentative solutions are given.

A system's input/output is its communication with the other systems in its environment. By viewing the relationship as communication between partners, we identify the fundamental requirements in input/output programming, and discuss the responses of various programming languages to these requirements. Traditional programming languages provide either nothing or an expensive incomplete solution. The new languages Modula and Ada now offer major improvements in this area. We describe the style of their solutions, and give corresponding guidance for low-level input/output programming.

Predicates are used in the Revised ALGOL 68 Report to indicate blind alleys and to reduce the number of rules in the Report. They may also be used by the compiler writer to implement some of the non-context-free aspects of the language. This paper shows how the predicates can be transformed in a relatively straightforward way into ALGOL 68 procedures to form part of an analyser for the revised language.

If array handling is to be properly described diagrammatically, implementation dependent information must be incorporated. By introducing to van der Meulen diagrams more of the information usually found in the headers of arrays, the resulting diagrams can clearly show the effect of the various Algol 68 array manipulation instructions. These diagrams have proved a valuable teaching aid.

There is a number of comparisons of various programming languages, but there is only a limited number of comparisons based on the quantitative assessement (Perrit, Dhillon, 81). This paper provides the comparison of some Algol 68 features with similar features in other languages e.g. Pascal and Ada. The comparison is based upon the statistics (profiles) of Algol 68 programs. Terms used in this paper come rather from general programming languages background than from particular Algol 68 terms. Special features and necessary Algol 68 terms are explained in the text. The most significant results: 25 per cent of IFs are conditional expressions, constant declarations are more frequent than variable declarations.

An outline of the three phase method of discrete event simulation is given, and problems in designing a language for this method based on ALGOL 68, together with the final form of the language, are discussed. An important area is seen to be that of lists or sets, and the necessity of devising facilities that are powerful yet simple to use is stressed. Operators are shown to be particularly useful for this.

The facilities of ALGOL 68 for defining new data types and operations are used for the description and manipulation of pictures. Starting with points, polygons and strings as primitives, more complex pictures may be built up with operations such as uniting of pictures, positioning, scaling, and rotating. The use of the various interactive devices is shortly discussed and a sketch of the procedure, which translates the data structure being created by a GRAPHEX68 program into a graphical assembly language, is given.

WITH MANY of the general programming languages available today inadequate in their string handling capabilities, users who wish to process text have to resort to unnatural extensions to languages such as FORTRAN and ALGOL 60, in which string manipulation is often provided by subroutines or procedures from a library. There are, of course, languages specifically designed to meet the needs of those who wish to pursue non-numeric programming activities languages such as SNOBOL IV [1] and SNAP [2] but these may either fall short on numerical or structural capabilities, or not be implemented on the user's machine. Some languages, designed for interactive use, such as SCAN [3], are usually machine dependent. A few more recent languages, such as ALGOL W [4] and ALGOL68 [5], although they have good string manipulative capabilities built into them, are not always available to some sections of the community (ALGOL W is orientated to IBM 360/370 machines, ALGOL 68 has not yet become readily available on many ranges of computers). The general programming language EULER [6], proposed as a successor to ALGOL 60, had many of the characteristics of that language. It also had many new features that need to be described in more detail. The language 'is a block structured language, where a block contains declarations and statements enclosed within begin and end. The essential difference between blocks in EULER and blocks in ALGOL 60 is that EULER blocks, which can return a usable value, can be a valid constituent of an expression, for the value of the block is the result of the last expression evaluated before leaving the block.

A syntactic error recovery technique is presented that is simple and at the same time very powerful. It has the main property that it is phrase marker oriented, where phrase markers are considered symbols delimiting language constructions, e.g., begin and end for blocks, (and) for expressions, and [and] for indices. The basic idea of this error recovery technique originates from P. Branquart and has been worked out in the Algol 68 compiler project, see [8] and [9]. Here, we are especially concerned with the generation aspects of error recovery. In particular, it is investigated how error recovery can be mechanised in an ELL(1) and LALR(1) syntax directed translation scheme and which conditions the syntax must satisfy. Both the ELL(1) and LALR(1) generators are implemented and are part of the system LILA: a Language Implementation LAboratory [28, 29, 30]. Only the ELL(1) generator is described here.

Two methods for extending Algol 68 to handle decision tables are described. One method allows an extension to Algol 68 to handle limited entry decision tables while the other method, which involves the use of a preprocessor, extends Algol 68 to handle mixed entry decision tables. Two systems have been constructed using the ideas outlined in this paper; these are described and examples of their use are given.

The classical programming languages such as PASCAL or ALGOL 68 do not provide full data type security. Run-time errors are not precluded on basic operations. Type safety necessitates a refinement of the data type notion which allows subtypes. The compiler must also be able to ensure that basic operations are applicable. This verification consists in determining a local subtype of globally declared variables or constants. This may be achieved by improved compiler capabilities to analyze the program properties or by language constructs which permit the expression of these properties. Both approaches are discussed and illustrated by the problems of access to records via pointers, access to variants of record structures, determination of disjoint collections of linked records, and determination of integer subrange. Both approaches are complementary and a balance must be found between what must be specified by the programmer and what must be discovered by the compiler.

An examination is made of the different ways in which APL and ALGOL 68 refer to cross-sections or other subsets of an array. It is noted that APL allows a variety of reference operations but no reference variables; on the other hand, ALGOL 68 has reference variables and parameters, but only one array operation. Two kinds of array reference are distinguished - the linear and the nonlinear - and a proposal is made for representing a linear reference by a simple form of descriptor, suitable for processing in hardware. The reference operations are then divided into those which give linear results and those which give non-linear. By retaining only the linear ones, it is possible to combine the main advantages of the APL and ALGOL 68 operations into a single system. A discussion is given of some of the issues involved, including those of dynamic types and bounds.

We illustrate the use of Algol 68 as a systems implementation language by reference to practical uses of the language. We argue that the code patch facility as implemented in Algol 68-R is a good way of interfacing systems programs to their machine-dependent environment, and does not violate the spirit of high-level language programming.

An ALGOL 68 expert described PL/I, not long ago, as a 'hotch-potch of obsolete ideas'. The PL/I people tend not to know much about ALGOL 68, and not to care much either. In fact the two languages have many features in common, which makes it convenient to consider them together. We begin with the lexical aspect, that is, how statements are actually written. Here ALGOL 68 has followed on from ALGOL 60, but PL/I has taken features from several different languages. In ALGOL 68 language words are 'basic tokens' and are distinguished from identifiers by writing them in a different type face, which may be represented in a particular implementation by use of the underline character or by enclosing the word between quote marks, exactly as in ALGOL 60. Spaces and card or line boundaries are ignored in all contexts, except perhaps within basic tokens. In PL/I there is only one alphabet. The fact that a word is a keyword, however, does not prevent its being used as an identifier. The usage may always be deduced from the context. Spaces are significant where they separate one word from the next. In general extra spaces are allowed. Card or line boundaries are not significant. The semicolon is used to show where each statement finishes. For characters in general, PL/I offers either a 48-character set or a 60-character set. Alternatives are provided for the extra 12 characters when the smaller set is in use. ALGOL 68 is defined in terms of abstract symbols, but the Report does stoop to suggesting representations for them, which turn out to be on similar lines to the PL/I set, but hopeful of 80-odd characters if available—or well over 100 if the different type fount is to be provided. Here one feels that PL/I was designed with punched cards and line printers in mind, while ALGOL 68 is envisaged for 7 or 8 channel paper tape as the main input/output medium.

A method for the creation of a virtual Algol 68 program library on top of a subset of the NAG‐FORTRAN library is discussed.

A method is described of introducing to absolute beginners basic concepts of structured programming, including constructing programs by “step-wise refinement”. This is interleaved with a “top-down” description of a simple mini-subset of ALGOL 68, which is closely followed by the concepts of data structuring and procedurisation, as expressed in this language. Emphasis throughout is on the programming philosophy behind the approach controlling the teaching of ALGOL 68, rather than vice versa.

This paper presents a new model for exception handling, called the replacement model. The replacement model, in contrast to other exception-handling proposals, supports all the handler responses of resumption, termination, retry, and exception propagation, within both statements and expressions, in a modular, simple, and uniform fashion. The model can be embedded in any expression-oriented language and can also be adapted to languages which are not expression oriented with almost all the above advantages. This paper presents the syntactic extensions for embedding the replacement model into Algol 68 and its operational semantics. An axiomatic semantic definition for the model can be found in [27].

Janus is a symbolic language intended for use as an intermediate language in the transportation of software. Since its initial design four years ago, it has been used to implement a portable Pascal compiler, in the design of an Algol 68 compiler, and to realize a portable package of mathematical routines. These experiences, together with a critical re-evaluation of the design criteria, have led to some modification of the specifications of Janus and an increased confidence in the viability of the approach. They have also indicated some problems yet to be solved. This paper reviews the significant lessons which we have learned, and quotes some results which support our confidence.

This paper describes an implementation of coroutines in BCPL, and gives an example of the use of the coroutine mechanism in an experimental compiler for Algol 68.

Parameter passing mechanisms are developed for optional, repeatable, and varying type parameters. For optional parameters, a programmer-defined default value is passed when the actual parameter is not present; in addition, the called procedure may determine whether the actual parameter is present. An arbitrary number of actual parameters may be passed by binding them to an array-like structure in the called procedure. Syntax similar to Algol 68's union type is proposed to allow passing parameters of varying types. These mechanisms are suggested as useful extensions to Pascal-like languages.

The paper outlines the use of ALGOL 68R in the production of a series of simulation models for a Multi Radar Tracking feasibility study. Particular reference is made to the use of structures , the chaining mechanisms used and the modularity of the models. The multi-radar tracking models were developed in ALGOL 68'R by Plessey Radar Ltd. and run on their 1906S under George 3/MOP.

The use of complex data structures in most common languages is often unnecessarily confusing to all but the most experienced programmers. ATOL has been designed to include a variety of data structures in a way that is both simple to understand and easy to handle, yet sufficiently general and powerful for a wide range of applications. The syntax of the language is quite simple and suitable for interactive program development at on-line terminals, rather like Basic.The primary data type of the language is a character string or text. Three classes of data structures may be constructed: records, files and sequences. For each of these, the components may be either texts or other structures in any of the three classes. Records may be defined recursively to generate lists or trees of variable size. Arrays are not present in the language, their place being taken by files which are structures containing variable numbers of components selected by text keys. Data from a very wide range of applications may thus be easily and conveniently represented.The method used to denote the components of a structure in a program is significantly simpler than that used in languages like Algol 68 and Pascal. In addition, the need to use pointers explicitly has been kept to a minimum, thus reducing another source of confusion among inexperienced programmers. In general the language has been designed for the beginning programmer whose interests are in non-numerical applications such as occur in the arts and humanities and many areas of commercial data processing.