ABSTRACT. In their first report on Planning and Coding Problems for an Electronic Computing Instrument, issued in 1947, Herman Goldstine and John von Neumann proposed a notation they called flow diagrams. These diagrams did not simply provide a graphical representation of the “control flow” in a program, but were part of a detailed and comprehensive approach intended to reveal “errors and omissions” in program plans.

Thanks to the preservation of a little-known draft version of the report and correspondence between Goldstine and von Neumann, the evolution of the notation can be traced in some detail. A persistent theme within the development was the attempt to find an adequate way of describing the behaviour of iterative loops in programs. I will trace the outline of this history, paying particular attention to those aspects of the notation that were used to check the correctness of the program being designed.

The Planning and Coding reports contain a number of textbook examples of the use of the notation, and in 1949 Alan Turing used a flow diagram to illustrate a process for “checking large routines”. A comparison of Turing’s diagram with the Goldstine/von Neumann notation reveals many similarities, but also a significant difference.

However, in practice the use of the notation moved away from an explicit concern with correctness. As far as we know, the first application of the notation “in the wild” was for the Monte Carlo programs run on ENIAC in early 1948. Examination of the flow diagrams produced for this project, some produced by von Neumann himself, show that the notation quickly evolved from its textbook form into a less detailed version that emphasized program structure at the expense of detailed annotation of the properties of data. The presentation will conclude by considering some factors that may have contributed to this change.

ABSTRACT. We trace the roots of Abstract Interpretation and its role as a fundamental theoretical framework to understand and design program analysis and program verification methods.

Starting from the historical roots of program verification and formal methods, form A.M. Turing to C.A.R. Hoare, we show how abstract interpretation fits this mainstream in perfect continuity and how this theory shaped the literature and the practice in program analysis in the last 40 years, providing powerful tools for designing static program analyzers, automatic verifiers of software/hardware systems, type systems, security protocol analyzers, and algorithms for formal languages.

The top 5 most cited articles at ACM POPL include three articles on abstract interpretation, in particular the most cited article, which according to Google scholar has more than 7000 citations. We then will trace the beginning of its industrialization form the very first systematic use in verification of embedded systems to the nowadays wide spread use in high-end static program analysers.

Noteworthy examples include: (1) the Polyspace static analyzer for C/C++ and Ada programs has been fully conceived and designed by abstract interpretation and is successfully commercialized by TheMathWorks (2) Astree is a C static analyzer based on abstract interpretation, conceived and designed by Patrick and Radhia Cousot’s research group at ENS Paris, marketed by AbsInt GmbH (Germany), and used in the defense/aerospace (Airbus, Honda), electronic (Siemens), and automotive industries (Daimler); (3) Infer is a static analysis tool for detecting memory and concurrency bugs in Java/C/C++/Objective-C code, developed by Facebook, based on abstract interpretation and routinely used by Facebook software engineers.

We will survey the birth and evolution of abstract interpretation starting from the celebrated Cousot-Cousot's POPL77 paper and landing, through a 40+ years journey, to the current state-of-the-art of this research discipline. We will also give some personal hints on the main future challenges faced by abstract interpretation research.

ABSTRACT. The specification language B and its successor Event-B are used for the formal development of software and systems following the correct-by-construction approach. Both are based on first order predicate logic with higher-order sets, relations, functions.

B has originally been developed as a successor to Z by Jean-Raymond Abrial in the 1990s, focusing on two key concepts: using refinement to gradually develop models and tool support for proof and model checking. There are three classes of industrial applications of B: - B for software (classical B) [1]: refine specifications until B0, a low-level subset of B, is reached and apply code generators - B for system modelling (Event-B) [2]: verify critical properties, understand why a system is correct - B for data validation: express properties in B and check data (possibly using a double chain)

In our article, we will first give a primer on B and Event-B, introducing the main language features and how they are used. Afterwards, we will describe the history of B, starting with B's genesis as a tool for software validation [3, 4], discussing industrial applications of B in projects such as train speed control [5] and signalling [6] and other projects with RATP and SNCF performed by Alstom, Line 14 (Meteor) [7] or Canarsie [8]. Following, we will focus on the evolution of B into Event-B and from software to systems modelling, again focusing on industrial applications such as the flushing line NY [9], OCTYS [10], GIK/Railground [11], the HL3 standard [12] and cooperations with Peugeot. Additionally, we will discuss ventures of using B in other domains such as smart cards [13, 14].

