At 10:59 PM 10/26/99 , Ka-Ping Yee wrote:
> define square(x : int) : int
>
> define point {
> to getX : int
> to getY : int
> }
[+] Very cool!
>... parse these kinds of specifications (the
>grammar would be pretty easy, right?). Then one could take a
>parse tree for an interface spec and present a parse tree for an
>object to be mechanically verified as a rudimentary sanity check.
If we make this sanity check into an auditor, then
typedef SquareType (x : int) : int
typedef PointType {
to getX : int
to getY : int
}
allows
define square :: SquareType (x : int) : int { x * x }
define point :: PointType {
to getX : int { x }
to getY : int { y }
}
because they pass the sanity check, and
define pt : PointType := PointMaker new(3, 5)
because the initial value is verified as being an instance of code that passed this sanity check.
Cheers,
--MarkM