list contracts in methods and constructors are mandatory

JmlMetaModel.plantuml

@@ -0,0 +1,248 @@
+@startuml
+
+package "Java" #DDDDDD {
+	abstract class Statement
+	abstract class Expression
+	abstract class BodyDeclaration
+
+	abstract class Callable
+	class Method extends Callable
+	class Constructor extends Callable
+	/'(Callable,"JML".JmlContract) . JmlContainer'/
+	abstract class Type
+
+	class BlockStmt extends Statement
+	BlockStmt -> "*" Statement
+}
+
+package "JML" #DFEFEF {
+interface JmlContainer {
+	tags : List<String>
+}
+
+/'class Jmlish
+class DefaultJmlContainer '/
+abstract class JmlBodyDeclaration
+enum Behavior {
+    NONE
+    BEHAVIOR
+    NORMAL
+    ABRUPT
+    EXCEPTIONAL
+    MODEL
+    BREAK
+    CONTINUE
+    RETURN
+}
+abstract class JmlStatement extends Java.Statement, JmlContainer
+class JmlBeginStmt extends JmlStatement {
+
+}
+class JmlUnreachableStmt extends JmlStatement
+class JmlExpressionStmt extends JmlStatement {
+	/'expression: Java.Expression'/
+}
+JmlExpressionStmt -> Java.Expression
+
+class JmlGhostStmt extends JmlStatement {
+	stmt : Java.Statement
+}
+class JmlRefiningStmt extends JmlStatement
+JmlRefiningStmt -> JmlContract
+
+class JmlLabelStmt extends JmlStatement {
+	label: Java.SimpleName
+}
+
+class JmlEndStmt extends JmlStatement {}
+class JmlLetExpr extends Java.Expression {
+	variables: Java.VariableDeclarationExpr
+	expression: Java.Expression
+}
+abstract class JmlClassLevel extends JmlContainer
+class JmlRepresentsDeclaration extends JmlClassLevel
+class JmlFieldDeclaration extends JmlClassLevel
+class JmlMethodDeclaration extends JmlClassLevel
+class JmlClassAccessibleDeclaration extends JmlClassLevel
+class JmlClassExprDeclaration extends JmlClassLevel {
+	kind : SimpleName
+    name : SimpleName
+    modifiers : NodeList<Modifier>
+    expression : Java.Expression
+    jmlTags: List<SimpleName>
+}
+
+class JmlQuantifiedExpr extends Java.Expression {
+    /'private JmlBinder binder;'/
+    variables : List<Java.Parameter>
+    expressions : List<Java.Expression>
+}
+JmlQuantifiedExpr -> Quantifier
+enum Quantifier {
+        FORALL
+        EXISTS
+        NUM_OF
+        MIN
+        MAX
+        SUM
+        BSUM
+        UNION
+        SEQDEF
+        PRODUCT
+        CHOOSE
+}
+
+abstract class JmlClause {
+	name : SimpleName
+}
+JmlClause ---> JmlClauseKind
+enum JmlClauseKind {
+    ENSURES
+    ENSURES_FREE
+    ENSURES_REDUNDANTLY
+    REQUIRES
+    REQUIRES_FREE
+    REQUIRES_REDUNDANTLY
+    DECREASES
+    MODIFIES
+    MODIFIABLE
+    ASSIGNABLE
+    ACCESSIBLE
+    PRE
+    POST
+    PRE_REDUNDANTLY
+    POST_REDUNDANTLY
+    MAINTAINING
+    MAINTAINING_REDUNDANTLY
+    DECREASING
+    DECREASES_REDUNDANTLY
+    LOOP_INVARIANT
+    LOOP_INVARIANT_FREE
+    LOOP_INVARIANT_REDUNDANTLY
+    MEASURED_BY
+    RETURNS
+    RETURNS_REDUNDANTLY
+    BREAKS
+    BREAKS_REDUNDANTLY
+    CONTINUES
+    CONTINUES_REDUNDANTLY
+    OLD
+    FORALL
+    SIGNALS
+    SIGNALS_REDUNDANTLY
+    SIGNALS_ONLY
+    WHEN
+    WORKING_SPACE
+    WORKING_SPACE_REDUNDANTLY
+    CAPTURES
+    CAPTURES_REDUNDANTLY
+    INITIALLY
+    INVARIANT_REDUNDANTLY
+    INVARIANT
+    ASSIGNABLE_REDUNDANTLY
+    MODIFIABLE_REDUNDANTLY
+    MODIFIES_REDUNDANTLY
+    CALLABLE
+    CALLABLE_REDUNDANTLY
+    DIVERGES
+    DIVERGES_REDUNDANTLY
+    DURATION
+    DURATION_REDUNDANTLY
+    NONE
+}
+
+class JmlClauseIf extends JmlClause
+class JmlMultiExprClause extends JmlClause {
+        heaps : NodeList<SimpleName>
+}
+JmlMultiCompareExpr "*" -> "1" JmlClauseKind
+JmlMultiCompareExpr "*" -> "*" Java.Expression
+
+class JmlSimpleExprClause extends JmlClause {
+	/'expression : Java.Expression'/
+}
+JmlSimpleExprClause "*" -> "1" Java.Expression
+
+class JmlAccessibleClause extends JmlClause
+class JmlClauseLabel extends JmlClause {
+	label:Java.SimpleName
+	expression:Java.Expression
+
+}
+
+class JmlOldClause extends JmlClause {
+    declarations : Java.VariableDeclarationExpr
+}
+class JmlCallableClause extends JmlClause {
+
+}
+class JmlForallClause extends JmlClause {
+    boundedVariables : NodeList<Parameter>
+}
+class JmlCapturesClause extends JmlClause
+class JmlSignalsClause extends JmlClause {
+	parameter: Java.Parameter
+	expression: Java.Expression
+}
+class JmlSignalsOnlyClause extends JmlClause {
+	type: Java.Type
+}
+class JmlMultiCompareExpr extends Java.Expression
+class JmlImportDeclaration
+class JmlSetComprehension extends Java.Expression {
+	binding : Java.VariableDeclarator
+	predicate : Java.Expression
+}
+
+class JmlLogicType extends Java.Type
+JmlLogicType -> LogicPrimitiveType
+enum LogicPrimitiveType {
+	\seq
+	\map
+	\set
+	\bigint
+	\bigfloat
+}
+
+class JmlLabelExpr extends Java.Expression
+abstract class JmlBodyDeclaration extends Java.BodyDeclaration
+
+class JmlContract extends JmlContainer {
+	/'type : ContractType'/
+	name : Java.SimpleName
+	modifiers : List<Modifier>
+}
+JmlContract "1" --> "*" JmlContract
+JmlContract "1" --> "*" JmlClause
+JmlContract -> ContractType
+
+enum ContractType{
+	METHOD
+	LAMBDA
+	LOOP
+	LOOP_INV
+	STATEMENT
+	BLOCK
+}
+JmlContract -> Behavior
+
+enum JmlStmtKind {
+	ASSERT
+	ASSERT_REDUNDANTLY
+	ASSUME
+	ASSUME_REDUNDANTLY
+	HENCE_BY
+	HENCE_BY_REDUNDANTLY
+	SET
+}
+
+JmlExpressionStmt -> JmlStmtKind
+
+}
+
+Java.Callable "+ contracts 1" -> "0..*" JML.JmlContract
+
+Java.BlockStmt "+ contracts 1" -> "*" JML.JmlContract
+
+
+@enduml