The latest language evolution, B for data validation will be presented by discussing its use for Paris Line 1 [15] and the (subway) trains in Barcelona, Amsterdam, Calcutta, Cairo, Singapore and many more locations.

Language evolution aside, we want to discuss tool evolution in the B ecosystem. Both B and Event-B are supported by a range of tools, from provers to animators to model checkers. We want to give an overview over the B-method tools currently in use and their development and history, starting with early tools such as the B-Toolkit [16] to Atelier-B [3] and to Rodin [17] for Event-B. As not all tools are still available, we will also discuss the ones that disappeared or never really appeared.

In addition to industrial success stories, the academic reception of the Bmethod and its tools is notable as well and will be a distinct part of the article. Starting with the B User Workshop, to the ZB conference and further to the ABZ conference series, which brings together researchers working on different specification languages.

Switching from history and evolution to outlook, we want to discuss new language features such as extensions to Event-B and Rodin, and the extended classical B as understood by ProB. Furthermore, we intend to discuss new areas of application both for B as a language as well as for the B-method tools.

ABSTRACT. Dramatis personae

To simplify the narrative, we use initials to refer to key players and organisations.

AG Alena Griffiths DC David Carrington DD David Duke GR Gordon Rose GS Graeme Smith JSD Jin Song Dong OTC Overseas Telecommunications Commission, Australia PK Paul King RD Roger Duke UQ University of Queensland, Australia

The end of the 1980's saw a growing interest in object orientation as both a design and programming methodology with the advent of programming languages like C++ and Eiffel. The trend was taken up by some in the formal methods community, including a team of researchers in Australia. Their contribution was a formal specification language, Object-Z, which had immediate industrial impact, gained rapid international recognition, and then two decades later began to fade, along with some of its contemporaries, from the formal methods scene.

The seed from which Object-Z grew was a comment from a software engineer in industry: why couldn't a Z specification (that UQ was developing for OTC) be structured to make it easier to read; in particular, why couldn't it be structured like C++? This was in 1988. The engineer was working for OTC developing the specified system in C++. The recipient of the comment was GR, who a few days later called together RD and GS and showed them his idea for what became an Object-Z class. Over the next year, GR, RD and GS were joined by DC, DD and PK in defining the first version of Object-Z. GS rewrote the specification of the OTC system and, along with RD, attempted to verify (by hand) its critical properties. Doing this, they discovered two errors in the design. OTC was deeply impressed. Object-Z was a success and funding for it continued until OTC was merged with Telecom Australia in 1992.

By that time, DD and GS had completed PhDs on Object-Z. DD's thesis provided a denotational semantics based on `histories' which formed the basis of future work on the integration of Object-Z with other formalisms such as CSP. These PhDs were followed, throughout the 1990's, by several others on applications and further developments of Object-Z. Perhaps the most controversial development was to give Object-Z a reference semantics. GR and RD argued this would make it easier to translate Object-Z to programming languages like C++. GS argued that it would unnecessarily complicate reasoning. However, the decision was made and a new PhD student, AG, was given the task of defining the reference semantics. Another PhD student, JSD, added a number of features based on this semantics including self and mutually recursive classes.

By the mid-1990's, Object-Z was appearing in publications from outside of UQ. The number of such publications grew over the next decade and a half: on a webpage that GS maintained until 2004 there were 59 such publications. Since then interest has noticeably waned. It is interesting to reflect on why this is the case and, in particular, to compare Object-Z's fate with that of other specification languages of the time.

ABSTRACT. One division of concurrency thinking is between shared-variable and communication-based approaches. This abstract sketches a DAG of connections (with [n] referring back to the nth list item) on the former topic (our planned research will cover the latter which intertwines with the points below; also Temporal Logic research is for future work).

Perhaps the root of the directed graph should be challenge problems because these have been extremely stimulating: Dijkstra was a master (e.g. “Dining Philosophers”); Owicki’s “Find”, Hoare’s “Sieve of Eratosthenes”, the “Fisher/Galler algorithm” and Simpson’s “Four-slot” deserve special mention.

