JML Lemmas and proof scripts in model methods

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

@@ -70,6 +70,7 @@ PURE: 'pure';
 RETURN_BEHAVIOR: 'return_' BEHAVIOR;
 FINAL: 'final';
 MODEL: 'model'/*  -> pushMode(expr)*/;
+LEMMA: 'lemma' -> pushMode(expr);
 
 fragment Pred: '_redundantly'?; //suffix
 fragment Pfree: '_free'?;       //suffix
@@ -139,6 +140,7 @@ SEPARATES: 'separates' -> pushMode(expr);
 SET: 'set' -> pushMode(expr);
 SIGNALS: ('signals' Pred | 'exsures' Pred) -> pushMode(expr);
 SIGNALS_ONLY: 'signals_only' Pred -> pushMode(expr);
+USE_LEMMA: 'use_lemma' -> pushMode(expr);
 VAR: 'var';
 WHEN: 'when' Pred -> pushMode(expr);
 WORKING_SPACE: 'working_space' Pred -> pushMode(expr);

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

@@ -22,6 +22,7 @@ classlevel_element0: modifiers? (classlevel_element modifiers?);
 classlevel_element
   : class_invariant     | accessible_clause  | method_specification
   | method_declaration  | field_declaration  | represents_clause
+  | lemma_declaration
   | history_constraint  | initially_clause   | class_axiom
   | monitors_for_clause | readable_if_clause | writable_if_clause
   | datagroup_clause    | set_statement      | nowarn_pragma
@@ -33,7 +34,7 @@ methodlevel_element
   : field_declaration | set_statement | merge_point_statement
   | loop_specification | assert_statement | assume_statement | nowarn_pragma
   | debug_statement | block_specification | block_loop_specification
-  | assert_statement | assume_statement
+  | assert_statement | assume_statement | use_lemma_statement
  ;
 
 modifiers: modifier+;
@@ -157,13 +158,15 @@ name_clause: SPEC_NAME STRING_LITERAL SEMICOLON ;
 
 field_declaration: typespec IDENT (LBRACKET RBRACKET)* initialiser? SEMI_TOPLEVEL;
 method_declaration: typespec IDENT param_list (method_body=mbody_block | SEMI_TOPLEVEL);
-mbody_block: LBRACE mbody_var* mbody_statement RBRACE;
+mbody_block: LBRACE (mbody_var | assert_statement)* mbody_statement RBRACE;
 mbody_statement:
     RETURN expression SEMI_TOPLEVEL #mbody_return
   | IF LPAREN expression RPAREN (mbody_statement | mbody_block) ELSE (mbody_statement | mbody_block) #mbody_if
   ;
 mbody_var: VAR? IDENT EQUAL_SINGLE expression SEMI_TOPLEVEL;
 
+lemma_declaration: LEMMA IDENT param_list assertionProof SEMI_TOPLEVEL;
+
 param_list: LPAREN (param_decl (COMMA param_decl)*)? RPAREN;
 param_decl: ((NON_NULL | NULLABLE))? typespec p=IDENT (LBRACKET RBRACKET)*;
 history_constraint: CONSTRAINT expression;
@@ -176,6 +179,7 @@ maps_into_clause: MAPS expression;
 nowarn_pragma: NOWARN expression;
 debug_statement: DEBUG expression;
 set_statement: SET (assignee=expression) EQUAL_SINGLE (value=expression) SEMI_TOPLEVEL;
+use_lemma_statement: USE_LEMMA postfixexpr SEMI_TOPLEVEL;
 merge_point_statement:
   MERGE_POINT
   (MERGE_PROC (proc=STRING_LITERAL))?

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

@@ -94,7 +94,8 @@ private void print(List<TextualJMLConstruct> spec) {
                 }
                 case TextualJMLInitially c -> print(c.getModifiers(), c.getInv().first);
                 case TextualJMLMergePointDecl c -> print(c.getModifiers(), c.getMergeProc());
-                case TextualJMLMethodDecl c -> print(c.getModifiers(), c.getDecl());
+                case TextualJMLMethodOrLemmaDecl c ->
+                    print(c.getModifiers(), c.getMethodDefinition());
                 case TextualJMLModifierList c -> print(c.getModifiers());
                 case TextualJMLRepresents c -> print(c.getModifiers(), c.getRepresents().first);
                 case TextualJMLSetStatement c -> print(c.getAssignment());

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

