Proof Scripts in JML

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java

@@ -117,7 +117,7 @@ public Strategy<Goal> create(Proof proof, StrategyProperties sp) {
          */
         @Override
         public StrategySettingsDefinition getSettingsDefinition() {
-            return JavaProfile.DEFAULT.getSettingsDefinition();
+            return JavaProfile.getDefault().getSettingsDefinition();
         }
     }
 }

key.core/build.gradle

@@ -111,6 +111,7 @@ classes.dependsOn << generateSolverPropsList
 
 tasks.withType(Test) {
     enableAssertions = true
+    systemProperties(System.properties.findAll { key, value -> key.startsWith("key.") })
 }
 
 

key.core/src/main/antlr4/JmlLexer.g4

@@ -175,6 +175,8 @@ mode expr;
 /* Java keywords */
 BOOLEAN: 'boolean';
 BYTE: 'byte';
+CASE: 'case';
+DEFAULT: 'default';
 FALSE: 'false';
 INSTANCEOF: 'instanceof';
 INT: 'int';
@@ -244,6 +246,7 @@ FP_SUBNORMAL: '\\fp_subnormal';   //KeY extension, not official JML
 FP_ZERO: '\\fp_zero';   //KeY extension, not official JML
 FREE: '\\free';  //KeY extension, not official JML
 FRESH: '\\fresh';
+FROM_GOAL: '\\from_goal';  //KeY extension, not official JML
 INDEX: '\\index';
 INDEXOF: '\\seq_indexOf';  //KeY extension, not official JML
 INTERSECT: '\\intersect';  //KeY extension, not official JML

key.core/src/main/antlr4/JmlParser.g4

@@ -9,9 +9,11 @@ options { tokenVocab=JmlLexer; }
 @members {
   private SyntaxErrorReporter errorReporter = new SyntaxErrorReporter(getClass());
   public SyntaxErrorReporter getErrorReporter() { return errorReporter;}
+  private boolean isNextToken(String tokenText) {
+    return _input.LA(1) != Token.EOF && tokenText.equals(_input.LT(1).getText());
+  }
 }
 
-
 classlevel_comments: classlevel_comment* EOF;
 classlevel_comment: classlevel_element | modifiers | set_statement;
 classlevel_element0: modifiers? (classlevel_element modifiers?);
@@ -202,12 +204,35 @@ block_specification: method_specification;
 block_loop_specification:
   loop_contract_keyword spec_case ((also_keyword)+ loop_contract_keyword spec_case)*;
 loop_contract_keyword: LOOP_CONTRACT;
-assert_statement: (ASSERT expression | UNREACHABLE) SEMI_TOPLEVEL;
+assert_statement: (ASSERT (label=IDENT COLON)? expression | UNREACHABLE) (assertionProof SEMI_TOPLEVEL? | SEMI_TOPLEVEL);
 //breaks_clause: BREAKS expression;
 //continues_clause: CONTINUES expression;
 //returns_clause: RETURNS expression;
 
 
+// --- proof scripts in JML
+assertionProof: BY (proofCmd | LBRACE ( proofCmd )+ RBRACE) ;
+proofCmd:
+    // TODO allow more than one var in obtain
+  { isNextToken("obtain") }? obtain=IDENT typespec var=IDENT
+       ( obtKind=EQUAL_SINGLE expression SEMI
+       | obtKind=SUCH_THAT expression proofCmdSuffix
+       | obtKind=FROM_GOAL SEMI
+       )
+  | cmd=IDENT ( proofArg )* proofCmdSuffix
+  ;
+
+proofCmdSuffix:
+  SEMI | BY ( proofCmd | LBRACE (proofCmd+ | proofCmdCase+) RBRACE )
+  ;
+
+proofCmdCase:
+    CASE ( label=STRING_LITERAL )? COLON ( proofCmd )*
+  | DEFAULT COLON ( proofCmd )*
+  ;
+proofArg: (argLabel=IDENT COLON)? expression;
+// ---
+
 mergeparamsspec:
     MERGE_PARAMS
       LBRACE

key.core/src/main/antlr4/KeYLexer.g4

