University of Paisley, High Street,

Paisley, Scotland. PA1 2BE

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:

- Develop a formal model of a simple embedded micro-controller.
- Develop a model for a simple ANSI Standard Forth IDE. This environment should be formally specified and proven to be complete, consistent and compliant with the ANSI Standard.
- The Forth IDE should be implemented, and proven to meet with its specification.

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.

- [Bow87]
- Bowen, Jonathan P.:
*The Formal Specification of a Microprocessor Instruction Set*, Technical Monograph PRG-60, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, January 1987. - [Kem88a]
- Kemp, D. H.:
*Specification of Viper1 in Z*, RSRE Memorandum no. 4195, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, October 1988. - [Kem88b]
- Kemp, D. H.:
*Specification of Viper2 in Z*, RSRE Memorandum no. 4217, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, October 1988. - [KnS91a]
- Knaggs, Peter J., and W. J. Stoddart: Formal Forth, in
*Proc. Rochester Forth Conf. on Automated Instruments*, pages 50-55, June 1991. - [KnS91b]
- Knaggs, Peter J. and W. J. Stoddart: The Cell Type, in
*Proc. Rochester Forth Conf. on Automated Instruments*, pages 55-57, June 1991. - [Mac93]
- MacKenzie, Donald: Burden of proof goes to trial, in
*The Time Higher Education Supplement*, March 5, 1993. - [Poi90]
- Pöial, Jannus: The Algebraic Specification of Stack Effects for Forth Programs,
in
*Proc. EuroFORML Conf.*, October 1990. - [Poi91]
- Pöial, Jannus: Multiple Stack Effects of Forth Programs, in
*Proc. EuroFORML Conf.*, October 1991. - [Spi90]
- Spivey, J. Michael: Specifying A Real-Time Kernel, in
*IEEE Software*, pages 21-28, September 1990. - [StK91]
- Stoddart, W. J. and Peter J. Knaggs: Type inference in stack based languages, in
*Proc. EuroFORML Conf.*, October 1991. - [StK92]
- Stoddart, W. J. and Peter J. Knaggs: The (almost) Complete Theory of Forth Type Inference,
in
*Proc. EuroFORML Conf.*, September 1992. - [StK93]
- Stoddart, W. J. and Peter J. Knaggs: A type signature algebra for stack based machines,
in
*Formal Aspects of Computing*, 5(4):289-98, August 1993. - [Sto88]
- Stoddart, W. J.: Specification & Optimisation, in
*Proc. EuroFORML Conf.*, September 1988. - [Sto92]
- Stoddart, W. J.: Implementation of the Forth Type checker, in
*Proc. EuroFORML Conf.*, September 1992. - [Tho91]
- Thompson, Brain L.:
*Hardware Compilation as an Alternative Computation Architecture*, M.Sc. Thesis, School of Computing and Mathematics, University of Teesside, Borough Road, Middlesbrough, Cleveland, TS1 3BA, UK, August 1991.

- It should be noted that a simple abstract model similar to the one presented
in [Spi90] could provide a means of
standardising the multi-tasking aspect of Forth. This topic was not covered
by the ANSI Standard due to its complexity. However, a simple abstract model
that does not place any restrictions on the scheduling algorithm, yet provides
for the majority of algorithms should be acceptable.
- In would be possible, however the specification would have to be at such a
low level of abstraction that it would be too time consuming for sufficiently
little result.
- York Software Engineering is an offshoot of the University of York. The
Defence Research Agency was previously known as the Royal Signals and Radar
Establishment (RSRE) at Malvern.