Stack effect calculus with typed wildcards, polymorphism and inheritance

Abstract

Jaanus Pöial

University of Tartu, Estonia


In early 1990s author introduced a formal stack effect calculus for
verification of compilers that translated high level languages (Fortran,
Modula) into Forth, see [PST90],[P90a],[P90h]. The calculus was partially
applicable to static type checking of Forth programs, but this was not
the primary goal these days. Stack effects (formal specifications of input
and output parameters for stack operations) were defined using flat type
space where different types were considered incompatible and no subtyping
or inheritance was allowed. The so called wildcard types were introduced by
sets of stack effects, see [P91]. This framework does not suite well with
abstract stack machines that use principles of object orientation (see, for
example, [AG98] about type checking in Java Virtual Machine). Peter Knaggs
and Bill Stoddart improved the type signature algebra and introduced a lot
of useful things (type variables, subtyping, reference types, wildcards,
etc.), see [SK93], [K93].

In this presentation a modified framework for type checking is proposed
to support typed wildcards and inheritance. Now it is possible to perform
little more exact type calculations and express polymorphic operations.
Every type symbol has its place in the type hierarchy and, at the same time,
it may be treated as a wildcard symbol. Earlier approaches matched wildcards
to concrete symbols (resulting in this concrete symbol) or to other wildcards
(resulting in a new wildcard); this approach is more general allowing
stepwise refinement of types. Not only the type checking is target here, but
also the (static) choice of  the right version for polymorphic operations
(known as method overloading in object oriented languages). Given a type
hierarchy, formal specifications for operations and a program we can refine
the type signatures in the program  according to the context where an
operation appears. Experimental implementation of this framework is in
progress.


References

[PST90] Tombak M., Soo V., Pöial J. A Forth-Oriented Compiler Compiler
and its Applications. FORTH Dimensions (ISSN 0884-0822), Vol XVI No 5,
Jan-Feb 1995, Forth Interest Group, Oakland, USA, 21-22.

[P90a] Pöial J. Algebraic Specification of Stack Effects. FORTH Dimensions
(ISSN 0884-0822), Vol XVI No 4, Nov-Dec 1994, Forth Interest Group, Oakland,
USA, 18-20.

[P90h] Pöial J. A Bit of History. FORTH Dimensions (ISSN 0884-0822), Vol XVI
No 4, Nov-Dec 1994, Forth Interest Group, Oakland, USA, p. 17, 20.

[P91] Pöial J. Multiple Stack-effects of Forth Programs. 1991 FORML Conf.
Proceedings, euroFORML'91 Conference, Oct 11 - 13, 1991, Marianske Lazne,
Czechoslovakia, Forth Interest Group, Oakland, USA, 1992, 400-406.

[SK93] Bill Stoddart, Peter J. Knaggs: Type Interference in Stack Based
Languages. Formal Aspects of Computing 5(4): 289-298 (1993).

[K93] Peter J. Knaggs. Practical and Theoretical Aspects of Forth Software
Development. PhD thesis, School of Computing and Mathematics, University
of Teesside, Middlesbrough, Cleveland, UK, March 1993.

[AG98] Allen Goldberg. A Specification of Java Loading and Bytecode
Verification. In Proc. 5th ACM Conference on Computer and Communications
Security (CCS'98), pages 49-58, October 1998.

This work was supported by Estonian Science Foundation grant No. 5279