weigl/jmlparser

key.core/build.gradle

@@ -21,10 +21,10 @@ dependencies {
 
     api project(':key.util')
 
-    def JP_VERSION = "3.28.0-K13.5"
-    api "org.key-project.proofjava:javaparser-core:$JP_VERSION"
-    api "org.key-project.proofjava:javaparser-core-serialization:$JP_VERSION"
-    api "org.key-project.proofjava:javaparser-symbol-solver-core:$JP_VERSION"
+    def JP_VERSION = "3.28.0-J8.0-K13.5-SNAPSHOT"
+    api "io.github.jmltoolkit:jmlparser-core:$JP_VERSION"
+    api "io.github.jmltoolkit:jmlparser-core-serialization:$JP_VERSION"
+    api "io.github.jmltoolkit:jmlparser-symbol-solver-core:$JP_VERSION"
 
     testImplementation("com.google.truth:truth:1.4.4")
     testImplementation(project(":key.core"))

key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java

@@ -421,7 +421,9 @@ public ClassOrInterfaceType getType(String... names) {
             return null;
         }
         final SymbolReference<ResolvedMethodDeclaration> method = MethodResolutionLogic
-                .solveMethodInType(rct, name, jpSignature, contextTypeDeclaration.get());
+                .solveMethodInType(rct, name, jpSignature
+                //TODO super important        , contextTypeDeclaration.get()
+                );
         return method.getDeclaration()
                 .map(d -> (IProgramMethod) Objects
                         .requireNonNull(mapping.resolvedDeclarationToKeY(d)))
@@ -688,26 +690,24 @@ private ImmutableList<KeYJavaType> recFindImplementations(
         return result;
     }
 
-
-    // TODO(weigl): Implemented by @Drodt, no idea if it's correct
     private boolean declaresApplicableMethods(ResolvedTypeDeclaration rt, String name,
             List<ResolvedType> signature, ResolvedReferenceTypeDeclaration context) {
         if (rt instanceof MethodResolutionCapability mrc) {
-            var method = mrc.solveMethod(name, signature, false, context);
+            var method = mrc.solveMethod(name, signature, false
+                    //TODO super important: , context
+                    );
             return method.isSolved();
         }
         return false;
     }
 
-    // TODO(weigl): Implemented by @Drodt, no idea if it's correct
     private boolean isDeclaringInterface(
             ResolvedTypeDeclaration ct, String name,
             List<ResolvedType> signature) {
         Debug.assertTrue(ct.isInterface());
         var id = ct.asInterface();
         var set = id.getDeclaredMethods();
         for (var m : set) {
-            // TODO: check if m is visible for ct
             if (name.equals(m.getName())
                     && isCompatibleSignature(signature, m.formalParameterTypes()))
                 return true;

key.core/src/main/java/de/uka/ilkd/key/java/ast/ProgramElement.java

@@ -4,8 +4,8 @@
 package de.uka.ilkd.key.java.ast;
 
 
+import com.github.javaparser.ast.jml.clauses.JmlContract;
 import de.uka.ilkd.key.rule.MatchConditions;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
@@ -26,12 +26,6 @@ public interface ProgramElement extends SourceElement, ModelElement {
      */
     Comment[] getComments();
 
-    ///
-    default ImmutableList<TextualJMLConstruct> getAttachedJml() {
-        return ImmutableSLList.nil();
-    }
-
-
     /**
      * matches the source "text" (@link SourceData#getSource()) against the pattern represented by
      * this object. In case of a successful match the resulting {@link MatchConditions} with the

key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java

@@ -16,7 +16,6 @@
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.PosInProgram;
 import de.uka.ilkd.key.logic.ProgramPrefix;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 import de.uka.ilkd.key.util.Debug;
 
 import org.key_project.util.ExtList;

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java

@@ -12,7 +12,6 @@
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.ProgramElementName;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ConstructorDeclaration.java

@@ -5,14 +5,14 @@
 
 import java.util.List;
 
+import com.github.javaparser.ast.jml.clauses.JmlContract;
 import de.uka.ilkd.key.java.ast.Comment;
 import de.uka.ilkd.key.java.ast.PositionInfo;
 import de.uka.ilkd.key.java.ast.StatementBlock;
 import de.uka.ilkd.key.java.ast.abstraction.Constructor;
 import de.uka.ilkd.key.java.ast.reference.TypeReference;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.ProgramElementName;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
@@ -63,7 +63,7 @@ public ConstructorDeclaration(PositionInfo pi, List<Comment> c, ImmutableArray<M
             TypeReference o, Comment[] comments, ProgramElementName name,
             ImmutableArray<ParameterDeclaration> map1,
             Throws exceptions, StatementBlock body, boolean parentIsInterfaceDeclaration,
-            List<TextualJMLConstruct> specs) {
+            List<JmlContract> specs) {
         super(pi, c, map, o, comments, name, map1, exceptions, body, parentIsInterfaceDeclaration,
             ImmutableList.fromList(specs));
     }

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InterfaceDeclaration.java

@@ -24,7 +24,6 @@
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.ProgramElementName;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/JavaDeclaration.java

@@ -18,12 +18,12 @@
 
 import java.util.List;
 
+import com.github.javaparser.ast.jml.clauses.JmlContract;
 import de.uka.ilkd.key.java.ast.Comment;
 import de.uka.ilkd.key.java.ast.Declaration;
 import de.uka.ilkd.key.java.ast.JavaNonTerminalProgramElement;
 import de.uka.ilkd.key.java.ast.PositionInfo;
 import de.uka.ilkd.key.java.ast.declaration.modifier.*;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
@@ -39,7 +39,7 @@
 
 public abstract class JavaDeclaration extends JavaNonTerminalProgramElement implements Declaration {
 
-    protected final ImmutableList<TextualJMLConstruct> attachedJml;
+    protected final ImmutableList<JmlContract> attachedJml;
 
 
     /**
@@ -53,7 +53,7 @@ public abstract class JavaDeclaration extends JavaNonTerminalProgramElement impl
 
     public JavaDeclaration(PositionInfo pi, List<Comment> comments,
             @NonNull ImmutableArray<Modifier> modArray,
-            ImmutableList<TextualJMLConstruct> attachedJml) {
+            ImmutableList<JmlContract> attachedJml) {
         super(pi, comments);
         this.modArray = modArray;
         this.attachedJml = attachedJml;
@@ -89,7 +89,7 @@ public JavaDeclaration(ExtList children) {
         super(children);
         modArray = new ImmutableArray<>(children.collect(Modifier.class));
         this.attachedJml =
-            ImmutableList.fromList(List.of(children.collect(TextualJMLConstruct.class)));
+            ImmutableList.fromList(List.of(children.collect(JmlContract.class)));
     }
 
 
@@ -115,7 +115,7 @@ public VisibilityModifier getVisibilityModifier() {
 
 
     @Override
-    public ImmutableList<TextualJMLConstruct> getAttachedJml() {
+    public ImmutableList<JmlContract> getAttachedJml() {
         return attachedJml;
     }
 

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java

@@ -5,6 +5,7 @@
 
 import java.util.List;
 
+import com.github.javaparser.ast.jml.clauses.JmlContract;
 import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.ast.abstraction.Method;
@@ -13,7 +14,6 @@
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 import de.uka.ilkd.key.speclang.njml.SpecMathMode;
 
 import org.key_project.util.ExtList;
@@ -94,7 +94,7 @@ public MethodDeclaration(
             Comment[] voidComments, ProgramElementName name,
             ImmutableArray<ParameterDeclaration> parameters, Throws exceptions,
             StatementBlock body, boolean parentIsInterfaceDeclaration,
-            ImmutableList<TextualJMLConstruct> attachedJml) {
+            ImmutableList<JmlContract> attachedJml) {
         super(pi, comments, modArray, attachedJml);
         this.returnType = returnType;
         this.voidComments = voidComments;

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java

@@ -12,7 +12,6 @@
 import de.uka.ilkd.key.java.ast.expression.literal.NullLiteral;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 import de.uka.ilkd.key.speclang.njml.SpecMathMode;
 
 import org.key_project.util.ExtList;

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Do.java

@@ -8,7 +8,6 @@
 import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.visitor.Visitor;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableList;

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/EnhancedFor.java

@@ -9,7 +9,6 @@
 import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration;
 import de.uka.ilkd.key.java.visitor.CreatingASTVisitor;
 import de.uka.ilkd.key.java.visitor.Visitor;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableList;

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/For.java

@@ -10,7 +10,6 @@
 import de.uka.ilkd.key.java.ast.declaration.VariableSpecification;
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.visitor.Visitor;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java

@@ -9,7 +9,6 @@
 import de.uka.ilkd.key.java.ast.ProgramElement;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.nparser.KeyAst;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement;
 
 import org.key_project.util.ExtList;
 
@@ -27,7 +26,7 @@ public class JmlAssert extends JavaStatement {
     /**
      * the kind of the statement, assert or assume
      */
-    private final TextualJMLAssertStatement.Kind kind;
+    private final Kind kind;
 
     /**
      * the condition in parse tree form
@@ -42,7 +41,7 @@ public class JmlAssert extends JavaStatement {
      * @param positionInfo
      *        the position information for this statement
      */
-    public JmlAssert(TextualJMLAssertStatement.Kind kind, KeyAst.Expression condition,
+    public JmlAssert(Kind kind, KeyAst.Expression condition,
             PositionInfo positionInfo) {
         super(positionInfo);
         this.kind = kind;
@@ -55,15 +54,15 @@ public JmlAssert(TextualJMLAssertStatement.Kind kind, KeyAst.Expression conditio
      */
     public JmlAssert(ExtList children) {
         super(children);
-        this.kind = Objects.requireNonNull(children.get(TextualJMLAssertStatement.Kind.class));
+        this.kind = Objects.requireNonNull(children.get(Kind.class));
         this.condition = Objects.requireNonNull(children.get(KeyAst.Expression.class));
     }
 
     public JmlAssert(JmlAssert other) {
         this(other.kind, other.condition, other.getPositionInfo());
     }
 
-    public TextualJMLAssertStatement.Kind getKind() {
+    public Kind getKind() {
         return kind;
     }
 
@@ -166,4 +165,19 @@ public ProgramElement getChildAt(int index) {
     public void visit(Visitor v) {
         v.performActionOnJmlAssert(this);
     }
+
+    public enum Kind {
+        ASSERT("assert"), ASSUME("assume");
+
+        private final String name;
+
+        Kind(String name) {
+            this.name = name;
+        }
+
+        @Override
+        public String toString() {
+            return name;
+        }
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopStatement.java

@@ -8,7 +8,6 @@
 import de.uka.ilkd.key.java.*;
 import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.ast.expression.Expression;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MergePointStatement.java

@@ -23,8 +23,6 @@
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMergePointDecl;
 
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableList;

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java

@@ -5,24 +5,23 @@
 
 import java.util.List;
 
+import com.github.javaparser.ast.key.KeyTransactionStmt;
 import de.uka.ilkd.key.java.*;
 import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.rule.MatchConditions;
 
-import com.github.javaparser.ast.key.KeyTransactionStatement;
-
 public class TransactionStatement extends JavaStatement {
-    private final KeyTransactionStatement.TransactionType type;
+    private final KeyTransactionStmt.TransactionType type;
 
-    public TransactionStatement(KeyTransactionStatement.TransactionType type) {
+    public TransactionStatement(KeyTransactionStmt.TransactionType type) {
         super();
         this.type = type;
     }
 
     public TransactionStatement(
             PositionInfo pi, List<Comment> c,
-            KeyTransactionStatement.TransactionType type) {
+            KeyTransactionStmt.TransactionType type) {
         super(pi, c);
         this.type = type;
     }

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/While.java

@@ -8,7 +8,6 @@
 import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.visitor.Visitor;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableList;