Proposal: Name resolution via companion namespace

[wadoon]

From the last Chapter 4 draft in #6. We have an open discussion point around the name conflicts.
I re-post here my proposal for the \spec namespace.

There is a situation that is unavoidable. A Java class Parent may contain a declaration of a JML name n that is appropriately distinct from any potentially conflicting name in Parent . However, unknown to the specifier of Parent , a class Child can later be derived from Parent and the (Java) author of Child , not knowing about the JML specifications of Parent , may declare a name n in Child . In such a case. with a local Java entity and an inherited JML entity having the same name, what does the name refer to? In Java code, the name refers of course to the (one) Java declaration. In JML code the ambiguity is resolved in favor of the Java name. In this case the JML entity could be referred to in JML code within Child as super.n .

Need a more general solution to the name resolution problem of the last bullet above. Do we need a pseudo operator something like \jml(n) to force resolution as a JML name? Or do we need a syntax to write JML identifiers that cannot be Java identi- fiers, such as ‘n or a convention to write JML identifiers that are unlikely to be Java identifiers, such as $$n ? Or perhaps syntax like super.Parent.n to limit the name resolution to the Parent class, where it will find the one JML declaration of n ? The last is perhaps the most future-proof and Java-like.

For the ambiguity problem, the \jml(n) would not my favorite. This is very untypical for Java. super.Parent.n is also strange as Java defines Parent.super.n (in alignment to OuterClass.this.n).

My suggestion would be to have a concept like an companion object (similar to Kotlin). Every instance has a companion instance, a field of a generated inner class called \spec, which holds all JML member definitions.

If we write abc inside a JML construct, first, we lookup with the Java name resolution, if not found we lookup in the \spec namespace. It also can be fully-qualified address by using super.\spec.n, or this.\spec.n. It is also usable for static specification: java.lang.Object.\spec.method(). Additionally, it makes easy to explain spec_public & Co. These defines the visibility of the elements in \spec.

The construct would looks similar on an idealized view:

class A {
     public class \spec {
        // JML member declaration of A
     }
     public final /*@ model*/ \spec \spec = new \spec();
}

[leavens]

I can see some merit in the idea of a companion object named \spec, although I don't particularly like having to use a name like \spec in an otherwise Java-like name. Would it be sensible to have the name "spec" used for this in JML with the provision that \spec could also be used as an alias, in case the Java code uses "spec"?

[davidcok]

I summarize this proposal as the following

• java and Jml names are in the same namespace. That is, within the same class, JML cannot declare names that duplicate Java names (that is the declaration would be disallowed were it a Java declaration).
• within specification expressions, one resolves names using Java rules, except that specification declarations are also considered.
• The new point: where a java declaration hides a specification declaration (in the Java sense), the hiding name is used, as expected; the prefix \spec. can be used to designate that only specification names should be considered.
• spec is a synonym for \spec, in scopes where spec is not already declared as a Java or JML name.

However, in retrospect I don't think a solution is needed here at all. Casting works just fine. The following pure Java example would work for JML as well.

class Parent {
  int n = 10;
}

class Parent2 extends Parent {
  int n = 20;
}

public class Names extends Parent2 {
  int n = 30;

  public static void main(String ... args) {
    Names x = new Names();
    System.out.println(x.n + " " + ((Parent2)x).n + " " + ((Parent)x).n);  // yields 30 20 10
  }

}

[davidcok]

So I propose adding no new features to JML to refer to hidden names.

[leavens]

Yes, if we can just use casting, then we could just explain that in the reference manual and not add new features to JML. Good idea @davidcok!

[leavens]

To be clear, I'm okay with the proposal as in @davidcok's last long message, without any new JML features.

[mattulbrich]

I am happy if we can get away without a new construct.