NetNews Usenet Archive 1993 #3/NN_1993_3.iso/spool/comp/lang/forth/3974

Internet Message Format | 1993-01-24 | 2.9 KB

Path: sparky!uunet!psinntp!alliant!merk!harvee.billerica.ma.us!esj
From: [e-mail] (Eric S Johansson)
Newsgroups: comp.lang.forth
Message-ID: <[e-mail]>
Organization: gators 'r us
Subject: types (forth and other)
Reply-To: [e-mail]
X-Software: HERMES GUS 1.10 Rev. Dec 23 1992
Date: Sat, 23 Jan 1993 09:32:32 -0400
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Lines: 59

there have been a series of good articles on forth, types and how
they relate.  But, as usual, it got bogged down in a debates over a
faulty implementation of a type system.  So in the spirit of throwing
a little more fuel on the fire, here are another few concepts and ideas
for folks to chew on.

"type" describes properties and some think of type as specifying
the operations one can perform on a type.  I tend to think of
operations specifying type instead of the converse, but for now, the point
is not terrible important.

pre and post conditions are associated with implementation of a type.

For an example: an integer is a type.
        x is of type integer.
        limiting x to a range of [3..8] is a postcondition of x

frequently types and postconditions are merged in the implementations
of type systems.

checking postcondition, and the related preconditions, at compile time
are more difficult than checking type but it can be done if the
compiler has knowledge of types, preconditions and postconditions for
all operations.

lets play with an example.  the definition below is of type int
yielding int.  the definition takes an int with precondition of being
in the range of 3 to 8 inclusive.  the definition yields an int with a
post condition of being in the range of 3 to 8 inclusive.

: pl1 ( int [3..8] --- int [3..8] )
    1 +
;

A type+pre/postcondition aware compiler (from now on called a tpp
compiler) would flag the above as violating the postcondition.  it could
do this only because it knows the type and properties of +.  if a
tpp compiler did not know the properties of +, it would have to insert
a runtime check to enforce the post condition.

Now, things get messy if we look at +.  it is real easy to specify
its type.  + is of type int by int yielding int.  however adding
the information needed by a tpp compiler to verify postconditions
of anything using + is a bit sticky but can be done.

I suggest that anyone interested in working with these concepts look
into formal methods in general and the work done by the Z folks
specificly.  there are some more applical areas of formal methods but the
Z stuff is more accessible and should work well in the forth domain.

overall, I think designing an extensible type system and building a
tpp compiler base on that type system would be very interesting and
*very* useful.

--- eric
--
HOME: [e-mail]  HAM  ka1eec
WORK: 617.630.4687 (w)   [e-mail]
source of the public's fear of the unknown since 1956