VerCors does not find global declarations if given multiple files

[ArmborstL]

If global declarations are defined in one file and used in another, VerCors does not make the connection. I have file A.java

/*@ resource p(A a) = true; @*/
class A {
} 

and file B.java

class B {
    /*@ requires p(a); @*/
    void m(A a) { }
}

Invoking VerCors on both files together results in "Could not find method named p" for the usage in B. It should be able to match the declaration in A.java to the usage in B. Pieter commented that currently "within a Java file, the resolution works normally; cross-file you can not see the global declarations in other JavaNamespaces".

[ArmborstL]

Result of discussion today:

• ghost fields are part of the class, and thus not an issue
• so the question is mostly how to handle top-level specifications like in the example above.

In principle, there are two approaches to importing such specifications:

• use the target language namespacing, e.g. embed specifications in Java packages. This would then mean that it depends on the target language how importing works.
• have a dedicated specification namespace and importing mechanism. This would be more consistent across target languages.

To an end user, the first one would probably feel more natural, so this should be the default way.

However, for libraries (e.g. providing graph functionalities) we might want to have a single implementation that can be used in specifications of all target languages. Thus, here a dedicated namespace is needed. It is already possible to include PVL files into non-PVL projects, which would be the way for the libraries. But it was agreed that this should be used only for specification purposes, not e.g. mix implementations with parallel blocks into non-PVL projects.

[pieter-bos]

Rough proposal:

//@ spec_import Graph.stuff;

package a;
import a.b.C;
import d.e.F;
//@ ghost import g.h.globalPredicate;

class Test {
  /*
  Here we can use:
  - globalPredicate
  - g.h.globalPredicate
  - (implicitly) any stuff in a.*
  - stuff (from Graph.stuff)
  */
}

//@ spec_import Graph.stuff;
#include <interface.h>
//@ ghost include <predicates.h>