javaparser-core-testing/src/test/java/com/github/javaparser/JKIssue.java

@@ -38,7 +38,7 @@ void test() throws IOException {
 
         var methods = cu.getPrimaryType().get().getMethods();
         for (var method : methods) {
-            Assertions.assertEquals(1, method.getContracts().get().size());
+            Assertions.assertEquals(1, method.getContracts().size());
         }
     }
 
@@ -50,7 +50,7 @@ void test2() throws IOException {
         CompilationUnit cu = parser.parse(Paths.get("src/test/test_sourcecode/MissingParentSimpleExprClause.java"))
                 .getResult().get();
 
-        var clause = cu.getType(0).getMethods().get(0).getContracts().get().get(0).getClauses().get(0).asJmlSimpleExprClause();
+        var clause = cu.getType(0).getMethods().get(0).getContracts().get(0).getClauses().get(0).asJmlSimpleExprClause();
         Assertions.assertEquals(1, clause.getChildNodes().size());
     }
 }

javaparser-core/src/main/java/com/github/javaparser/ast/body/CallableDeclaration.java

@@ -47,7 +47,7 @@
 /**
  * Represents a declaration which is callable eg. a method or a constructor.
  */
-public abstract class CallableDeclaration<T extends CallableDeclaration<?>> extends BodyDeclaration<T> implements NodeWithAccessModifiers<T>, NodeWithDeclaration, NodeWithSimpleName<T>, NodeWithParameters<T>, NodeWithThrownExceptions<T>, NodeWithTypeParameters<T>, NodeWithJavadoc<T>, NodeWithAbstractModifier<T>, NodeWithStaticModifier<T>, NodeWithFinalModifier<T>, NodeWithStrictfpModifier<T>, NodeWithContracts<CallableDeclaration> {
+public abstract class CallableDeclaration<T extends CallableDeclaration<?>> extends BodyDeclaration<T> implements NodeWithAccessModifiers<T>, NodeWithDeclaration, NodeWithSimpleName<T>, NodeWithParameters<T>, NodeWithThrownExceptions<T>, NodeWithTypeParameters<T>, NodeWithJavadoc<T>, NodeWithAbstractModifier<T>, NodeWithStaticModifier<T>, NodeWithFinalModifier<T>, NodeWithStrictfpModifier<T>, NodeWithContracts<T> {
 
     private NodeList<Modifier> modifiers;
 
@@ -62,7 +62,6 @@ public abstract class CallableDeclaration<T extends CallableDeclaration<?>> exte
     @OptionalProperty
     private ReceiverParameter receiverParameter;
 
-    @OptionalProperty
     private NodeList<JmlContract> contracts = new NodeList<>();
 
     @AllFieldsConstructor
@@ -450,8 +449,8 @@ public Optional<CallableDeclaration> toCallableDeclaration() {
     }
 
     @Generated("com.github.javaparser.generator.core.node.PropertyGenerator")
-    public Optional<NodeList<JmlContract>> getContracts() {
-        return Optional.ofNullable(contracts);
+    public NodeList<JmlContract> getContracts() {
+        return contracts;
     }
 
     @Generated("com.github.javaparser.generator.core.node.PropertyGenerator")

javaparser-core/src/main/java/com/github/javaparser/ast/expr/LambdaExpr.java

@@ -29,6 +29,8 @@
 import com.github.javaparser.ast.Node;
 import com.github.javaparser.ast.NodeList;
 import com.github.javaparser.ast.body.Parameter;
+import com.github.javaparser.ast.jml.NodeWithContracts;
+import com.github.javaparser.ast.jml.clauses.JmlContract;
 import com.github.javaparser.ast.nodeTypes.NodeWithParameters;
 import com.github.javaparser.ast.observer.ObservableProperty;
 import com.github.javaparser.ast.stmt.BlockStmt;
@@ -58,14 +60,16 @@
  *
  * @author Raquel Pau
  */
-public class LambdaExpr extends Expression implements NodeWithParameters<LambdaExpr> {
+public class LambdaExpr extends Expression implements NodeWithParameters<LambdaExpr>, NodeWithContracts<LambdaExpr> {
 
     private NodeList<Parameter> parameters;
 
     private boolean isEnclosingParameters;
 
     private Statement body;
 
+    private NodeList<JmlContract> contracts = new NodeList<>();
+
     public LambdaExpr() {
         this(null, new NodeList<>(), new ReturnStmt(), false);
     }
@@ -279,4 +283,15 @@ public boolean isPolyExpression() {
     public boolean isExplicitlyTyped() {
         return getParameters().stream().allMatch(p -> !(p.getType().isUnknownType()));
     }
+
+    @Override
+    public NodeList<JmlContract> getContracts() {
+        return contracts;
+    }
+
+    @Override
+    public LambdaExpr setContracts(NodeList<JmlContract> contracts) {
+        this.contracts = contracts;
+        return this;
+    }
 }

javaparser-core/src/main/java/com/github/javaparser/ast/jml/JmlModelProgram.java

@@ -13,7 +13,6 @@
 import com.github.javaparser.ast.visitor.GenericVisitor;
 import com.github.javaparser.ast.visitor.VoidVisitor;
 import com.github.javaparser.metamodel.OptionalProperty;
-import java.util.Optional;
 
 /**
  * @author Alexander Weigl
@@ -53,8 +52,8 @@ public <A> void accept(VoidVisitor<A> v, A arg) {
     }
 
     @Override
-    public Optional<NodeList<JmlContract>> getContracts() {
-        return Optional.of(contracts);
+    public NodeList<JmlContract> getContracts() {
+        return contracts;
     }
 
     @Override

javaparser-core/src/main/java/com/github/javaparser/ast/jml/NodeWithContracts.java

@@ -1,34 +1,24 @@
 package com.github.javaparser.ast.jml;
 
-import com.github.javaparser.ast.Generated;
 import com.github.javaparser.ast.Node;
 import com.github.javaparser.ast.NodeList;
 import com.github.javaparser.ast.jml.clauses.JmlContract;
 import com.github.javaparser.jml.JmlUtility;
-import java.util.Optional;
 
 /**
  * @author Alexander Weigl
  * @version 1 (12/9/21)
  */
 public interface NodeWithContracts<T extends Node> {
 
-    @Generated("com.github.javaparser.generator.core.node.PropertyGenerator")
-    Optional<NodeList<JmlContract>> getContracts();
+    NodeList<JmlContract> getContracts();
 
-    @Generated("com.github.javaparser.generator.core.node.PropertyGenerator")
     T setContracts(NodeList<JmlContract> contracts);
 
     default void addContracts(JmlContract contracts) {
-        final var o = getContracts();
-        if (o.isPresent()) {
-            final var jmlContracts = o.get();
-            jmlContracts.add(contracts);
-            if (jmlContracts.size() == 1)
-                JmlUtility.fixRangeContracts(this);
-        } else {
-            setContracts(new NodeList<>(contracts));
+        final var jmlContracts = getContracts();
+        jmlContracts.add(contracts);
+        if (jmlContracts.size() == 1)
             JmlUtility.fixRangeContracts(this);
-        }
     }
 }