@@ -40,6 +40,7 @@ lexer grammar KeYLexer;
    }
 
     private Token tokenBackStorage = null;
+    // see: https://keyproject.github.io/key-docs/devel/NewKeyParser/#why-does-the-lexer-required-some-pieces-of-java-code
     @Override
     public void emit(Token token) {
        int MAX_K = 10;
@@ -219,6 +220,7 @@ AXIOMS : '\\axioms';
 PROBLEM : '\\problem';
 CHOOSECONTRACT : '\\chooseContract';
 PROOFOBLIGATION : '\\proofObligation';
+// for PROOF see: https://keyproject.github.io/key-docs/devel/NewKeyParser/#why-does-the-lexer-required-some-pieces-of-java-code
 PROOF : '\\proof';
 PROOFSCRIPT : '\\proofScript';
 CONTRACTS : '\\contracts';
@@ -389,6 +391,7 @@ LESSEQUAL: '<' '=' | '\u2264';
 LGUILLEMETS: '<' '<' | '«' | '‹';
 RGUILLEMETS: '>''>' | '»' | '›';
 IMPLICIT_IDENT: '<' '$'? (LETTER)+ '>' ('$lmtd')? -> type(IDENT);
+MATCH_IDENT: '?' IDENT?;
 
 EQV:	'<->' | '\u2194';
 CHAR_LITERAL

key.core/src/main/antlr4/KeYParser.g4

@@ -7,6 +7,7 @@ parser grammar KeYParser;
 @members {
 private SyntaxErrorReporter errorReporter = new SyntaxErrorReporter(getClass());
 public SyntaxErrorReporter getErrorReporter() { return errorReporter;}
+public boolean allowMatchId = false; // used in proof script parsing
 }
 
 options { tokenVocab=KeYLexer; } // use tokens from STLexer.g4
@@ -147,6 +148,7 @@ string_value: STRING_LITERAL;
 simple_ident
 :
     id=IDENT
+  | {allowMatchId}? id=MATCH_IDENT
 ;
 
 simple_ident_comma_list
@@ -873,7 +875,7 @@ proofScriptExpression:
   | integer
   | floatnum
   | string_literal
-  | LPAREN (term | seq) RPAREN
+  | LPAREN {allowMatchId=true;} (term | seq) {allowMatchId=false;} RPAREN
   | simple_ident
   | abbreviation
   | literals

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

@@ -18,6 +18,7 @@
 import de.uka.ilkd.key.speclang.SpecificationElement;
 import de.uka.ilkd.key.util.Debug;
 
+import org.jspecify.annotations.Nullable;
 import org.key_project.logic.Name;
 import org.key_project.logic.Namespace;
 import org.key_project.logic.sort.Sort;
@@ -430,7 +431,7 @@ public static boolean isVisibleTo(SpecificationElement ax, KeYJavaType visibleTo
     /**
      * returns a KeYJavaType having the given sort
      */
-    public KeYJavaType getKeYJavaType(Sort sort) {
+    public @Nullable KeYJavaType getKeYJavaType(Sort sort) {
         List<KeYJavaType> l = lookupSort2KJTCache(sort);
         if (l != null && l.size() > 0) {
             // Return first KeYJavaType found for sort.

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

@@ -964,7 +964,9 @@ public CatchAllStatement convert(de.uka.ilkd.key.java.recoderext.CatchAllStateme
      * @return the converted statement
      */
     public JmlAssert convert(de.uka.ilkd.key.java.recoderext.JmlAssert ja) {
-        return new JmlAssert(ja.getKind(), ja.getCondition(), positionInfo(ja));
+        return new JmlAssert(ja.getKind(), ja.getOptLabel(), ja.getCondition(),
+            ja.getAssertionProof(),
+            positionInfo(ja));
     }
 
     // ------------------- declaration ---------------------

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

@@ -96,7 +96,8 @@ public interface SourceElement extends SyntaxElement, EqualsModProperty<SourceEl
      * These are not syntactical equal, therefore false is returned.
      */
     @Override
-    default <V> boolean equalsModProperty(Object o, Property<SourceElement> property, V... v) {
+    default <V> boolean equalsModProperty(Object o, Property<? super SourceElement> property,
+            V... v) {
         if (!(o instanceof SourceElement)) {
             return false;
         }

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java

@@ -440,7 +440,8 @@ private void transformAssertStatement(TextualJMLAssertStatement stat,
 
         de.uka.ilkd.key.java.Position pos = ctx.getStartLocation().getPosition();
         final Kind kind = stat.getKind();
-        JmlAssert jmlAssert = new JmlAssert(kind, ctx);
+        JmlAssert jmlAssert =
+            new JmlAssert(kind, ctx, stat.getAssertionProof(), stat.getOptLabel());
         try {
             updatePositionInformation(jmlAssert, pos);
             doAttach(jmlAssert, astParent, childIndex);

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JmlAssert.java

@@ -6,6 +6,7 @@
 import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement;
 
+import org.jspecify.annotations.Nullable;
 import recoder.java.ProgramElement;
 import recoder.java.SourceVisitor;
 import recoder.java.Statement;
@@ -23,6 +24,10 @@ public class JmlAssert extends JavaStatement {
      */
     private final TextualJMLAssertStatement.Kind kind;
 
+    /**
+     * The optional proof for an assert statement (not for assume)
+     */
+    private final KeyAst.@Nullable JMLProofScript assertionProof;
 
     /**
      * The condition of this statement in parse tree form
@@ -31,12 +36,21 @@ public class JmlAssert extends JavaStatement {
     private final KeyAst.Expression condition;
 
     /**
-     * @param kind the kind of this statement
-     * @param condition the condition for this statement
+     * The optional label for this assertion (may be null)
      */
-    public JmlAssert(TextualJMLAssertStatement.Kind kind, KeyAst.Expression condition) {
+    private final @Nullable String optLabel;
+
+    public JmlAssert(TextualJMLAssertStatement.Kind kind, KeyAst.Expression condition,
+            String optLabel) {
+        this(kind, condition, null, optLabel);
+    }
+
+    public JmlAssert(TextualJMLAssertStatement.Kind kind, KeyAst.Expression condition,
+            KeyAst.@Nullable JMLProofScript assertionProof, String optLabel) {
         this.kind = kind;
         this.condition = condition;
+        this.assertionProof = assertionProof;
+        this.optLabel = optLabel;
     }
 
     /**
@@ -48,6 +62,8 @@ public JmlAssert(JmlAssert proto) {
         super(proto);
         this.kind = proto.kind;
         this.condition = proto.condition;
+        this.assertionProof = proto.assertionProof;
+        this.optLabel = proto.optLabel;
     }
 
     public TextualJMLAssertStatement.Kind getKind() {
@@ -58,6 +74,10 @@ public KeyAst.Expression getCondition() {
         return condition;
     }
 
+    public KeyAst.@Nullable JMLProofScript getAssertionProof() {
+        return assertionProof;
+    }
+
     @Override
     public int getChildCount() {
         return 0;
@@ -87,4 +107,8 @@ public void accept(SourceVisitor sourceVisitor) {
     public Statement deepClone() {
         return new JmlAssert(this);
     }
+
+    public String getOptLabel() {
+        return optLabel;
+    }
 }

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

@@ -8,10 +8,17 @@
 import de.uka.ilkd.key.java.PositionInfo;
 import de.uka.ilkd.key.java.ProgramElement;
 import de.uka.ilkd.key.java.visitor.Visitor;
+import de.uka.ilkd.key.logic.op.LocationVariable;
 import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement;
 
+import de.uka.ilkd.key.speclang.njml.JmlIO;
+import de.uka.ilkd.key.speclang.njml.JmlParser;
 import org.key_project.util.ExtList;
+import org.key_project.util.collection.ImmutableList;
+
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
 
 /**
  * A JML assert statement.
@@ -29,21 +36,36 @@ public class JmlAssert extends JavaStatement {
      */
     private final TextualJMLAssertStatement.Kind kind;
 
+    /*
+     * Temporary solution until full jml labels are there ...
+     * (To be clarified if compatible still)
+     */
+    private final String optLabel;
+
     /**
      * the condition in parse tree form
      */
-    private KeyAst.Expression condition;
+    private final KeyAst.Expression condition;
+
+    /**
+     * the assertion proof in parse tree form
+     */
+    private final KeyAst.@Nullable JMLProofScript assertionProof;
 
     /**
      * @param kind assert or assume
      * @param condition the condition of this statement
+     * @param assertionProof the optional proof for an assert statement (not for assume)
      * @param positionInfo the position information for this statement
      */
-    public JmlAssert(TextualJMLAssertStatement.Kind kind, KeyAst.Expression condition,
+    public JmlAssert(TextualJMLAssertStatement.Kind kind, String label, KeyAst.Expression condition,
+            KeyAst.@Nullable JMLProofScript assertionProof,
             PositionInfo positionInfo) {
         super(positionInfo);
         this.kind = kind;
+        this.optLabel = label;
         this.condition = condition;
+        this.assertionProof = assertionProof;
     }
 
     /**
@@ -52,11 +74,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.optLabel = children.get(String.class);
         this.condition = Objects.requireNonNull(children.get(KeyAst.Expression.class));
+        // script may be null
+        this.assertionProof = children.get(KeyAst.JMLProofScript.class);
     }
 
     public JmlAssert(JmlAssert other) {
-        this(other.kind, other.condition, other.getPositionInfo());
+        this(other.kind, other.optLabel, other.condition, other.assertionProof,
+            other.getPositionInfo());
     }
 
     public TextualJMLAssertStatement.Kind getKind() {
@@ -148,6 +174,10 @@ protected int computeHashCode() {
         return System.identityHashCode(this);
     }
 
+    public KeyAst.@Nullable JMLProofScript getAssertionProof() {
+        return assertionProof;
+    }
+
     @Override
     public int getChildCount() {
         return 0;
@@ -162,4 +192,30 @@ public ProgramElement getChildAt(int index) {
     public void visit(Visitor v) {
         v.performActionOnJmlAssert(this);
     }
+
+    /**
+     * This method collects all terms contained in this assertion. This is at least the condition.
+     * If there is a proof script, all terms in the proof script are collected as well.
+     *
+     * @return a freshly created list of at least one term
+     */
+    public @NonNull ImmutableList<JmlParser.ExpressionContext> collectTerms() {
+        ImmutableList<JmlParser.ExpressionContext> result = ImmutableList.of();
+        if (assertionProof != null) {
+            result = result.prepend(assertionProof.collectTerms());
+        }
+        result = result.prepend(condition.ctx);
+        return result;
+    }
+
+    public ImmutableList<LocationVariable> collectVariablesInProof(JmlIO io) {
+        if (assertionProof != null) {
+            return assertionProof.getObtainedProgramVars(io);
+        }
+        return ImmutableList.of();
+    }
+
+    public String getOptLabel() {
+        return optLabel;
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java

@@ -1513,6 +1513,8 @@ public void performActionOnJmlAssert(JmlAssert x) {
             ProgramElement createNewElement(ExtList changeList) {
                 changeList.add(x.getKind());
                 changeList.add(x.getCondition());
+                changeList.add(x.getAssertionProof());
+                changeList.add(x.getOptLabel());
                 return new JmlAssert(changeList);
             }
         };

key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java

@@ -349,7 +349,7 @@ protected int computeHashCode() {
     }
 
     @Override
-    public <V> boolean equalsModProperty(Object o, Property<JTerm> property, V... v) {
+    public <V> boolean equalsModProperty(Object o, Property<? super JTerm> property, V... v) {
         if (!(o instanceof JTerm other)) {
             return false;
         }

key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualsModProperty.java

@@ -49,7 +49,7 @@ public interface EqualsModProperty<T> {
      * @param <V> the type of the additional parameters needed by {@code property} for the
      *        comparison
      */
-    <V> boolean equalsModProperty(Object o, Property<T> property, V... v);
+    <V> boolean equalsModProperty(Object o, Property<? super T> property, V... v);
 
     /**
      * Computes the hash code according to the given ignored {@code property}.