1. Hoare’s 1969 Axiomatic Basis [Hoa69] established a clear approach to constructing proofs of sequential imperative programs.
2. Hoare’s Proof of FIND [Hoa71] pointed the way to a development method for such programs [Obviously 1]. For sequential programs, Apt’s [Apt81] looks at the first decade of Hoare’s logic and [Jon03] traces the move to development methods.
3. After his seminal 1969 paper on sequential programs [1] Hoare looked at extending the approach to parallel programs. In a 1971 paper [Hoa72] it is shown that it is possible to prove that a collection of parallel non- interfering threads satisfy specifications that are the conjunction of the pre/post conditions of its constituent threads. That paper treated the situation where all variables were stack variables.
4. There are many “inventions” of the idea of data abstraction and development by “reification” or “refinement” — initial examples were for sequential programs.
5. Susan Owicki’s 1975 thesis [Owi75] (and a joint paper with her PhD supervisor Gries [OG76]) made a key step in reasoning about shared-variable concurrent programs: the basic idea is to construct separate Hoare-style [1] proofs of all threads under the assumption that there is no interference and to follow this by showing, for each thread T_i, that the the sibling threads do not interfere with the proof of T_i. De Roever’s 2001 book classes [dR01], the Owicki/Gries approach [5] as non-compositional because failure to discharge their final “einmischugsfrei” proof obligation can result in needing to redo the development.
6. 1981 research on Rely/Guarantee (R/G) conditions [Jon81] offers a compositional development method for shared-variable concurrent programs by adding explicit rely and guarantee conditions to Hoare-like pre/post conditions. [1, 2]. It slowly emerged that data abstraction/reification [4] were intimately involved.
7. (Although material on Temporal Logic is planned future work, the 1984 paper by Barringer/Kuiper/Pnueli “Now You Can Compose Temporal Logic Specifications” is an intriguing link to [6]).
8. Reynolds’ Separation Logic in [Rey00] tackled the delicate issue of reasoning about (sequential) programs that use heap variables. [1]
9. In conjunction with others (there’s a nice history paper) O’Hearn developed Concurrent Separation Logic [O’H07] from [8] to reason about concurrent programs that share heap variables. CSL introduces a separating conjunction that, in a sense, carries forward the idea from Hoare’s approach [3]; although dealing with the trickier case of heap variables, separating conjunction formalises rules for when it is valid to conjoin pre and post conditions of separate threads. Another way of looking at CSL is that it is actually a logic of ownership which is important because the ownership of heap locations can pass between threads.
10. Vafeiadis’ RGSep [Vaf07, FFS07] and Feng’s SAGL are serious at- tempts to combine [6] and [9] formally. Furthermore, a friendly rivalry/cooperation exists between researchers working on R/G [6] and CSL [9] with five papers on Simpson’s algorithm alone — in fact, Bornat uses a combination of the ideas (plus “linearisability”).

Currently: research on Views promises a common way of showing property-oriented methods to be sound; recent developments on recasting R/G methods have led to pleasing and useful algebraic presentations. [Hay16, HJ18].

References

[Apt81] Krzysztof R. Apt. Ten years of Hoare’s logic: a survey—part I. ACM Transactions on Programming Languages and Systems, 3(4):431–483, October 1981.

[dR01] Willem-Paul de Roever. Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, 2001.

[FFS07] Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP: Programming Languages and Systems, pages 173– 188. Springer, 2007.

[Hay16] I. J. Hayes. Generalised rely-guarantee concurrency: An algebraic foundation. Formal Aspects of Computing, 28(6):1057–1078, November 2016.

[HJ18] I. J. Hayes and C. B. Jones. A guide to rely/guarantee thinking. In Jonathan Bowen, Zhiming Liu, and Zili Zhan, editors, Engineering Trustworthy Software Systems – Second International School, SETSS 2017, LNCS. Springer-Verlag, 2018.

[Hoa69] Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, 1969.

[Hoa71] Charles Antony Richard Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39–45, January 1971.

[Hoa72] C. A. R. Hoare. Towards a theory of parallel programming. In Operating System Techniques, pages 61–71. Academic Press, 1972.

