DESIGN AND SPECIFICATION OF THE MINIMAL SUBSET OF AN OPERATING SYSTEM.

The authors are engaged in a project to produce a precise description of a design for a family of operating systems. The design decisions are being expressed by means of formal module specifications. In an attempt to write a concise specification of one of the most critical modules, a ″virtual memory mechanism″ , some previously discussed specification techniques proved to be inadequate. The specification was much too large. Through a series of improvements in both the design and in the specification techniques a much more compact description has been achieved. The design and its specification are explained.