True) polymorphism in SPARK2000

The SPARK programming language and associated tools are specifically intended for the implementation of high integrity systems. SPARK2000 is an extension to the SPARK95 language to support object-oriented programming. This paper presents how polymorphism can take place in SPARK2000 through restrictions on the use of access types. Those restrictions ensure that neither aliasing nor definition of recursive types can occur in SPARK2000. Due to the last restriction, the storage requirement of any program can be statically determined.