[Jon81] C. B. Jones. Development Methods for Computer Programs including a Notion of Interference. PhD thesis, Oxford University, June 1981. Printed as: Programming Research Group, Technical Monograph 25.

[Jon03] Cliff B. Jones. The early search for tractable ways of reason- ing about programs. IEEE, Annals of the History of Computing, 25(2):26–49, 2003.

[OG76] S. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319–340, 1976.

[O’H07] Peter O’Hearn. Resources, concurrency and local reasoning. (accepted for publication in) Theoretical Computer Science, 2007.

[Owi75] S. S. Owicki. Axiomatic Proof Techniques for Parallel Programs. PhD thesis, Department of Computer Science, Cornell University, 1975. Hard copy - Published as technical report 75-251.

[Rey00] J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Jim Davies, Bill Roscoe, and Jim Woodcock, editors, Millennial Perspectives in Computer Science, pages 303–321, Houndsmill, Hampshire, 2000. Palgrave.

[Vaf07] Viktor Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, 2007.

ABSTRACT. This is a proposed talk, not a paper

Berry weaves the twin peaks of (1) his life in computing, programming, programming languages, formal methods, software engineering, electronic publishing, and requirements engineering with (2) the almost concurrent development of programming languages, software engineering, and requirements engineering.

The focus in this presentation will be on his participation in formal methods, how it stimulated his eventual move to requirements engineering at the same time he was becoming more and more disillusioned about the usefulness and effectiveness of formal methods.

ABSTRACT. This talk will report the history of ideas and the main advances in the domain of software testing based on formal specifications. Going back to the seventies, being a bit caricatural, software testing was perceived, on the one hand, by its actors as an empirical activity that had nothing to gain from formal methods, on the other hand, by the advocates of these methods as doomed to disappear since in the long run programs will be correct by construction… At the date of this workshop, these two communities do not yet reach a complete consensus. But fortunately there have been some significant moves from both sides and various success stories that allow saying that there is a fruitful convergence toward testing methods based on formal specifications. Sound and effective testing methods have been established based on various types of formal specifications, leading to tools for assisting the testing process. A comprehensive survey can be found in [Hierons et al. 2009].

In the seventies and before, most works in the area were based on finite state machines, an approach inspired by circuit testing, then applied to software [Chow 78] and later on widely developed and extended for conformance testing of communication protocols, as surveyed in [Lee and Yannakakis 1996]. A notable exception is the foundational paper by Goodenough and Gerhart in 1975 where the importance of “all the conditions relevant to the correct operation of a program”, namely its logical specification, was pointed out, and the derivation of test cases from such specifications, was introduced.

This approach developed slowly during the eighties for various kinds of formal specification languages [Gannon McMullin 81], [Jalote 83], [Bougé et al. 86], [Hall 88], [Brinksma 88] despite the recurrent questions on the interest of testing pieces of software that have been formally specified and proved correct w.r.t. their specifications.

In the nineties, however, several well founded methods often validated by prototypical tools and convincing case studies provided evidence of the interest of the approach. One can mention (among many others) [Bernot Gaudel Marre 1991] and [Gaudel 1995] for algebraic specifications, [Dick Faivre 1993] for VDM, [Carrington Stocks 1994] for VDM, etc. This led to important research projects resulting in exploitable testing environments such as TGV, BZ, Asm, Z (SANTEN 97, Hierons 97), TorX, GATEL, etc Since the beginning of the 21th century such tools and methods have greatly benefited of advances in the areas of constraint solvers [de Moura Bjorner 2008], symbolic evaluation [Cadar et al.], theorem provers [Brucker Wolff 2012], and of the increasing acceptance of formal methods in industrial projects.

References

