First off the big news: I’ve found a day and time when it seems like all my committee members are available, and a room should be available as well. Right now everything seems on track for a defense on June 14, 2007.
When I wrote the last time, I said I was finally using my TeraStation for backup purposes, as intended. Then I decided to uninstall the Dropbear SSH server and install OpenSSH, and in the process I accidentally deleted a whole lot of startup scripts; the TeraStation wouldn’t boot anymore, and I couldn’t access it using telnet, SSH or the web interface. Fortunately, putting the original firmware back on it and then redoing all my changes worked. I didn’t even lose any data, it just cost me time. Maybe I should stop messing around with it now… Otherwise I need a backup for my backup unit.
I’ve played around a bit with Corky’s idea from Tuesday, i.e. allowing stronger invariants on a method in a subclass. Let’s consider the following program, first using the system I have right now, and then using the modified system that incorporates Corky’s idea:
class A {
@Invariant1
@Invariant2
public void m() { ... }
}
class B extends A {
@Invariant3
public void m() { ... }
}
public class Test {
public static void main(String[] args) {
A a = new A();
a.m();
A a2 = new B();
a2.m();
B b = new B();
b.m();
}
}
What invariants must be satisfied for each of the three calls?
In the current system, the call to a.m() must satisfy @Invariant1 and @Invariant2; the call to a2.m() must satisfy @Invariant1 and @Invariant2 because these invariants were inherited from A.m(), and additionally, @Invariant3 must be satisfied. The exact same applies to b.m(): All three invariants must be satisfied. Because the invariant was strengthened in a subclass method by adding @Invariant3, the current system emits a subtyping warning for B.m().
In the proposed new system, the call to b.m() would be allowed because the static type B is the type at which the invariant was strengthened. More precisely, it is allowed to strengthen an invariant as long as an instance of the type at which the addition occurred, or a subtype thereof, is never used as a supertype of the type at which the invariant was strengthened: Let T be the type at which the invariant was strengthened. As long as an instance of type U, U <: T, is never used as an instance of type S, T <: S, not T = S, this strengthening is acceptable.
This system seems to make sense. At first I also wondered if B.m() has to satisfy the inherited @Invariant1 and @Invariant2 at all, but I’ve realized it has to: An instance of type B, used with the static type B, could “escape” and using subsumption become an A.
The problem with this system is that it cannot provide the static guarantee that an instance of type B is never used as one of its supertypes, at least not without some kind of flow analysis that also takes into account code that is not compiled at the moment. If we wanted a static guarantee for that, so that we get the subtyping warnings in all of the cases where an instance of a subtype with strengthened invariant is used abstractly as a supertype, we would have to check that this doesn’t happen every time we compile any code, whether the code is the definition of type B itself, the code directly uses B, or the code uses something that uses B, ad infinitum.
This could be done statically, of course, but we’d have to tell the compiler or instrumentor which subtypes have strengthened invariants so it can check for violations. Maybe a data flow analysis could reveal these situations, but it would certainly be a very expensive task. If we don’t allow incremental compilation, tyhe task becomes easier, but disallowing incremental compilation runs completely counter to Java culture, and it would even rule out the use of libraries — even the Java API (rt.jar) would have to be recompiled.
Because of the loss of static information, I don’t think this should be the default system. Perhaps this system should be used dynamically and check the call sites for errors: The static analysis done by the instrumentor would emit a subtyping warning for the definition of B.m(), and then the dynamic checker would emit a warning for the call site a2.m(), but not for b.m().
This still has to ripen a little bit in my head, but I think I agree with Corky that this information should go into my thesis, even if I don’t implement it yet. These considerations are useful, I believe.
