Building issues

[CopperEagle]

Hey there @wadoon

Thanks for the repository. For my project, I need to translate jml to java code (into assertions). Unfortunately there is no documentation. I wanted to ask you

1. How do I build this into a jar usable from Java?

2. How can I use your jml2java module from Java?

I tried

# gradle init
gradle build

but I end up getting a few-byte jar file both with and without init. Also, the Github action build keeps failing too so that's not helping either.

Any help is appreciated

[wadoon]

You can use the regular Gradle targets, e.g., gradle classes, testClasses, or assemble to compile the class files, and also the test classes, or to finally build all artifacts. I also fixed some compiler errors.

The functionalities are rather in an unfinished state. For example you mentioned jml2java module: Some expressions are supported, but support for complicated constructs (especially, \old) is absent.

Currently, we are migrating JJBMC from openjml to jmlparser, which also implements a jml2java conversion feature, but designed for bounded model checker (e.g., use of nondet. variables).

/cc @JonasKlamroth

[CopperEagle]

Dear @wadoon and @JonasKlamroth

Regarding invariants I have a question. I was suprised to find out that the official JML reference by David R. Cok, Gary T. Leavens, and Mattias Ulbrich does not specify what the visibility modifiers mean, e.g. //@ private invariant head == 0. How does the JML community typically interpret this?

Am I right to guess that it modifies for which methods the invariant applies, as follows:

• public invariant: Only for public methods
• protected invariant: Only public and protected ones
• package invariant (no modifier): Only package and public ones
• private invariant: Any method

Is this right? Or is it typically interpreted more restrictive?
Once again, thank you very much for your assistance.

Kind regards

[wadoon]

The modifier interpretation is only for visibility reasons.

The reason is that an invariant can express facts on private, protected or internal variables (or methods), that might not be visible to the caller/user of a method/class.

Therefore, like in Java, using private fields in public invariants is a bad choice.

Now it depends on your reasoning and the scope of your invariant utilization. Hence, how do you use the invariants in your tooling?

In general, all invariants need to hold on method calls. But with an external checker, you might only use public invariants, as the access is limited to those members.

KeY completely ignores all visibility modifiers.

If you want to disable the class invariants on a method, the method must have the helper modifier (at least in KeY). Invariants of object parameters (e.g., foo(o)) are not assumed automatically in KeY.

[CopperEagle]

Dear @wadoon

Thank you for your response! In the tool I write, the invariants have access to all fields and are only for a specific class. It is then used to test this class. So there is no passing of specifications up or down the class hierarchy.

I was assuming that there is some mechanism in JML invariants itself to steer where they apply. Private methods typically are private because they violate some invariant and thus should not be used from the outside. However, the approach using the helper modifier is indeed more finegrained and makes more sense.

Also, I wanted to ask whether you could recommend some real projects/classes that use JML (so I can test my tool on them). The only industrial example I know so far that uses JML is the encryption-sdk by AWS. Could you point out some other datastructure implementations or projects that make use of JML?

Thank you very much for your answer!

[wadoon]

I have gathered most of the case studies in the KeY organization:

https://github.com/keyproject/

There are:

• https://github.com/KeYProject/ips4o-verify
  New very fast sorting algorithm. TACAS'24

• https://github.com/KeYProject/VerifyingIdentityHashMap
  java.util.IdentityHashMap -- Best paper, iFM'22

• https://github.com/KeYProject/BitSet-KeY-Artifact
  java.util.BitSet, FACS'23

• https://github.com/KeYProject/rbtree-verification
  Red-Black Trees

• https://github.com/KeYProject/DualPivotQuickSort
  Dual Pivot Quicksort: One of the standard sorting algorithms in Java. VSTTE'17?

• https://github.com/KeYProject/TimSort
  TimSort -- also a JDK default sorting algorithm. CAV'15. Bug found.

• https://github.com/KeYProject/verifythis-ltc-2020
  Simplified Version of the Hagrid key-server

[CopperEagle]

@wadoon Oh, I did not yet know KeY had some examples on their Github. Thank you so much for your support! It helped a lot!