1. R. M. Hierons, K. Bogdanov, J. P. Bowen, R. Cleaveland, J. Derrick, J. Dick, M. Gheorghe, M. Harman, K. Kapoor, P. Krause, G. Luttgen, A. J. H. Simons, S. Vilkomir, M. R. Woodward, and H. Zedan, Using formal specifications to support testing, ACM Comput. Surv. 41(2), 1-76, 2009.
2. T. Chow, Testing software design modeled by finite-state machines, IEEE Trans. on Software Engineering, SE-4(3):178187, 1978.
3. D. Lee and M. Yannakakis, Principles and methods of testing finite state machines—a survey, Proceedings of the IEEE, 84(8):1090-1123, 1996.
4. J. B. Goodenough and S. L. Gerhart, Toward a theory of test data selection, IEEE Trans. on Software Engineering, SE-1(2): 156-173, 1975.
5. J. Gannon, P. McMullin and R. Hamlet, Data Abstraction, Implementation, Specification, and Testing, ACM Trans. Program. Lang. Syst.,3(3):211-223, 1981.
6. P. Jalote, Specification and Testing of Abstract Data Types, COMSAC83, pp. 508- 511, 1983.
7. L. Bougé and N. Choquet and L. Fribourg and M.-C. Gaudel, Test set generation from algebraic specifications using logic programming, Journal of Systems and Software, 6(4): 343-360, 1986.
8. P.A.V. Hall, Towards testing with respect to formal specification, Second IEE/BCS Conference: Software Engineering, pp.159 - 163, 1988.
9. E. Brinksma, A theory for the derivation of tests, in: Protocol Specification, Testing, and Verification, VIII, North-Holland, 1988, pp. 63-74.
10. 10. G. Bernot, M.-C. Gaudel, and B. Marre, Software testing based on formal specifications: a theory and a tool, Soft. Eng. Journal, 6(6):387-405, 1991.
11. Gaudel, M.-C., Testing can be formal, too, TAPSOFT’95, LNCS 915, pp. 82-96, 1995.
12. J. Dick and A. Faivre, Automating the generation and sequencing of test cases from model-based specifications, LNCS 670, pp. 268-284, 1993.
13. Ph. Stocks, D.A. Carrington, Test Templates: A Specification-Based Testing Framework. ICSE 1993: 405-414
14. E. Brinksma and J. Tretmans, Testing Transition Systems: An Annotated Bibliography, LNCS 2076, 187-195, 2001.
15. L. De Moura and N. Bjørner. Z3: An efficient SMT solver, LNCS 4963, 337-340, 2008.
16. C. Cadar, P. Godefroid, S. Khurshid, C. S. Pasareanu, K. Sen, N.Tillmann, and W. Visser, Symbolic execution for software testing in practice: preliminary assessment, ICSE ’11, 1066-1071, 2011.
17. A. D. Brucker and B. Wolff, On Theorem Prover-based Testing, Formal Aspects of Computing, 25(5):683-721, 2013.

ABSTRACT. Charles Babbage (1791-1871) was Lucasian Professor of mathematics in Cambridge from 1828-1839. He displayed a fertile curiosity that led him to study many contemporary processes and problems in a way which emphasised an analytic, data driven view of life.

