[Prev][Next][Index][Thread]
Component Pascal type system is unsound
-
To: Types List <types@cis.upenn.edu>
-
Subject: Component Pascal type system is unsound
-
From: Fergus Henderson <fjh@cs.mu.oz.au>
-
Date: Fri, 28 Dec 2001 02:49:13 +1100
-
In-Reply-To: <200112171946.fBHJk4C03239@saul.cis.upenn.edu>; from ajeffrey@cs.depaul.edu on Mon, Dec 17, 2001 at 01:18:22PM -0600
-
References: <200112171946.fBHJk4C03239@saul.cis.upenn.edu>
-
User-Agent: Mutt/1.2.5i
While we're on the topic of languages with unsound type
systems, let me mention another one: Component Pascal.
<http://www.oberon.ch/docu/language_report.html>.
According to www.oberon.ch, Component Pascal is a refined version of
Pascal, Modula-2, and Oberon, and moreover it is advertised as being
"type-safe".
However, in July this year, in response to some mail from John Gough,
I constructed an example which demonstrates a hole in Component Pascal's
type checking.
The basic problem arises due to the parameter compatibility rules for
"OUT"-mode parameters (which use pass-by-reference) and "extended types"
(Component Pascal's name for derived classes).
These rules allow, for instance, "OUT"-mode parameters whose type is
a pointer to an extended type to be bound to variables whose type is
a pointer to the base type. This can lead to problems when such
parameters are aliased.
Here's an example which shows the problem.
MODULE Foo;
TYPE
base = RECORD
x : INTEGER;
END;
derived1 = RECORD(base)
y : INTEGER;
END;
derived2 = RECORD(base)
z : INTEGER;
END;
VAR
b : POINTER to base;
PROCEDURE bar(OUT a1 : POINTER TO derived1;
OUT a2 : POINTER TO derived2);
BEGIN
NEW(a2);
NEW(a1);
a2^.z := 42;
END bar;
BEGIN
bar(b, b);
END Foo.
Component Pascal allows this sort of code, but this program ends up
assigning to the `z' member of an object of type `derived1', which
does not have any `z' member.
(I probably have some of the details of this program wrong, since I don't
have a Component Pascal implementation around to check it. But John Gough
has verified that the problem I describe did occur for his Component
Pascal implementation, and last I heard the authors of the Component
Pascal told him that they are planning to revise the language to correct
this type loophole... in particular removing OUT parameter variance.)
--
Fergus Henderson <fjh@cs.mu.oz.au> | "I have always known that the pursuit
The University of Melbourne | of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.