New annotation to give an externally-visible name to a generated Dafny class

[lukemaurer]

Currently, an {:extern} declaration on a class has two effects: Allowing that class to have {:extern} methods and giving that class a predictable name that external code, written in the target language, can refer to. When generating a library, it makes sense to give an {:extern} declaration even when there are no extern methods, just to give the generated class the right name.

Unfortunately, this usage has surprising consequences in the Java and JavaScript backends. A class can have both Dafny methods and extern methods, so somehow the backend has to combine user code and generated code in the same class. The C# backend uses partial classes to do this, whereas Java and JavaScript use inheritance. If there happen to be no methods for the user to implement, the C# backend doesn't need the user to supply any code at all, since C# allows a class to be declared partial even if it's complete. Thus someone can just add {:extern} to a Dafny class and not have to write any C# code. But the Java and JavaScript backends will fail without a user-supplied class because they generate code that expects both a base class and an derived class. This means that the user must always supply a class, even if it's a silly stub class that does nothing but extend (in the Java case) or be extended by (JavaScript) the generated class. See Test/comp/Extern3.js (the AllDafny class) and Test/comp/AllDafny.java. (The Go backend would probably have the same problem, but it currently doesn't support mixing Dafny methods and extern methods at all.)

Rather than add special logic for extern classes without extern methods, it would make more sense to separate the two effects of the {:extern} declaration by adding an annotation that just means “give this class the following name, visible to external code.” @robin-aws suggests that this should actually be what {:extern} means, and that {:native} should be the annotation on a method whose implementation is in native code.

[samuelgruetter]

I also think it would be helpful to have two distinct annotations:

• one to say "don't compile this because it already exists in the target language, where it has the following name",
• one to say "do compile this to the target language, but give it the following name there"

Specifying a name would be optional in the first one (and default to the Dafny name), but mandatory in the second one.

And if these annotations are redesigned, we should keep in mind that we might need to provide different extern names for different target languages. When I was working on Dafny code which is compiled both to Java and C# last summer, we used a quick and dirty sed script to achieve this, but it would be much better to have actual support for this in Dafny.

[robin-aws]

The more I work on a potential solution to #461 and #463, the more I think that it makes more sense to keep the meaning of {:extern} as is, but with more restrictions on Dafny features that can't be directly compiled, and to introduce a new annotation as you suggest (or new declaration mechanism entirely) to "import" existing external names.

[cpitclaudel]

The situation is a bit worse than this: the meaning for extern is not the same for traits and classes, at least in C#: for classes an extern method is omitted, but for traits extern only serves to rename methods, and an interface generated unles :compile false is set.