In popular culture Babbage has been celebrated as an anachronistic Victorian engineer. In reality, Babbage is best understood as a figure rooted in the enlightenment, who had substantially completed his core investigations into `mechanisation of thought' by the mid 1830s: he is thus an anachronistic Georgian: the construction of his first difference engine design is contemporary with the earliest public railways in Britain.

A fundamental question that must strike anybody who examines Babbage's precocious designs is: how could one individual working alone have synthesised a workable computer design, designing an object whose complexity of behaviour so far exceeded that of contemporary machines that it would not be matched for over a hundred years?

We shall explore the extent to which the answer lies in the techniques Babbage developed to reason about complex systems. His Notation which shows the geometry, timing, causal chains and the abstract components of his machines, has a direct parallel in the Hardware Description Languages developed since 1975 to aid the design of large scale electronics. These modern languages typically have a geometry facet in which the arrangement of electronic components in space is specified; a register transfer facet which emphasises the interconnection of functional units and registers; and a behavioural facet which describes sequences as state machines or in software-like notations. The interlaced facets present different abstractions to the design engineer: the separation of concerns underpins our ability to design complex systems. Babbage's notation has a 'trains' facet which captures the chain of cause and effect within a system, a timing facet which displays state and a 'forms' facet which shows geometry.

In this presentation, we shall provide a basic tutorial on Babbage's notation showing how his concepts of 'pieces' and 'working points' effectively build a graph in which both parts and their interactions are represented by nodes, with edges between part-nodes and interaction-nodes denoting ownership, and edges between interaction-nodes denoting the transmission of forces between individual assemblies within a machine. We shall give examples from Babbage's Difference Engine 2 (DE2) for which a complete set of notations was drawn in 1849, and compare them to a design of similar complexity specified in 1987 using the Inmos HDL.

We shall show that early drafts of the DE2 notations use hierarchy to manage complexity. We shall discuss whether Babbage's notation is sufficiently formal and complete to allow symbolic simulation of a system such as DE2. We shall conclude by examining the role of abstraction in Babbage's design process, with special reference to Reuleaux's 1976 criticism of Babbage's notation that 'It is at once evident, however, that under this system mechanisms of completely different constructions might be represented by one and the same set of symbols'.

ABSTRACT. In 1962, IFIP formed Working Group 2.1 to design a successor to the seminal algorithmic language Algol60 [1]. WG2.1 eventually produced the specification for Algol68 [2]—a sophisticated language, presented using an elaborate two-level description notation, which received a mixed reception. WG2.1 continues to this day; technically, it retains responsibility for the Algol languages, but practically it takes on a broader remit under the current name Algorithmic Languages and Calculi. Over the years, the Group has been through periods of focus and periods of diversity. But the period of sharpest focus covered the decade from the mid 1980s to mid 1990s, when what became known as the Bird-Meertens Formalism (BMF) drew the whole group together again. It is the story of that decade that I wish to tell.

BMF arose from the marriage of Bird’s work in recursive programming [3, 4] and Meertens’ efforts in designing the simple accessible programming languages B [5] and ABC [6]. (Meertens taught Guido van Rossum, who went on to design Python based on some of the ideas in ABC.) The motivation for the BMF is transformational programming: developing an efficient program by starting with an obviously correct but possibly hopelessly inefficient initial specification, then applying a series of meaning-preserving transformations to yield an extensionally equivalent but acceptably efficient final program. The essence of the formalism is a concise functional notation. The functional approach ensures referential transparency, and the straightforward manipulation technique of substitution of equals by equals, as in high school algebra. Concision is necessary in order to make such manipulations feasible with just pen and paper; in particular, like APL, BMF embraced funny symbols such as a slash for reduction (+/ sums a sequence of numbers) and banana brackets ([...]) for homomorphisms, which led to the notation being nicknamed Squiggol. Little emphasis was placed on executability: the notation was ‘wide-spectrum’ [7], accommodating convenient specification notations such as inverses and intersection as well as a sublanguage that obviously corresponds to executable code.

The BMF research paradigm consisted of establishing a body of theorems about recurring problem structures and corresponding solution techniques. Typical examples are fusion properties (combining two traversals over a data structure into one), scan lemmas (replacing the independent reduction of each initial segment of a sequence with a single accumulation along the sequence), and Horner’s Rule (exploiting distributivity, as for products over sums in polynomial evaluation). These three formed the core of a beautiful derivation of a linear-time solution to the Maximum Segment Sum problem [8], a central example in the BMF canon. The effort culminated in Bird and de Moor’s book The Algebra of Programming [9], with a collection of theorems expressed in a relational notation providing greedy and dynamic-programming solutions to optimization problems.

WG2.1’s passion for the approach started to fade after Bird and de Moor’s book appeared, and the group’s focus diversified again. Partly this was due to falling out of love with the Squiggolly notation, which may be convenient for aficionados but excludes the unfamiliar reader; later work favours more conventional syntax. It was also partly due to dissatisfaction with the relational approach, which seems necessary for many optimization problems but is too complicated for most readers (and even for writers!); in fact, Bird is returning in a forthcoming book to tackling many of the same optimization problems using a nearly completely functional approach. I hope to pick out some of the lessons from this ebb and flow of enthusiasm.

References

1. John W. Backus, Friedrich L. Bauer, Julien Green, C. Katz, John McCarthy, Alan J. Perlis, Heinz Rutishauser, Klaus Samelson, Bernard Vauquois, Joseph Henry Wegstein, Adriaan van Wijngaarden, and Michael Woodger. Report on the algorithmic language ALGOL 60. Communications of the ACM, 3(5):299–314, 1960.
2. A. van Wijngaarden, B. J. Mailloux, J. E. L. Peck, C. H. A. Koster, M. Sintzoff, C. H. Lindsey, L. G. L. T. Meertens, and R. G. Fisker. Revised report on the algorithmic language Algol 68. Acta Informatica, 5(1–3):1–236, 1975. Also appeared as Mathematical Centre Tract 50, CWI, Amsterdam, and published by Springer Verlag in 1976.
3. Richard S. Bird. Notes on recursion elimination. Communications of the ACM, 20(6):434–439, 1977.
4. Richard S. Bird. Improving programs by the introduction of recursion. Communications of the ACM, 20(11):856–863, November 1977.
5. Lambert G. L. T. Meertens and Steven Pemberton. Description of B. SIGPLAN Notices, 20(2):58–76, 1985.
6. Leo Geurts, Lambert Meertens, and Steven Pemberton. The ABC Programmer’s Handbook. Prentice-Hall, 1990. ISBN 0-13-000027-2.
7. F. L. Bauer, R. Berghammer, M. Broy, W. Dosch, F. Geiselbrechtinger, R. Gnatz, E. Hangel, W. Hesse, B. Krieg-Brückner, A. Laut, T. Matzner, B. Möller, F. Nickl, H. Partsch, P. Pepper, K. Samelson, M. Wirsing, and H. Wössner. The Munich Project CIP, Volume 1: The Wide-Spectrum Language CIP-L, volume 183 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1985.
8. Richard S. Bird. Algebraic identities for program calculation. Computer Journal, 32(2):122–126, April 1989.
9. Richard Bird and Oege de Moor. Algebra of Programming. Prentice-Hall, 1996.

ABSTRACT. This contribution aims to present an archival study carried out in the Braga District Archives (ADB) of a fund related to the activity of Professor Willem van der Poel as Chairman of IFIP Working Group 2.1. This fund was entrusted to ADB in late 2017, via a protocol with IFIP WG 2.1.

The material spans over a period of time which, starting in the second half of the twentieth century, witnesses significant advances in computer programming as a scientific body of knowledge: the spread of the Algol family of programming languages. For archivists with little background in computer programming, handing this fund was a challenging exercise. The archival process that gave on-line access to this collection [1] ranged from treatment of the documentation itself to its archival formal description and digital preservation (document scanning).

The formal description followed two international standards: the General International Standard Archival Description [2]; the International Standard Archival Authority Record for Corporate Bodies, Persons and Families [3]. Both are issued by the International Council on Archives (ICA).

These standards are very important for archival description, normalization and dissemination because they rely on scientific procedures which, in this particular exercise, unveiled not only the organic aspects of IFIP, of its Technical Committee TC2 and the WG 2.1 group, but also the relationship between such institutions and main protagonists such as Heinz Zemanek, Nikolas Wirth, and several others. In particular, the idea of "assigning meanings to programs" arises in letters and other documents circulating within the group in the mid-1960s, thus already contributing to the body of knowledge today known as "formal methods".

Altogether, the authors intend to demonstrate how normalized archival procedures can help in laying out the historiography of the origins of programming science and formal methods, through the careful identification of document archival series such as meeting minutes, meeting processes, correspondence, proposals, technical notes, reports, resolutions, management support documents, news in newspapers, and so on.

We would like also to discuss how to interface ADB’s Willem van der Poel's fund with other collections, namely the Software Preservation Project, the Brian Randell Collection (Newcastle, UK) and Andrei Ershov (web) archives.

Last but not least, the authors would like to raise the issue of digital preservation. Nowadays, IFIP WG2.1 information and work-flow don’t rely on physical paper anymore. What are the challenges in preserving the last (say) 20 years’ bulk of emails, text source files (written in a myriad of different, constant evolving editors), PDF (and also PS) files, websites and so on, when compared to the “classic” archival techniques applied to van der Poel’s collection? How “trustful” is a mailbox file stored in a personal computer compared to a folder of yellowish papers? Moreover, can archival standards and principles be applied to software itself? In the parallel, programming languages such as Algol can perhaps be compared to Latin: a language that open-sourced others through a process of transformation and refinement, leaving its marks there.

References

1. http://pesquisa.adb.uminho.pt/details?id=1619260
2. https://www.ica.org/en/isadg-general-international-standard-archival-description-second-edition
3. https://www.ica.org/en/isaar-cpf-international-standard-archival-authority-record-corporate-bodies-persons-and-families-2nd