Contracts for static methods

[BenRomberg]

The only way this seems possible while keeping the ability to refactor is with an annotation on the static method, e.g.:

public class SomeClass {
  @StaticContractReference(StaticMethodContract.class)
  public static void staticMethod() {
    // ...
  }
}

public class StaticMethodContract {
  @StaticContract
  public void contractMethod() {
    if (preCondition()) {
      assert ...;
    }
    // ...
  }
}

This would not be possible when using external contracts, where a naming-convention is the only thing I can come up with. On the other hand, static methods should be rarely used. Maybe the Annotation-hassle isn't worth the effort at all.

[marcphilipp]

I wouldn't consider this feature necessary for 4.0 (if at all).

[BenRomberg]

Well, it should be pretty easy to implement and can come in handy for legacy support. The main effort will be writing tests for almost every feature for static methods as well.

[BenRomberg]

Static methods was easy, what's missing is static initializers. Not so easy, as the compiler is initializing the synthetic field $assertionsDisabled using Class.desiredAssertionStatus in the static initializer for every class using an assert statement :-(

Will have to find out if this is compiler specific. If it's not, we can safely remove this compiler magic and also make the needed -ea VM argument obsolete.

[marcphilipp]

I would consider enabling assert without the -ea VM argument magic (which I rather dislike when it comes to programming)…

[BenRomberg]

You're right, we shouldn't change the assert mechianism as specified. Also, who knows how other compilers handle the -ea argument - maybe there's no such field that's being initialized in the static initializer.

However, we can probably assume that if we run the static initializer code in the contract class (being copied to a separate method) as the pre- and post-condition of the static initializer of the target class, that all static initializations are taking place as needed. This is because the static initializer of the target class is being run just before the target class is first being used (in a static or non-static way) and therefore the contract class can't be used earlier than that, making the pre-condition of the static initializer the earliest possible use of the contract class.

[marcphilipp]

If I remember correctly, you can have multiple static initializers in a single class. How would you write a contract for this? A separate one for each initializer or one preconfition that must hold before the first and a postcondition that must hold after the last?

[BenRomberg]

Very good point!

• Yes, you can have multiple static initializers.
• javac combines them into one static initializer at compile-time.
• I'm pretty sure that multiple static initializers aren't possible in byte-code (as they're named <clinit> and you cannot have multiple methods with the same name), but I'll double-check to be safe.

So, you'd always write pre- and post-conditions for all static initializers combined, because that's all we know when looking at the bytecode.

Another example of bytecode-differences are initializers like this:

public class DummyClass {
  {
    // this will be executed when an object of the class is instantiated
  }
}

Code in (non-static) initializers like that simply gets inserted at the beginning of every constructor (named <init>) in the bytecode. So there's no way we can write contracts for those initializer-blocks alone - they'll always have to be included with the constructor.

[BenRomberg]

We could also postpone the ability to write contracts for static initializers to post-4.0-GA. Although it could come in handy, e.g. if you have a static Map being initialized in the static initializer and you want to ensure that there are at least a certain amount of elements, or at least as many as there are elements in an enum, etc.

[marcphilipp]

My opinion is not really important, but I also think that this is not a must-have feature for 4.0.

[BenRomberg]

Btw, I double-checked: There can at most be one static initializer <clinit> in bytecode.