This research aims to reduce the cost of special purpose and general purpose computer software by scientific publication of programs of high quality and general usefulness. Within the next twenty years, one would hope that quite substantial software systems could be purchased for no more than the price of a book which contains the documentation and source text.
There are hopeful signs that such an ideal may be technically achievable. For relatively small scientific subroutines, publication is an accepted method of dissemination. For larger nuclear codes, the Computer Physics Communications provides a means of dissemination. The Numerical Algorithms Group markets a large library of numerically sound algorithms. Unfortunately, the source text of these programs is not usually presented in a well-engineered form; it is only tested and not inspected by referees; and it is not adaptable to meet variable needs of its users. The investigators are discussing these problems with NAG.
In the longer term, they hope to show the way to publish non-numerical software of general utility, for example editors, peripheral controllers, word processors, filing systems, and perhaps even compilers and operating systems. These are most urgently required for low-cost computer systems, and local networks. Again, there are promising signs: personal computing magazines publish small-scale programs in low level languages. Stoy and Strachey's OS6 is designed for a personal computer, and was published in 1972. But the most spectacular recent development has been the UCSD PASCAL (TM) system, developed by Ken Bowles at the Institute for Information Science. This is written in PASCAL and provides support for PASCAL programming on microcomputers of the most widely available varieties. Although commercialisation prohibits publication of the complete source text, this system provides excellent support for execution of published applications programs written in PASCAL.
A very serious obstacle to the successful publication and use of non-numerical software is the absence of any consensus on its specification. In the case of trigonometric subroutines, it is generally agreed the objective is to compute a known single valued function of a single argument. In the case of a text editor, there is no such agreement on the functions to be provided or even on the number and types of their arguments and results. It seems that the computer industry must develop a tradition for publishing software specifications, preferably using some of the formal tools which are currently the subject of research and development.
For various reasons work on the grant did not effectively start until the beginning of 1979. Nevertheless some valuable preliminary work has been covered. The most tangible achievement has been the importation of the UCSD PASCAL (TM) system and its implementation on the DICOLL LSI-11. This software is now available to all investigators in the DCS program following the negotiation of a block licence agreement with Softech Microsystems Incorporated, the distributors of the system. Five DICOLL LSI-11 machines have now been installed at the Programming Research Group, and they are connected in a star network to a central printing and file server. In addition. a word processing system has been developed for a high quality low cost dot matrix printer.
Progress on the problem of program specification is necessarily less tangible. The investigators have started by considering a specification of a particular example, the editor described in Kernighan and Plauger's book Software Tools, which was published without any kind of specification. A formal specification has been constructed, using the methods of Denotational Semantics, which were pioneered at Oxford, and implemented by Peter Mosses under the name SIS. Considerable effort has been expended to reimport SIS back to Oxford on the Group's own computer. This has required the installation of extra storage and a consequential restructuring of the local operating system. When this is available. it is hoped that it will be used by a number of students for the rigorous specification of software products.
An alternative, more abstract, approach to program specification is taken by Professor Abrial. His methods are firmly based on logic and set theory. couched in a notation (Z) similar to that of a programming language. However, it is deliberately intended to be not executable by computer. Professor Abrial is currently an SRC visiting fellow with the Group.
In summary, the investigators are approaching the topic of software engineering from the high level of abstract specification and from the very low level of bit pushing protocols of microprocessors and cheap peripherals. The gap between these two approaches is distressingly wider than ever. It is the task of software engineering to span this gap in a reliable, efficient, and cost-effective fashion. To these criteria. the investigators have added a novel more difficult one - that all design decisions must be documented at publication standard. and that the eventual product should itself be published.
The main achievement of the project has been a new phase in the enhancement of Professor Abrial's specification notation (Z) and the application of the enhanced language to several large specification problems. The semantics of Z have been specified axiomatically [1] and a basic library of specification tools produced [2]. Initial responses to the work of the group (by Burstall, Horning, Jones and Schumann) indicate that it has provided additional insights into the problems and techniques of software specification.
Six specific applications of Z have been made to date [3][4][5] [6][7][8]; the applications are in a diversity of areas including word processing, concurrent systems, databases and semantics of programming languages.
The first application in which the group was involved [3] was to specify and implement a Computer Aided Visitor Information and Reception system (Caviar), basically a database, for Standard Telecommunications Laboratories Ltd. The group was given an informal specification of STL's requirements. In trying to formalise this specification they discovered a number of areas in which the informal specification was either incomplete or imprecise. This emphasised the utility of the process of formal specification as a tool in system design; without the attempt to formally specify the system, some of the inconsistencies in the informal specification might have been discovered after perhaps a substantial amount of effort had been invested in implementation.
Presentation of the specification to STL resulted in feedback on the database design which enabled the correction of those parts of the specification which did not match STL's requirements. Precise answers could be given to questions about the expected behaviour of the proposed database by reference to the formal specification rather than by arm-waving or educated guessing. A working prototype of a substantial subsystem was demonstrated in late April. The demonstration revealed that the precise operator interface to the database should have been specified. The effort involved in implementing a 'firm but friendly' user interface turned out to be considerably more than that involved in the implementation of the database kernel.
This project led to two major innovations in Z, the concept of class-function to overcome the burden of specifying state to state transitions and the join operators between classes, class functions and objects to permit the merging of independently specified subsystems.
The display interface paper [7] applies Z to the construction of a design of a display interface similar to that specified by Guttag and Horning who use algebraic axioms and predicate transformers. The purpose of this work was to show that the tools added to Z during the Caviar design and the methodology applied to the construction of Caviar are relevant to the specification of a system of an entirely different nature.
A second strand of the group's work has been the installation and adaptation of the UCSD Pascal(TM) system preparatory to the delivery of Cambridge Ring hardware.
Much work has been done on removing bugs from the system and building up tools for use under the system (eg software for the production of high quality documents containing formal mathematical notation on a Sanders printer). The fruits of this work will be made available to other participants in the DCS Programme.
Co-operation with the Engineering Science Department of the University is continuing. The purpose of the co-operative project is to investigate the feasibility of using the UCSD system to implement adaptive (self-tuning) controllers, suitable for real chemical processes.
The period has been one of consolidation of work done since September 1980. Feedback from a number of sources resulted in a decision to adopt a more compact and conventional mathematical notation [9]. This notation has been used to rewrite several of the specifications produced in 1980, some of which will be made available as monographs.
The notational retrenchment has had many positive results. Having removed the need to add language features whenever some difficulty in specification was encountered. it became possible to concentrate more on the theoretical questions underlying these difficulties. As a result it is now possible to give a consistent model for the class notation, which had formerly defied attempts at a formal semantics.
For the same reasons progress has been made on the foundations of an alternative style of specification, based on the construction of domains which model the histories of elements of an abstract type. This style of specification has proven to be useful for the gradual presentation of large-scale specifications. An example can be found in the papers on Caviar [[10], and the Reliable Filing System [11]. The mathematical foundation for the work, elaborated by Abrial in his forthcoming book, are summarised in [9].
Collaboration with Richard Miller of the University of Wollongong (Australia) who visited the Specification Group between January and June 1981 resulted in draft description of the Filestore Subsystem of the UNIX(TM) operating system [12].
Investigation of the possibilities of providing a proof checking system for the notation have been carried out with the cooperation of the LCF group at Edinburgh. The help given by Mike Gordon and Luca Cardelli is gratefully acknowledged.
Work on the specification of Distributed Systems continues. A component of a distributed system is specified by giving a description of its external connections - along which it can communicate with surrounding components, and a set of assertions involving the histories of the communications along these connecting channels. A collection of component specifications constitute a description of a distributed system, and reflects the decisions taken concerning distribution within a future realisation of the system.
Component descriptions have two purposes:
Ib Sorensen is pursuing this line of research in association with the Specification Group, and will complete his Doctoral Dissertation later this year.
Geraint Jones has been carrying out an investigation of specification techniques for time-critical processes. The main fruits of the work have been the definition of a small programming language and a method of reasoning about the performance of algorithms described in it.
The SLIK programming system - an implementation of a purely applicative Lisp-like language under the UCSD system written by John Hughes - has been distributed to several sites. It was made available to participants in the CREST Summer School on Functional Programming held in Newcastle during the summer of 1981.
The display editor which is formally specified in [13] has been distributed to several commercial and educational sites as a UCSD Pascal (TM) program.
Collaboration with the Engineering Science Department of the University on the implementation of Adaptive Control Algorithms continued until early this year. UCSD Pascal was chosen, and with the help of project members an interactive kernel was written to enable user interaction with the adaptive algorithm. The use of a polling-based rather than interrupt driven method of data retrieval meant that the entire system was implemented within Pascal. and will prove easy to maintain. The main defect in the system was the speed of operation. A sampling rate of half a second was the most which could be achieved within the framework of the (interpreted) UCSD system. This is adequate for many industrial processes, although a little too slow for the kind of analogue simulation techniques used in Engineering Science. For this reason the system has been reprogrammed in a compiler-based Pascal dialect.
The CAVIAR database specified and implemented for STL [3] has been delivered. As reported in 1980, the group want to assess the effectiveness of the formal specification as a maintenance document for the implementation. For this reason a member of STL's programming staff visited the group for training in the notation and methods of specification, and has taken over the maintenance of the system. The original specification has been rewritten so as to reflect the work of the specification group in the last twelve months [10]. It is still too early to report on this exercise.
Several MSc students chose projects in formal specification; noteworthy amongst these were:
Two research officers, B A Sufrin and Dr W-H Kaubisch are employed under this grant. Professor J-R Abrial was an SRC supported Senior Visiting Fellow for part of the duration of this grant. A number of research students and research fellows are engaged in this project.
During 1981, Cliff Jones and Christopher Kalus were awarded the degree of D.Phil.
Research staff associated with the project are now:
Research students associated with the project are:
Seminars have been given at the Universities of Essex, Warwick, Edinburgh, Queen Mary College, South-West Regional Computing Centre and to IBM and ICL.
1. J-R. Abrial, The Specification Language Z: Syntax and Semantics, Programming Research Group 1980.
2. J-R. Abrial, The Specification Language Z: Basic Library, Programming Research Group 1980.
3. J-R. Abrial, T. C. Clement, L. Sorensen, B. A. Sufrin, Specification of CAVIAR: a Computer-Assisted Visitor Information and Reception System, Programming Research Group 1980.
4. J-R. Abrial, An Attempt to use Z to Specify the Semantics of a Simple Programming Language, Programming Research Group, 1980.
5. J-R. Abrial, Specification of a Basic File Handler, Programming Research Group, 1980.
6. J-R. Abrial, Specification of some Aspects of a Simple Batch Operating System, Programming Research Group, 1980.
7. L. Sorensen, Specification of a Display Interface, Programming Research Group, 1980.
8. B. A. Sufrin, Specification of a Display Editor, Programming Research Group,1980.
9. B. A. Sufrin, Reading Formal Specifications, PRG Monograph Number 24, 1981.
10. J-R. Abrial, Specification of a Computer-aided Visitor Information System, Specification Group Working Paper, PRG, 1981.
11. J-R. Abrial, Specification of a Reliable File-Storage System, Specification Group Working Paper, PRG 1981.
12. Miller and Sufrin, Specification of the Unix(tm) Filing System, Specification Group Working Paper, PRG, 1981.
13. B. A. Sufrin, Formal Specification of a Display Editor, Programming Research Group Monograph Number 21, 1981.
14. C. B. Jones, Development Methods for Computer Programs including a Notion of Interference, D.Phil Thesis, Oxford University 1981.
15. C. Kalus, Applicative Programming and Data Processing, D.Phil Thesis, Oxford University 1981.
The project is an investigation into the application of purely functional programming languages, in particular Henderson's Lispkit Lisp [1], to the design and implementation of computer operating systems. It is intended that such operating systems will be physically distributed over a small collection of microprocessors, each microprocessor providing an independent and well defined service within the operating system. The collection of processors will be integrated by a simple communications network to give a powerful single system. Functional programming languages are good candidates for designing such systems for several reasons. They are well suited to the task of describing the behaviour of independent processes which communicate with their neighbours by message passing along serial channels. Their mathematical simplicity and rigid programming discipline enables rapid developments of reliable software.
The investigations in this project have yielded an understanding of the functional programming style in an important field of applications. Operating systems are clearly a vital component of future computer systems, and the application of functional programming should provide indications as to how such systems may be simplified in structure, and hence be developed more easily, and made more reliable. In order to focus attention it is intended that a long term goal will be to implement, in a functional style, a complete system to support a programmer who wishes to develop functional programs. Research on this topic is continuing with support from ICL.
Several prototype mini-operating systems have been developed in Lispkit Lisp which execute interactively on the single processor implementation described above. These range from simple systems described by Henderson [2], and other similar systems designed around the concept of communicating processes, to rather different systems inspired by the Unix concepts of shells and pipes. These experiments suggest that there are many more interesting operating systems to be designed which are at the same time simple yet very powerful. The experiments are also forcing a detailed consideration of techniques for handling important problems such as non-determinism, concurrency, and processes with multiple input and output streams. This experience has been an essential contribution to the redesign of the Lispkit Lisp implementation which now enable it to support the operating system components executing at each node of the microprocessor network.
In order to be able to define operating systems which execute a number of concurrent processes it was necessary to extend the programming language Lispkit Lisp with a non-deterministic form of expression. The basic form of this expression as currently used allows two concurrent processes to be commenced and for the termination of one of them to discard the other. This is adequate to define the sorts of concurrency needed to be able to define even quite general multi-programming environments. The process of deciding how this language primitive can be packaged for presentation to more general users is still being resolved. It is fully described in [3]. The necessary extensions to the abstract machine are reasonably straightforward. This is a result of some significance, and one which the group intend to take fullest advantage of in subsequent research.
A second operational problem which has been solved concerns the need for communication among functional programs when a network of processors is involved. Simple interactive functional programs are defined as functions from one input stream (the keyboard, say) to one output stream (the screen, for example). When a functional program must communicate with more than one user, or with a mixture of users and other machines, it is necessary to have many input and output streams. Various solutions were investigated. Finally it was decided upon. and has been implemented, a scheme whereby the program is a function from a tuple of streams to a tuple of streams. The details of this solution are also reported at length in [3] as are the necessary extensions to the abstract machine.
Armed with these completed developments the project is now into the final stage as originally proposed, being able to demonstrate a simple two machine file transfer system using two Perqs back to back using an RS232 link. These experiments are in the process of being repeated using other machines available in greater multiplicity. The results of these experiments along with others carried out on a single processor will be reported on shortly. Experiments on the single processor have been to demonstrate that Lispkit Lisp is adequate for writing operating system shells, notwithstanding that it is a purely functional language.
In this project concentration has been on the provision of basic machine and language facilities for defining operating systems. The group have become increasingly aware that. while they have validated their conjecture that they can write operating systems in purely functional style there are many other applications which would benefit from similar developments. It is believed that a system has been produced which will allow the investigations to move on to study the use of functional programming for a wider range of applications.
In order to encourage and promote the study of functional programming the Lispkit Lisp implementation and associated software tools are available for distribution to interested researchers. The implementation is available for PERQs, for Intel 8086 (or Intel 8088) based computers, for Motorola 68000 based computers, and for the VAX [4]. In addition a reference implementations in Pascal and C are available.
1. P. Henderson, Functional Programming: Application and Implementation, Prentice-Hall International. 1980.
2. P. Henderson, Purely Functional Operating Systems, in Functional Programming and its Applications, Cambridge University Press 1982.
3. S. B. Jones, Abstract Machine Support for Purely Functional Operating Systems, Programming Research Group Technical Monograph. PRG-34, Oxford, 1983.
4. P. Henderson. G. Jones and S. B. Jones, The Lispkit Manual, (two volumes) Programming Research Group Technical Monograph, PRG-32, Oxford. 1983.
The availability of inexpensive computing power has made it economically attractive to construct computer systems from physically discrete interacting components. Such distributed systems require
The Oxford Distributed Computing Project addresses the second requirement. The latest software engineering techniques are used to aid in specification and design, and to avoid preconceptions inherent in traditional computing environments which are less relevant for modern technology.
Formal specification provides a framework in which software designs may be proposed and partly evaluated in advance of (even a prototype) implementation. The project uses a specification technique drawn almost entirely from classical mathematics; this allows great freedom in the exploration of new software designs. It is intended that the distributed system be accompanied by a specification which can be published independently of its implementation, and that the specification be precise and clear enough to allow, for example, independent supply of the system's components (interworking). The specification could also serve as an effective national or international standard of high quality.
Progress has been made in several areas. Firstly, an experimental device service [1] has been provided which acts as a distributed extension of the UCSD P-system. Secondly, experience has been gained by the project staff with specification techniques [2] and some progress has been made in improvement of them. Thirdly, the design of classes of distributed system service has been explored and implementable services have been specified. Two services in particular, one for providing low-level disc storage [5], and the other for providing spooling to a printer [6], have been both specified and implemented. Further work has been done on the rigorous specification of communication protocols.
In the coming year, the provision of services will be extended towards a higher-level filing system and the mail facilities (see [3] [4] for example specifications of services of these kinds), as well as archiving, logging and accounting services. There is much collaboration in matters of specification with members of the Software Engineering project, and good contact with visitors from industry.
The eventual publication of a distributed system specification will make the design's applicability largely hardware independent; conformance to the design will allow interchangeability of components (whether supplied by manufacturer or by user).
1. A. Newman, An Experimental UCSD Device Service for the Cambridge Ring, Programming Research Group, February 1982.
2. C. Morgan, Specification of a Communication System, Proceedings of the International Conference on Synchronisation, Communication and Control in Distributed Computer Systems, Polytechnic of Central London, 20-24 September 1982, Academic Press.
3. B. Sufrin, Formal Specification of an Automated Mail System, Programming Research Group Internal Report, April 1982.
4. C. Morgan and B. Sufrin, Specification of the UNIX Filing System, IEEE Trans. Software Engineering.
5. A Block Storage Service, Programming Research Group Internal Report, May 1983.
6. A Printing Service, Programming Research Group Internal Report, July 1983.
