Add FM 2024 Tutorial tests

[Drodt]

Intended Change

Adds FM 2024 Tutorial examples as tests.

Plan

• Make remaining proofs close
• Fix method resolution bug

Type of pull request

• Other: Test addition

Ensuring quality

• I added new test case(s) for new functionality.
• I have tested the feature as follows: ...
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[Drodt]

What I had to change compared to the original tutorial:

I had to add //@ set nodeseq = \seq_empty in the constructor of LinkedList. That was missing in the original. Did we change the initialization of sequence attributes? KeY 3.0 set it to null.

[Drodt]

Also: Method resolution for Arrays.copyOf(array, array.length + 10) fails (comes up when getting a name proposal or using typeof). JavaParser says:

com.github.javaparser.resolution.MethodAmbiguityException: Ambiguous method call: cannot find a most applicable method: JavaParserMethodDeclaration{wrappedNode=public static double[] copyOf(double[] original, int newLength);, typeSolver=de.uka.ilkd.key.java.loader.JavaParserFactory$DynamicTypeSolver@787b2e03}, JavaParserMethodDeclaration{wrappedNode=public static float[] copyOf(float[] original, int newLength);, typeSolver=de.uka.ilkd.key.java.loader.JavaParserFactory$DynamicTypeSolver@787b2e03}
        at com.github.javaparser.resolution.logic.MethodResolutionLogic.findMostApplicable(MethodResolutionLogic.java:1123)
        at com.github.javaparser.resolution.logic.MethodResolutionLogic.findMostApplicable(MethodResolutionLogic.java:993)
        at com.github.javaparser.symbolsolver.javaparsermodel.contexts.JavaParserTypeDeclarationAdapter.solveMethod(JavaParserTypeDeclarationAdapter.java:319)
        at com.github.javaparser.symbolsolver.javaparsermodel.contexts.ClassOrInterfaceDeclarationContext.solveMethod(ClassOrInterfaceDeclarationContext.java:111)
        at com.github.javaparser.symbolsolver.javaparsermodel.declarations.JavaParserClassDeclaration.solveMethod(JavaParserClassDeclaration.java:339)
        at com.github.javaparser.resolution.logic.MethodResolutionLogic.solveMethodInType(MethodResolutionLogic.java:1364)
        at com.github.javaparser.resolution.logic.MethodResolutionLogic.solveMethodInType(MethodResolutionLogic.java:1352)
        at de.uka.ilkd.key.java.KeYProgModelInfo.getProgramMethod(KeYProgModelInfo.java:422)
        at de.uka.ilkd.key.java.JavaInfo.getProgramMethod(JavaInfo.java:623)
        at de.uka.ilkd.key.java.ast.reference.MethodReference.method(MethodReference.java:323)
        at de.uka.ilkd.key.java.ast.reference.MethodReference.getKeYJavaType(MethodReference.java:374)
        at de.uka.ilkd.key.java.TypeConverter.getKeYJavaType(TypeConverter.java:528)
        at de.uka.ilkd.key.rule.metaconstruct.TypeOf.transform(TypeOf.java:40)
        at de.uka.ilkd.key.java.visitor.ProgramReplaceVisitor.performActionOnProgramMetaConstruct(ProgramReplaceVisitor.java:107)

[WolframPfeifer]

What I had to change compared to the original tutorial:

I had to add //@ set nodeseq = \seq_empty in the constructor of LinkedList. That was missing in the original. Did we change the initialization of sequence attributes? KeY 3.0 set it to null.

I think that is a bug: seq is a value data type, it should not be possible to assign null to a ghost field of that type. Also, this is the whole reason for the need to specify the default value (as is currently done via /*! defaultValue(x)*/ attached to the sort declaration). I tried to rework that in #3659, see there for more details.

I think instead of null, the default value should be assigned. We should probably fix that for the 3.0 release, I will look into it.

[wadoon]

Did I catch the fix correctly? wadoon/key-javaparser@3c959a4 @unp1

[Drodt]

Did I catch the fix correctly? wadoon/key-javaparser@3c959a4 @unp1

Yes

[wadoon]

Fixed pre-version 3.28.0-K13.6-SNAPSHOT. Available at Maven Central SNAPSHOTS: https://central.sonatype.com/repository/maven-snapshots/

[wadoon]

Still failing...

[Drodt]

Proofs are fixed now.

[wadoon]

If anything is ok, I'd like to publish on key-javaparser on maven central.

[Drodt]

It all works. You may also apply the full fix in javaparser/javaparser#5066. It seems to work for variadic parameters too.

[wadoon]

Do we want to make the example accessible via ExampleChooser?

[Drodt]

Do we want to make the example accessible via ExampleChooser?

I can do that. Any opinions, @mattulbrich @WolframPfeifer?

[WolframPfeifer]

Do we want to make the example accessible via ExampleChooser?

I can do that. Any opinions, @mattulbrich @WolframPfeifer?

I would say it absolutely makes sense to make it more visible.

[WolframPfeifer]

This PR was merged into main, not into the 3.0 rc branch. Also, #3936 has main as merge target. Was/is that intentional?

[Drodt]

I can apply those commits there as well.