Over the last couple of years several papers have been presented attempting to bring formal methods to Forth, or applying formal methods to Forth. This paper brings together many of these ideas and suggests a method by which they could be integrated into a single formally specified and implemented Forth programming environment.
Much of the theoretical work described in this paper exists in some form. However, the proposed integration of these theoretical ideas has not been investigated any further than this paper.
Several papers have appeared in the formal methods world that relate to Forth, although the authors may not consider this so. For example, Spivey [Spi90] describes a simple real-time kernel with a co-operative round-robin scheduler. He goes on to describe the simple prioritised interrupt system provided by the kernel [1]. Indeed this is a good description of Forth's Co-operating multi-tasking system. The scheduler is described in sufficiently abstract terms that most, if not all, current Forth schedulers would meet it requirements.
Bowen [Bow87] provides a formal description of the Motorola M6800 microprocessor. The intention was to provide a basis for formal proof of software developed for this processor. Bowen says "more complicated and modern microprocessors such as the 68000 family could be specified in a similar manner. However such processors would require a larger document and more work in order to cover them fully." The Forth based processors (such as the F-RISC or Dolphin processors) would make a particularly good processor for such a specification, as it implements the Forth abstract machine directly in silicon.
Jannus Pöial's paper [Poi90] was the first to show a formal typing system for Forth. Although the work was still incomplete it sparked off an interest at Teesside leading to our paper [StK91]. After continued work by both teams we have developed two very different typing algebras. The most recent description of which can be found in [StK93].
At Teesside we have implemented a version of the type algebra in SML [Sto92], and are working on extending Mitch Bradley's SunForth to include type checking, without detracting from the Forth's flexibility. Using type checking we are able to identify programming errors at compile time, rather than having to track down spurious run time errors.
The ANSI Standard's concentration on portability has introduced many new data types (and pointers). This matches well with the idea of checking for the abuse of such types.
Even with this formal basis it was not possible to conduct proofs due to the lake of stack typing [2]. It was at this point our investigations were suspended. When Pöial published his work on a type theory suitable for stack based languages [Poi90] he presented us with a method for overcoming the this problem.
Although we have since concentrated our efforts into developing our own type algebra, we now feel that it should be possible to generate a formal basis for Forth. The idea being that one would take a specification, and refine it into a Forth implementation. Using the formal base it should be possible to prove that the implementation has the same properties as the original specification, and is therefore a true implementation of that specification.
The Open Systems Federation (OSF) and the DRA are currently attempting to develop an ADA `producer' for their ANDF intermediate language technology. This compiler is being specified using the RSL formal notation. The idea being that one could use the RAISE method to derive an ADA implementation of a formal specification and prove that it holds the same properties as the original specification.
This would start with a formal specification of a stack processor, probably an existing one, or better yet one still in the design stage. Having developed this specification, it should be possible to develop a full ANSI standard Forth system for it, complete with a formal programming model.
The idea is to provide the formal support for embedded applications. One could develop a formal specification of an application. This specification could then be refined, using the formal model, into a Forth program. As the Forth system is formally defined we can prove that the resultant program is a true implementation of the original specification.
This project could be achieved in the following way:
The flexibility of Forth makes a formal model slightly more difficult than for other languages, however, the underlying abstract machine is particularly well suited for formal specification. With the addition of the type algebra we feel that this is now possible. Such a formal IDE underpinned by a specified micro-controller would make it possible to prove that the full system is a true implementation of the original specification.
This is about as far as we can go before having to specify and prove hardware! The failure of the Viper project [Kem88a, Kem88b] shows this to be a difficult, if not impossible, task. However given some of the new hardware compilation techniques being developed by the Programming Research Group at the University of Oxford this may become easier in the future [Tho91].
We looked briefly at Spivey's description of a simple Forth-like real-time kernel complete with a co-operative round-robin scheduler, and at Bowen's specification of the Motorola 6800. This proves that not only is the Forth abstract machine well suited for formal specification, but it would be of interest to Formal methods/Safety critical practitioners. As there are Forth engines that implement the abstract machine directly in silicon we could take such a specification all the way down to the processor's instruction set (and possible even further).
We went on to present a project that would bring the different ideas together. The project is outlined by means of a proposal that we (the Forth community) develop a formal Forth IDE such that one can use a formal model to derive a Forth implementation of a specification. It should be possible (using the formal model) to prove that the Forth implementation holds the same attributes as the original application's specification, and is therefore a true implementation of that specification.
Providing a complete embedded programming environment would make Forth a more attractive target language. As the IDE has been developed to a standard and has been proven, one need only concentrate on the problem at hand and not on the underlying environment as is currently the case.