Parsing error in KeY Book example listing 16.2

[Robert-Brune]

Description

Parsing error in the examples of the key book (listing 16.2).
See stack trace.
Expect the following the be valid JML:

int /*@ strictly_pure @*/ max(…

Reproducible

Always.

Intermediate Solution

Change

int /*@ strictly_pure @*/ max(…

to

/*@ strictly_pure @*/ int max(…

Steps to reproduce

Load the example listing 16.2.

Additional information

ERROR WindowUserInterfaceControl - de.uka.ilkd.key.proof.init.ProofInputException: Failed to parse Java source in /var/folders/fw/w6f1wf8j12q0bhpqs9nfvcsw0000gn/T/key-examples11643747124465876277/newBook/Chapter_16/Sort:
Error occurred:
/var/folders/fw/w6f1wf8j12q0bhpqs9nfvcsw0000gn/T/key-examples11643747124465876277/newBook/Chapter_16/Sort/Sort.java:9/5: (line 9,col 5) Java syntax error: unexpected  "/*@ strictly_pure @*/" "*/", expected one of "_" "assert" "ccat" "ccatch" "enum" "exec" ...
	at de.uka.ilkd.key.proof.init.ProblemInitializer.readJava(ProblemInitializer.java:289)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:617)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:483)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:554)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:348)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:307)
	at de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:74)
	at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:124)
	at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:117)
	at java.desktop/javax.swing.SwingWorker$1.call(SwingWorker.java:305)
	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
	at java.desktop/javax.swing.SwingWorker.run(SwingWorker.java:342)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
	at java.base/java.lang.Thread.run(Thread.java:1583)
Caused by: de.uka.ilkd.key.util.parsing.BuildingExceptions: Error occurred:
/var/folders/fw/w6f1wf8j12q0bhpqs9nfvcsw0000gn/T/key-examples11643747124465876277/newBook/Chapter_16/Sort/Sort.java:9/5: (line 9,col 5) Java syntax error: unexpected  "/*@ strictly_pure @*/" "*/", expected one of "_" "assert" "ccat" "ccatch" "enum" "exec" ...
	at de.uka.ilkd.key.java.JavaService.unwrapParseResult(JavaService.java:294)
	at de.uka.ilkd.key.java.JavaService.readCompilationUnits(JavaService.java:329)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.readJava(ProblemInitializer.java:282)
	... 14 common frames omitted

---

• Commit: 359625f

[WolframPfeifer]

Thanks for testing and reporting this! It is actually a known change that comes with the changed parser. It is also mentioned in the migration guide: https://github.com/KeYProject/key/wiki/Migration-Guide:-KeY%E2%80%902.13.0-to--KeY%E2%80%903.0.0

We are aware that this requires to change some previously loadable examples, however, there are good reasons. Before, there were several places where the implementation needed to search for modifiers (e.g. pure, strictly_pure, helper, ...). Now, they are all in one place, which makes the implementation easier and more robust.

I will close as wontfix.

[WolframPfeifer]

Actually, some examples (for instance, Sort.java from KeY Book -- Chapter 16) still not loadable because the modifiers appear after the return type. Should we change these old examples, to make them loadable (even if it becomes inconsistent with the KeY book then)?

[WolframPfeifer]

I fixed this on the KeY 3.0 RC via 56541d4.