JML should receive an Abstract Syntax Tree

[wadoon]

Description

The JML constructs should be represented in an AST together with Java. This allows us to simplify the KeY world sustainably. The following entities could be removed:

1. Specification repository
2. Rewriting of the contracts in the spec repo.
3. TextualJMLConstruct, JMLTransformer

The affected parts are huge:

• JMLSpecExtractor and Translator, removal of JML{Lexer,Parser}.g4.
• Rewriting a lot of rules, varcond, for the search for contracts.
• Contracts (semantically) could be created on the fly, rather eagerly, and put in the SpecificationRepository.

But we also need to otherthing our KeY-Java AST.

Steps

1. Reconsider the Java-AST.

   • Can we generate the AST for better efficiency?

   • Is it possible to remove ExtList?

     Currently needed to copy AST nodes with modified fields.

   • Get rid of the dozens of modifier and operator classes.

2. Implement JML class hierarchy. Here is the hierarchy of the jml parser:

   • JmlLogicType
   • Behavior
   • JmlStatement
     • JmlBeginStmt
     • JmlEndStmt
     • JmlUnreachableStmt
     • JmlExpressionStmt // assert, assume, ...
     • JmlGhostStmt // everything can be ghosted.
     • JmlRefiningStmt // constracts on BlockStmt and Stmts
     • JmlLabelStmt // spec-only labels
   • JmlClassLevelDeclaration
     • JmlRepresentsDeclaration
     • JmlFieldDeclaration // wrapper around FieldDeclaration
     • JmlMethodDeclaration // wrapper around MethodDeclaration
     • JmlClassAccessibleDeclaration
     • JmlClassExprDeclaration // invariant, initially, axiom, ...
   • JmlExpression

     • JmlLetExpr // (\let x = 2+2 in ...)

     • JmlQuantifiedExpr // (\op binders; exprs...)

     • JmlSetComprehensionExpr // new JMLObjectSet {Integer i | myIntSet.has(i) && i != null && 0 <= i.intValue() && i.intValue() <= 10 }

       After JMLref. Should be reworked as no calculation is possible.

       • We should go for quantified expr instead: (<type> <binder>; <pred>; <calc>).

     • JmlLabelExpr //\lbl, \lblneg, \lblpos

     • JmlBinaryInfixExpr

     • JmlMultiCompareExpr // a <= b <= c

     • JmlTypeExpr // \type()

   • JmlClause
     • JmlInfFlowClause // determines/seperates, ...
     • JmlMultiExprClause // decreases , , ...;
     • JmlConditionalClause // \if ;
     • JmlOldClause // OLD
     • JmlCallableClause // callable ... ;
     • JmlForallClause // FORALL
     • JmlLabledClause // breaks ()
     • JmlSimpleExprClause // ensures : ;
     • JmlSignalsClause //
     • JmlSignalsOnlyClause //
   • JmlContract