Issue Importing .proof Files in KeY: "Could Not Resolve BigInteger.ONE"

[JDavidCE2022]

Hello. I am trying to import .proof files from Peter H. Schmitt's Ordinal Numbers implementation in KeY. However, every time I load a proof file, I get the following error:

Could not resolve UncollatedReferenceQualifier "BigInteger.ONE" @8/24 in "FILE:C:\Users\jes\Downloads\.\GoodsteinBig.java" (11) Consider using a classpath in your input file if this is a classtype that cannot be resolved (see https://keyproject.github.io/key-docs/user/Classpath for more details). Caused by: recoder.service.UnresolvedReferenceException: Could not resolve UncollatedReferenceQualifier "BigInteger.ONE" @8/24 in "FILE:C:\Users\jes\Downloads\.\GoodsteinBig.java" (11)

This issue occurs regardless of the Java version or KeY version I use.

Setup and Attempts

KeY Versions Tried:

• KeY-2.12.3 (2024-09-08)
• KeY-2.8.0 (2020-12-01)
• KeY-2.6.3 (2017-10-11)
• KeY-2.6.2 (2017-04-13)

Java Versions Tried:

• JDK 21 (KeY-2.12.3, KeY-2.8.0)
• JDK 17 (KeY-2.12.3, KeY-2.8.0)
• JDK 11 (KeY-2.8.0)

Results: In all cases, the error remains the same (BigInteger.ONE cannot be resolved).

Context
The files I am using come from the Ordinal Numbers project by Peter H. Schmitt, which includes:

• GoodsteinBig.java (which computes Goodstein sequences using BigInteger)
• Goodstein.java (which is analyzed in the paper)
• .proof and key files for correctness proofs

According to the project documentation, the .proof files should be loadable into KeY via File → Load Proof. However, KeY fails to resolve BigInteger.ONE.

Steps I Have Taken to Fix the Issue

• Set the classpath manually in a .key file, adding:
  \bootclasspath "C:\Program Files\Eclipse Adoptium\jdk-17.0.14+7\lib"; \classpath "C:\Program Files\Eclipse Adoptium\jdk-17.0.14+7\modules\java.base"; \javaSource "GoodsteinBig.java";
  No effect; the error persists.

• Ran KeY with a custom classpath using commands like:
  java -classpath "C:\Program Files\Eclipse Adoptium\jdk-17.0.14+7\modules\java.base" -jar key-2.12.3-exe.jar
  Still fails to resolve BigInteger.ONE.

• Used fully qualified names (e.g., java.math.BigInteger.ONE) in GoodsteinBig.java. No effect.

• Tested different JDK versions. The error remains in every case.

Request for Help

I suspect this might be an issue with:

• How KeY resolves classpath dependencies for BigInteger
• The .proof file structure in this particular project

Could anyone familiar with KeY’s classpath system or proof imports suggest what might be going wrong?
Is there a specific way to ensure Java standard libraries are properly recognized in KeY?

Thanks in advance for any help!

[wadoon]

For me, it seems that ordinal numbers require a special version of KeY linked on the web page, based on KeY 2.4, but it seems you use the current release version of KeY (i.e. 2.12.3).

Your error corresponds to the fact that our BigInteger class class misses the ONE constant on branch main. But adding it might results into the next error b/c some definitions are missing.

@mattulbrich In the old KeY repo, there is the branch pschmittOrd, which seems to correspond to the special KeY version.

[JDavidCE2022]

Ok, thank you very much. Is there a precompiled version of the pschmittOrd KeY branch available for download?

[wadoon]

The first link of my answer is the link to the pre-compiled version. Back then it was not a fat jar.

For me, it seems that ordinal numbers require a special version of KeY linked on the web page, based on KeY 2.4, but it seems you use the current release version of KeY (i.e. 2.12.3).