[PRL] the "success" of types

[William D Clinger]

Felix wrote:
> I'm sorry, what was this point of this example?

That one can indeed "write an invariant that states:  Right now,
x and y are both lists of some type T (though at other times
they might not be of the same type)" in Java.

> John said that you can't write down certain time dependent invariants  
> of practical interest.

He was wrong.

> I inferred that he wanted this invariant to  
> be automatically checked (statically, I assume, though some may be  
> happy with a dynamic check, as long as it happens at a sensible  
> place).

You are probably right about what John wanted and should have
said, but what John actually claimed is that he "can't write"
an invariant...".  In my very first post of this thread, I wrote:

    First of all, checking of invariants is not at all the same thing
    as thinking about them or writing them down.

I seized upon John's false claim as an opportunity to make this
point yet again.

> My hypothesis is that the error will be signaled at  
> the invocation of the .intValue() method (but I have not checked this  
> hypothesis; its just based on my knowledge of type-erasure).  So if  
> this is true, then we would find that stating John's invariant didn't  
> actually buy us anything; it wasn't checked at the point of the cast  
> expression, so what was the point writing that invariant down?

The point of writing down an invariant that isn't checked at
compile time, and is checked but poorly even at run time, is
approximately the same as the point of writing down a purpose
statement that isn't checked at compile time, and is checked
but poorly even at run time.

> So, again, my question: why was this a counterexample to John's claim  
> that you can't express what he wants in Java?

Because the counterexample shows you can use the syntax of Java
to write down the invariant John claimed you couldn't write in
Java.

Will