@@ -14,6 +14,7 @@
 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.jml.pretranslation.TextualJMLLemmaDecl;
 import de.uka.ilkd.key.speclang.njml.SpecMathMode;
 
 import org.key_project.util.ExtList;
@@ -424,6 +425,11 @@ public boolean isModel() {
         return super.isModel();
     }
 
+    public boolean isLemma() {
+        return attachedJml.stream().anyMatch(TextualJMLLemmaDecl.class::isInstance);
+    }
+
+
     @Override
     public int getStateCount() {
         return super.getStateCount();

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

@@ -55,6 +55,7 @@ public enum ModifierKind {
     JML_CODE("code"),
     JML_OT_PEER("peer"),
     JML_OT_REP("rep"),
+    JML_LEMMA("lemma"),
     JML_OT_READ_ONLY("read_only");
 
     private final String codeRepresentation;

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

@@ -0,0 +1,63 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.ast.statement;
+
+import de.uka.ilkd.key.java.ast.PositionInfo;
+import de.uka.ilkd.key.java.ast.ProgramElement;
+import de.uka.ilkd.key.java.visitor.Visitor;
+import de.uka.ilkd.key.speclang.njml.JmlParser;
+
+/**
+ * JML use_lemma statement
+ *
+ * @author Mattias Ulbrich
+ */
+public class UseLemmaStatement extends JavaStatement {
+
+    /**
+     * The parser context of the statement produced during parsing.
+     */
+    private final JmlParser.PostfixexprContext context;
+
+    /** Constructor used in recoderext */
+    public UseLemmaStatement(JmlParser.PostfixexprContext context, PositionInfo positionInfo) {
+        super(positionInfo);
+        this.context = context;
+    }
+
+    /** Constructor used when cloning */
+    public UseLemmaStatement(UseLemmaStatement copyFrom) {
+        this(copyFrom.context, copyFrom.getPositionInfo());
+    }
+
+    /**
+     * Removes the attached parser context from this set statement
+     *
+     * @return the parser context that was attached
+     */
+    public JmlParser.PostfixexprContext getParserContext() {
+        return context;
+    }
+
+    /** {@inheritDoc} */
+    @Override
+    public void visit(Visitor v) {
+        v.performActionOnUseLemmaStatement(this);
+    }
+
+    @Override
+    public int getChildCount() {
+        return 0;
+    }
+
+    @Override
+    public ProgramElement getChildAt(int index) {
+        throw new IndexOutOfBoundsException("UseLemmaStatement has no program children");
+    }
+
+    @Override
+    protected int computeHashCode() {
+        return System.identityHashCode(this);
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java

@@ -40,6 +40,7 @@
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMergePointDecl;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLUseLemmaStatement;
 
 import org.key_project.logic.MetaSpace;
 import org.key_project.logic.Namespace;
@@ -775,6 +776,10 @@ public Object visit(KeYMarkerStatement n, Void arg) {
                 KeyAst.SetStatementContext context = n.getData(MarkerStatementHelper.KEY_ASSIGN);
                 yield new SetStatement(context, pi);
             }
+            case MarkerStatementHelper.KIND_USE_LEMMA -> {
+                TextualJMLUseLemmaStatement stm = n.getData(MarkerStatementHelper.KEY_USE_LEMMA);
+                yield new UseLemmaStatement(stm.getExpression(), pi);
+            }
 
 
             case MarkerStatementHelper.KIND_MERGE_POINT -> {

key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java

@@ -6,6 +6,7 @@
 import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMergePointDecl;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLUseLemmaStatement;
 
 import com.github.javaparser.ast.DataKey;
 
@@ -20,11 +21,14 @@ public class MarkerStatementHelper {
     public static final int KIND_ASSUME = 2;
     public static final int KIND_SET = 3;
     public static final int KIND_MERGE_POINT = 4;
+    public static final int KIND_USE_LEMMA = 5;
 
     public static final DataKey<KeyAst.SetStatementContext> KEY_ASSIGN = new DataKey<>() {
     };
     public static final DataKey<TextualJMLMergePointDecl> KEY_MERGE_POINT = new DataKey<>() {
     };
     public static final DataKey<TextualJMLAssertStatement> KEY_ASSERT = new DataKey<>() {
     };
+    public static final DataKey<TextualJMLUseLemmaStatement> KEY_USE_LEMMA = new DataKey<>() {
+    };
 }

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java

@@ -191,7 +191,7 @@ public JMLTransformer(TransformationPipelineServices services) {
      * @return the new method declaration
      * @throws SLTranslationException
      */
-    private @NonNull MethodDeclaration transformMethodDecl(TextualJMLMethodDecl decl,
+    private @NonNull MethodDeclaration transformMethodDecl(TextualJMLMethodOrLemmaDecl decl,
             @Nullable TextualJMLModifierList jmlModifiers)
             throws SLTranslationException {
         // prepend Java modifiers
@@ -248,6 +248,13 @@ private Statement transformSetStatement(TextualJMLSetStatement stat) {
         return stmt;
     }
 
+
+    private Statement transformUseLemmaStatement(TextualJMLUseLemmaStatement stat) {
+        KeYMarkerStatement stmt = new KeYMarkerStatement(KIND_USE_LEMMA);
+        stmt.setData(KEY_USE_LEMMA, stat);
+        return stmt;
+    }
+
     private KeYMarkerStatement transformMergePointDecl(TextualJMLMergePointDecl stat) {
         KeYMarkerStatement mps = new KeYMarkerStatement(KIND_MERGE_POINT);
         mps.setData(KEY_MERGE_POINT, stat);
@@ -294,7 +301,7 @@ private void transformClassLevelComments(TypeDeclaration<?> td) throws SLTransla
                     if (c instanceof TextualJMLFieldDecl fd) {
                         // ghost/model field decl.: transform into "real" field decl.
                         td.addMember(transformClassFieldDecl(fd));
-                    } else if (c instanceof TextualJMLMethodDecl md) {
+                    } else if (c instanceof TextualJMLMethodOrLemmaDecl md) {
                         // model method decl.:
                         final MethodDeclaration decl = transformMethodDecl(md, jmlModifiers);
                         jmlModifiers = null; // these are used now
@@ -325,6 +332,8 @@ private void transformClassLevelComments(TypeDeclaration<?> td) throws SLTransla
                         String errorMessage = switch (c) {
                             case TextualJMLSetStatement a ->
                                 "A set assignment only allowed inside of a method body";
+                            case TextualJMLUseLemmaStatement a ->
+                                "A use_lemma statement is only allowed inside of a method body";
                             case TextualJMLMergePointDecl a ->
                                 "Merge points are only allowed inside of a method body";
                             case TextualJMLLoopSpec a ->
@@ -442,6 +451,8 @@ private void transformMethodLevelCommentsAt(BlockStmt blockStmt, URI fileName)
                         // local ghost variable declaration!
                         case TextualJMLFieldDecl field -> statement = transformVariableDecl(field);
                         case TextualJMLSetStatement set -> statement = transformSetStatement(set);
+                        case TextualJMLUseLemmaStatement ulema ->
+                            statement = transformUseLemmaStatement(ulema);
                         case TextualJMLMergePointDecl mergePointDecl ->
                             statement = transformMergePointDecl(mergePointDecl);
                         case TextualJMLAssertStatement assertStatement ->

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

@@ -607,6 +607,19 @@ ProgramElement createNewElement(ExtList changeList) {
         def.doAction(x);
     }
 
+    @Override
+    public void performActionOnUseLemmaStatement(UseLemmaStatement x) {
+        DefaultAction def = new DefaultAction(x) {
+            @Override
+            ProgramElement createNewElement(ExtList changeList) {
+                // there are no AST elements below the use lemma statement, so we can use the copy
+                // constructor.
+                return new UseLemmaStatement(x);
+            }
+        };
+        def.doAction(x);
+    }
+
     @Override
     public void performActionOnReturn(Return x) {
         DefaultAction def = new DefaultAction(x) {

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

@@ -216,6 +216,11 @@ public void performActionOnSetStatement(SetStatement x) {
         doDefaultAction(x);
     }
 
+    @Override
+    public void performActionOnUseLemmaStatement(UseLemmaStatement x) {
+        doDefaultAction(x);
+    }
+
     @Override
     public void performActionOnDefault(Default x) {
         doDefaultAction(x);

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

@@ -149,6 +149,8 @@ public interface Visitor {
 
     void performActionOnSetStatement(SetStatement x);
 
+    void performActionOnUseLemmaStatement(UseLemmaStatement x);
+
     void performActionOnConditional(Conditional x);
 
     void performActionOnNewArray(NewArray x);

key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java

@@ -226,6 +226,10 @@ public boolean isModel() {
         return method.isModel();
     }
 
+    public boolean isLemma() {
+        return method.isLemma();
+    }
+
     /**
      * Test whether the declaration is strictfp.
      */