Towards Formal Forth

Peter J. Knaggs

Department of Computing and Information Systems,
University of Paisley, High Street,
Paisley, Scotland. PA1 2BE

pjk@paisley.ac.uk


Abstract

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.


1. Introduction

Over the last three years or so we have seen several papers attempting to bring the worlds of formal methods and Forth together. Papers have appeared on the initial investigation into the specification of the Forth Integrated Development Environment (IDE) [Sto88, KnS91a]; to a stack based type theory (suitable for Forth) [Poi90, Poi91, KnS91b, StK91, StK92, Sto92, StK93].

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.

1.1. Type Checking

There are currently two teams developing formal type checking systems for Forth, one at the University of Tartu and the other at the University of Teesside. Although these teams are working in the same area, and communicate with each other, they are approaching the problem in two very different ways.

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.

1.2. Formal Basis

At Teesside, we investigated the idea of providing a formal basis for the specification of the Forth IDE. Our initial thoughts where presented in [Sto88] and later in a more complete form in [KnS91a].

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.

1.3. Formal Methods

The Formal Methods world has been looking for a way to develop embedded software that can be proven to work. York Software Engineering and the Defence Research Agency (DRA) [3] have recently released a system known as SPARK, a method for deriving correct ADA programs from Z specifications.

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.

2. Proposal

In this section we present a project in which the whole Forth community could take a part. This is a large project and could take a long time to come to fruition. There may be several research projects in the idea presented here.

2.1. Outline

The project is to develop a formal Forth IDE similar to the OSF/DRA ADA system. This would allow one to specify a problem. And using a known method (such as RAISE) derive a Forth program that can be proven to be a correct implementation of that 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:

  1. Develop a formal model of a simple embedded micro-controller.
  2. 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.
  3. The Forth IDE should be implemented, and proven to meet with its specification.

2.2. Argument

Although attempts have been made at specifying hardware before (re Viper), in this project we propose using an existing (or forthcoming) embedded micro-controller. The reasoning behind this, is that the technology already exists, and we are interested in how to best use this technology.

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].

3. Summary

Over the last couple of years papers have appeared on specification of the Forth IDE; to stack based type-theories. We have looked at some of this work, and some of the work coming from the Formal methods/Safety critical systems people. This was found to be not only applicable to Forth, but to have a similar intent.

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.

4. References

[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.

End Notes:

  1. 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.

  2. 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.

  3. 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.