Skip to main content

Semantic descriptions library

These are my (current, evolving) contributions to a "library of semantics". This material is being extended when time and resources allow. (The work was initiated during the PLanCompS project.)

Formal descriptions of ALGOL-60

Thanks to painstaking work by Roberta Velykiene, the following scanned PDFs have an overlay which makes searching possible (even for Greek letters!)

We have written an Exegesis of these descriptions looking at how they tackled various issues such as basic approach (operational vs. denotational), syntax (concrete vs. abstract), abnormal sequencing, ability to mechanise, etc. Troy Astarte outlined this material at the Paris HaPoP meeting in 2016 and we are currently finalising the conference proceedings chapter.

VDM descriptions of programming languages

Those aspects of "VDM" relating to language description were firmed up in the IBM Laboratory in Vienna around a project to build a complier from the PL/I language to the "FS" machine (that got cancelled).

One direct output was "published" as the Technical Report on the PL/I description (Part I) and (Part II) which I've had scanned; (cite as).

Another report described the overall method (cite as).

An older report investigated different implementation techniques for reference to non-local variables (Warning: this uses VDL notation!) (full citation).

Other descriptions (follow the citation links to get to the pdf) using VDM include:

An interesting precursor of the shift to denotational semantics was a "functional semantics" written between my two stays in Vienna (1968-70, 1973-76)

  • This IBM Hursley Technical Report TR12.105 contains a semantics of ALGOL-60 (the standard challenge language). We decided to print (in Section 5) the ALGOL report on right-hand pages facing the relevant formulae on left hand pages; printed landscape!! The best approximation that I can give to this is to print two landscape pages above each other on A4. (A further warning is that since this was scanned, the pdf is over 5Mb.) Technically the material has some residual interest because it works out the "exit" idea in a framework that is related to Plotkin's SOS — but my notation was verbose. Linking in the other direction, having done this it was easy to absorb the "exit combinators" into the denotational VDM.

Related (Programming language description) VDM on-line resources

Books and chapters (follow the citation links to get to the pdf)

VDL Description of PL/I (ULD-III)

These 1960s Technical Reports from the IBM Laboratory Vienna comprise what was known as "ULD-III" and present a complete formal description of PL/I using the "Vienna Definition Language". There were three major versions of ULD-III in 1966, 1968 and 1969.

Version-I: Gerhard Chroust had the only copy that we could locate and he bravely allowed us to guilotine the spine so that we could make this scan available for which we are very grateful. It is interesting to observe the extent to which the VDL ideas were in place after a relatively short time. (The individual names of the autthors are given inside the document.)

Version-II which was kindly made available by Kees Pronk.

Version-III (this was kindly scanned by Callan Heard)

Scanned manuscripts

  • Two (two-part) drafts of Tony Hoare's "Axiomatic Basis"
  • Peter Aczel has kindly given me permission to make available two letters that he wrote to me when we were both in Computer Science at Manchester. Although Peter never sought to have them published, both letters are in my opinion scientifically important and certainly influenced my research.
    • In his letter from 1982, Peter gently chided me for the `unmemorable' proof rules in my 1980 book on VDM but clearly agreed with my emphasis on relational post conditions (this was certainly not the general approach in the 1980s) and felt it worth cleaning up the notation. This led to a complete rewrite of the book on the program development aspects of VDM: the book published in 1986 and its second edition in 1990 use Peter's form of the rules. Incidentally, Peter's note is the origin of the backhook used for the pre state in VDM post conditions.
    • The `Aczel traces' introduced in his On an inference rule for parallel composition had an even wider impact and are used in many discussions of interleaved concurrency for shared variable programs.
  • Martin Richards has kindly given me permission to make the CPL papers available on-line.
  • I happen to have an original (mimeographed?) copy of Bob Floyd's Assigning Meaning to Programs and have added a scanned copy because it shows the date of May 1966 which is the year before the normal citation (presumably the figure on page 3 is in Bob's own handwriting).
  • At least until Peter Mosses puts them on his own web site, the Reference manual for his SIS system and a collection of Worked and tested examples for his (Oxford) 1979 SIS system are here.

Related references

  1. Derek Andrews and Wolfgang Henhapl. Pascal. In Dines Bj{\o}rner and Cliff B. Jones, editors, Formal Specification and Software Development, pages 175–252. Prentice Hall International.
    View publication 
    @incollection{AndrewsHenhapl82,
  author = {Andrews, Derek and Henhapl, Wolfgang},
  crossref = {BjornerJones82},
  pages = {175--252},
  chapter = {6},
  title = {Pascal},
  url = {http://homepages.cs.ncl.ac.uk/cliff.jones/ftp-stuff/BjornerJones1982/Chapter-7.pdf},
  local-url = {file://localhost/Users/ncbj/Documents/Precious/cbj-WWW-pages/cliff.jones/ftp-stuff/BjornerJones1982/Chapter-7.pdf}
}
  2. Dines Bjørner and Cliff B. Jones, editors. Formal Specification and Software Development. Prentice Hall International, 1982.
    View publication 
    @book{BjornerJones82,
  editor = {Bj{\o}rner, Dines and Jones, Cliff B.},
  date-modified = {2007-09-21 07:09:59 +0100},
  isbn = {0-13-329003-4},
  length = {501 pages},
  publisher = {Prentice Hall International},
  title = {Formal Specification and Software Development},
  url = {http://homepages.cs.ncl.ac.uk/cliff.jones/ftp-stuff/BjornerJones1982},
  local-url = {file://localhost/Users/ncbj/Documents/Precious/cbj-WWW-pages/cliff.jones/ftp-stuff/BjornerJones1982/},
  year = {1982}
}
  3. D. Bjørner and O. N. Oest, editors. Towards a Formal Description of Ada, volume 98 of Lecture Notes in Computer Science. Berlin, 1980. Springer-Verlag. doi:10.1007/3-540-10283-3.
    View publication 
    @book{Bjorner80bis2,
  address = {Berlin},
  date-modified = {2007-09-23 13:57:35 +0100},
  doi = {10.1007/3-540-10283-3},
  editor = {Bj{\o}rner, D. and Oest, O. N.},
  local-url = {file://localhost/Users/ncbj/Documents/CBJ-Library/LNCS-98/},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Towards a Formal Description of Ada},
  url = {http://www.springerlink.com/content/t722165v4142/},
  volume = {98},
  year = {1980}
}

VDM for general program specification/design

See VDM.

Pointers to other sites

I'm keen to build a web of pointers to other interesting historical material; please e-mail me if you want me to add your URLs here.