diff --git a/JmlMetaModel.plantuml b/JmlMetaModel.plantuml deleted file mode 100644 index 490440578b..0000000000 --- a/JmlMetaModel.plantuml +++ /dev/null @@ -1,254 +0,0 @@ -@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 -} - -/'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 - expression : Java.Expression - jmlTags: List -} - -class JmlQuantifiedExpr extends Java.Expression { - /'private JmlBinder binder;'/ - variables : List - expressions : List -} -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 - WHEN - WHEN_REDUNDANTLY - NONE - -} - -class JmlClauseIf extends JmlClause { - then : Java.Expression - cond : Java.Expression -} -class JmlMultiExprClause extends JmlClause { - heaps : NodeList -} -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 { - pre : Java.Expression - methodCalls : List -} -class JmlForallClause extends JmlClause { - boundedVariables : NodeList -} -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 -} -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 \ No newline at end of file diff --git a/doc/docs/component_diagram.puml b/doc/docs/component_diagram.puml deleted file mode 100644 index 2a219aa581..0000000000 --- a/doc/docs/component_diagram.puml +++ /dev/null @@ -1,29 +0,0 @@ -@startuml -node core { - [Java parser] <-- [AST] - [Javadoc parser] - [AST] <-- [lexical preserving printer] - [AST] <-- [concrete syntax model] - [concrete syntax model] <-- [lexical preserving printer] - events <-- [lexical preserving printer] - [AST] <-- [comments inserter] - [AST] <-- [visitors] - [AST] <-- [meta model] - [AST] <-- [pretty printer] - [visitors] <-- [pretty printer] - [AST] - symbol_resolution - [AST] - events - [visitors] <-- [code generators] - [AST] <-- [code generators] - [meta model] <-- [code generators] - [AST] <-- [JSON (de)serializer] - [Java parser] <- [source root] -} -node symbol-solver { - [AST] <- [model] - symbol_resolution <- [model] - [model] <-- [core] - [model] <-- [logic] - [logic] <-- [core] -} -@enduml \ No newline at end of file diff --git a/doc/docs/devel.md b/doc/docs/devel.md deleted file mode 100644 index 2d918bd9f1..0000000000 --- a/doc/docs/devel.md +++ /dev/null @@ -1,27 +0,0 @@ -# Development of JML Parser - -## How To Compile Sources - -If you checked out the project from GitHub you can build the project with maven using: - -``` -mvn clean install -``` - -If you checkout the sources and want to view the project in an IDE, it is best to first generate some of the source -files; otherwise you will get many compilation complaints in the IDE. (mvn clean install already does this for you.) - -``` -mvn javacc:javacc -``` - -## Extending the AST - -If you modify the code of the AST nodes, specifically if you add or remove fields or node classes, -the code generators will update a lot of code for you. -The `run_metamodel_generator.sh` script will rebuild the metamodel, -which is used by the code generators which are run by `run_core_generators.sh` -Make sure that `javaparser-core` at least compiles before you run these. - -**Note**: for Eclipse IDE follow the steps described in the -wiki: https://github.com/javaparser/javaparser/wiki/Eclipse-Project-Setup-Guide diff --git a/doc/docs/index.md b/doc/docs/index.md deleted file mode 100644 index a826982c8c..0000000000 --- a/doc/docs/index.md +++ /dev/null @@ -1,395 +0,0 @@ -# JML Parser - -This project provides a library for the parsing of Java with -the Java Modelling Language (JML). JML is a formal specification -for Java to decribe the functional behavior, e.g., -pre- and post-conditions of methods, class and loop invariants. - -The bases of this project is the [Java Parser]https://github.com/javaparser/javaparser) -project, which is extended in the following ways: - -* new lexer and grammar rules -* new AST classes and also new attributes for `Block`, `WhileStatement`, - `ForStatement`, `DoStatement`, and `CallableDeclaration` (constructors and methods). -* (TODO) extension of the name resolution - -## JML AST Classes - -* Behavior -* Jmlish - * JmlLogicType - * JmlStatement - * JmlStmtWithExpression - * JmlUnreachableStmt - * JmlGhostStatements - * JmlSetStmt - * JmlRefiningStmt - * JmlName - * JmlClassLevel - * JmlRepresentsDeclaration - * JmlFieldDeclaration - * JmlClassAccessibleDeclaration - * ClassInvariantClause - * LocationSetExpression - * LocationSetPrimary - * LocationSetLiftExpression - * LocationSetArrayAccess - * LocationSetBindingExpr - * LocationSetFunction - * LocationSetFieldAccess - * JmlClause - * JmlClauseE - * CapturesClause - * SignalsClause - * OldClause - * JmlClauseHL - * DurationClause - * SignalsOnlyClause - * JmlClauseHE - * CallableClause - * JmlClauseLE - * ForallClause - * JmlContract - * JmlContainer - * JmlBodyDeclaration - * JmlContracts - * JmlSetComprehension - * JmlStatements - -```plantuml -@startuml -class com.github.javaparser.ast.jml.clauses.AccessibleClause { -- NodeList heaps -- NodeList exprs -- Expression measuredBy -} -class com.github.javaparser.ast.jml.DefaultJmlContainer { -} -class com.github.javaparser.ast.jml.locref.LocationSetConstructorExpression { -- NodeList arguments -} -class com.github.javaparser.ast.jml.clauses.JmlContracts { -- boolean singleLine -- NodeList jmlTags -- NodeList elements -} -class com.github.javaparser.ast.jml.clauses.WorkingSpaceClause { -} -abstract class com.github.javaparser.ast.jml.body.JmlClassLevel { -} -class com.github.javaparser.ast.jml.clauses.JmlClauseLE { -- SimpleName label -- Expression expr -} -abstract class com.github.javaparser.ast.jml.clauses.JmlClause { -- JmlClauseKind kind -} -class com.github.javaparser.ast.jml.clauses.LoopInvariantClause { -- Expression expr -} -class com.github.javaparser.ast.jml.clauses.EnsuresClause { -- NodeList heaps -- Expression expr -} -class com.github.javaparser.ast.jml.expr.JmlSetComprehension { -- VariableDeclarator binding -- Expression predicate -} -class com.github.javaparser.ast.jml.clauses.SignalsOnlyClause { -- NodeList types -} -class com.github.javaparser.ast.jml.clauses.CallableClause { -} -class com.github.javaparser.ast.jml.stmt.JmlStatements { -- boolean singleLine -- NodeList jmlTags -- NodeList elements -} -class com.github.javaparser.ast.jml.clauses.CapturesClause { -} -class com.github.javaparser.ast.jml.locref.LocationSetPrimary { -- Kind kind -} -class com.github.javaparser.ast.jml.stmt.JmlSetStmt { -- Expression rhs -- Expression lhs -} -class com.github.javaparser.ast.jml.clauses.DivergesClause { -} -class com.github.javaparser.ast.jml.clauses.JmlClauseHE { -- NodeList heaps -- Expression expression -} -class com.github.javaparser.ast.jml.clauses.JmlContract { -- Behavior behavior -- NodeList modifiers -- NodeList clauses -- NodeList subContracts -} -class com.github.javaparser.ast.jml.clauses.LoopVariantClause { -} -class com.github.javaparser.ast.jml.body.JmlRepresentsDeclaration { -- NodeList modifiers -- SimpleName id -- Expression expr -} -class com.github.javaparser.ast.jml.locref.LocationSetFieldAccess { -- LocationSetExpression scope -- SimpleName name -} -class com.github.javaparser.ast.jml.locref.LocationSetBindingExpr { -- Quantifier quantifier -- VariableDeclarationExpr boundedVars -- Expression predicate -- LocationSetExpression expr -} -class com.github.javaparser.ast.jml.clauses.ForallClause { -- NodeList variables -} -interface com.github.javaparser.ast.jml.JmlContainer { -} -class com.github.javaparser.ast.jml.stmt.JmlUnreachableStmt { -} -class com.github.javaparser.ast.jml.clauses.ReturnsClause { -- Expression expr -} -class com.github.javaparser.ast.jml.expr.JmlLetExpr { -- NodeList variables -- Expression body -} -class com.github.javaparser.ast.jml.expr.JmlMultiCompareExpr { -} -class com.github.javaparser.ast.jml.clauses.LoopDecreasesClause { -} -class com.github.javaparser.ast.jml.clauses.WhenClause { -- Expression expr -} -class com.github.javaparser.ast.jml.clauses.DurationClause { -} -class com.github.javaparser.ast.jml.clauses.JmlClauseE { -- Expression expr -} -class com.github.javaparser.ast.jml.clauses.ContinuesClause { -- SimpleName label -- Expression expr -} -interface com.github.javaparser.ast.jml.JmlKeyword { -} -class com.github.javaparser.ast.jml.clauses.ModifiesClause { -- NodeList heaps -- NodeList exprs -} -class com.github.javaparser.ast.jml.locref.LocationSetFunction { -- Function function -- NodeList arguments -} -class com.github.javaparser.ast.jml.body.JmlBodyDeclaration { -- boolean singleLine -- NodeList jmlTags -- NodeList elements -} -class com.github.javaparser.ast.jml.locref.LocationSetArrayAccess { -- {static} Expression ALL_INDICES -- LocationSetExpression name -- Expression index -} -class com.github.javaparser.ast.jml.stmt.JmlGhostStatements { -- NodeList statements -} -class com.github.javaparser.ast.jml.expr.JmlLabel { -- Kind kind -- SimpleName label -- Expression expression -} -interface com.github.javaparser.ast.jml.clauses.LoopContractable { -} -class com.github.javaparser.ast.jml.body.JmlFieldDeclaration { -- FieldDeclaration decl -} -class com.github.javaparser.ast.jml.clauses.SignalsClause { -- Type type -- SimpleName name -- Expression expr -} -class com.github.javaparser.ast.jml.expr.JmlQuantifiedExpr { -- JmlBinder binder -- NodeList variables -- NodeList expressions -} -class com.github.javaparser.ast.jml.stmt.JmlStmtWithExpression { -- JmlStmtKind kind -- Expression expression -} -class com.github.javaparser.ast.jml.expr.JmlFunction { -- JmlName functionName -- NodeList arguments -} -class com.github.javaparser.ast.jml.body.JmlClassAccessibleDeclaration { -- NodeList modifiers -- SimpleName label -- NodeList expressions -- Expression measuredBy -} -interface com.github.javaparser.ast.jml.clauses.MethodContractable { -} -class com.github.javaparser.ast.jml.type.JmlLogicType { -- Primitive type -} -class com.github.javaparser.ast.jml.clauses.OldClause { -- NodeList variables -} -class com.github.javaparser.ast.jml.body.JmlSpecification { -- boolean singleLine -- Set jmlTags -- NodeList elements -} -abstract class com.github.javaparser.ast.jml.stmt.JmlStatement { -} -class com.github.javaparser.ast.jml.stmt.JmlRefiningStmt { -} -class com.github.javaparser.ast.jml.clauses.JmlClauseHL { -- NodeList heaps -- NodeList exprs -} -interface com.github.javaparser.ast.jml.clauses.BlockContractable { -} -class com.github.javaparser.ast.jml.expr.JmlName { -- String identifier -- JmlName qualifier -} -abstract class com.github.javaparser.ast.jml.locref.LocationSetExpression { -} - - -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.AccessibleClause -com.github.javaparser.ast.jml.clauses.BlockContractable <|.. com.github.javaparser.ast.jml.clauses.AccessibleClause -com.github.javaparser.ast.jml.clauses.LoopContractable <|.. com.github.javaparser.ast.jml.clauses.AccessibleClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.AccessibleClause -com.github.javaparser.ast.jml.JmlContainer <|.. com.github.javaparser.ast.jml.DefaultJmlContainer -com.github.javaparser.ast.jml.locref.LocationSetExpression <|-- com.github.javaparser.ast.jml.locref.LocationSetConstructorExpression -com.github.javaparser.ast.jml.clauses.Jmlish <|.. com.github.javaparser.ast.jml.clauses.JmlContracts -com.github.javaparser.ast.jml.JmlContainer <|.. com.github.javaparser.ast.jml.clauses.JmlContracts -com.github.javaparser.ast.jml.clauses.Node <|-- com.github.javaparser.ast.jml.clauses.JmlContracts -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.WorkingSpaceClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.WorkingSpaceClause -com.github.javaparser.ast.Jmlish <|.. com.github.javaparser.ast.jml.body.JmlClassLevel -com.github.javaparser.ast.Node <|-- com.github.javaparser.ast.jml.body.JmlClassLevel -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.JmlClauseLE -com.github.javaparser.ast.Jmlish <|.. com.github.javaparser.ast.jml.clauses.JmlClause -com.github.javaparser.ast.Node <|-- com.github.javaparser.ast.jml.clauses.JmlClause -com.github.javaparser.ast.jml.clauses.LoopContractable <|.. com.github.javaparser.ast.jml.clauses.LoopInvariantClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.LoopInvariantClause -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.EnsuresClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.EnsuresClause -com.github.javaparser.ast.Jmlish <|.. com.github.javaparser.ast.jml.expr.JmlSetComprehension -com.github.javaparser.ast.expr.Expression <|-- com.github.javaparser.ast.jml.expr.JmlSetComprehension -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.SignalsOnlyClause -com.github.javaparser.ast.jml.clauses.BlockContractable <|.. com.github.javaparser.ast.jml.clauses.SignalsOnlyClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.SignalsOnlyClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.CallableClause -com.github.javaparser.ast.jml.stmt.Jmlish <|.. com.github.javaparser.ast.jml.stmt.JmlStatements -com.github.javaparser.ast.jml.JmlContainer <|.. com.github.javaparser.ast.jml.stmt.JmlStatements -com.github.javaparser.ast.stmt.Statement <|-- com.github.javaparser.ast.jml.stmt.JmlStatements -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.CapturesClause -com.github.javaparser.ast.jml.locref.LocationSetExpression <|-- com.github.javaparser.ast.jml.locref.LocationSetPrimary -com.github.javaparser.ast.jml.stmt.JmlStatement <|-- com.github.javaparser.ast.jml.stmt.JmlSetStmt -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.DivergesClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.DivergesClause -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.JmlClauseHE -com.github.javaparser.ast.jml.clauses.BlockContractable <|.. com.github.javaparser.ast.jml.clauses.JmlClauseHE -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.JmlClauseHE -com.github.javaparser.ast.jml.clauses.Jmlish <|.. com.github.javaparser.ast.jml.clauses.JmlContract -com.github.javaparser.ast.jml.clauses.Node <|-- com.github.javaparser.ast.jml.clauses.JmlContract -com.github.javaparser.ast.jml.clauses.LoopContractable <|.. com.github.javaparser.ast.jml.clauses.LoopVariantClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.LoopVariantClause -com.github.javaparser.ast.nodeTypes.NodeWithModifiers <|.. com.github.javaparser.ast.jml.body.JmlRepresentsDeclaration -com.github.javaparser.ast.jml.body.JmlClassLevel <|-- com.github.javaparser.ast.jml.body.JmlRepresentsDeclaration -com.github.javaparser.ast.jml.locref.LocationSetExpression <|-- com.github.javaparser.ast.jml.locref.LocationSetFieldAccess -com.github.javaparser.ast.jml.locref.LocationSetExpression <|-- com.github.javaparser.ast.jml.locref.LocationSetBindingExpr -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.ForallClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.ForallClause -com.github.javaparser.ast.jml.stmt.JmlStatement <|-- com.github.javaparser.ast.jml.stmt.JmlUnreachableStmt -com.github.javaparser.ast.jml.clauses.BlockContractable <|.. com.github.javaparser.ast.jml.clauses.ReturnsClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.ReturnsClause -com.github.javaparser.ast.expr.Expression <|-- com.github.javaparser.ast.jml.expr.JmlLetExpr -com.github.javaparser.ast.expr.Expression <|-- com.github.javaparser.ast.jml.expr.JmlMultiCompareExpr -com.github.javaparser.ast.jml.clauses.LoopContractable <|.. com.github.javaparser.ast.jml.clauses.LoopDecreasesClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.LoopDecreasesClause -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.WhenClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.WhenClause -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.DurationClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.DurationClause -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.JmlClauseE -com.github.javaparser.ast.jml.clauses.LoopContractable <|.. com.github.javaparser.ast.jml.clauses.JmlClauseE -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.JmlClauseE -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.ContinuesClause -com.github.javaparser.ast.jml.clauses.LoopContractable <|.. com.github.javaparser.ast.jml.clauses.ModifiesClause -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.ModifiesClause -com.github.javaparser.ast.jml.clauses.BlockContractable <|.. com.github.javaparser.ast.jml.clauses.ModifiesClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.ModifiesClause -com.github.javaparser.ast.jml.locref.LocationSetExpression <|-- com.github.javaparser.ast.jml.locref.LocationSetFunction -com.github.javaparser.ast.jml.JmlContainer <|.. com.github.javaparser.ast.jml.body.JmlBodyDeclaration -com.github.javaparser.ast.body.BodyDeclaration <|-- com.github.javaparser.ast.jml.body.JmlBodyDeclaration -com.github.javaparser.ast.jml.locref.LocationSetExpression <|-- com.github.javaparser.ast.jml.locref.LocationSetArrayAccess -com.github.javaparser.ast.jml.stmt.JmlStatement <|-- com.github.javaparser.ast.jml.stmt.JmlGhostStatements -com.github.javaparser.ast.expr.Expression <|-- com.github.javaparser.ast.jml.expr.JmlLabel -com.github.javaparser.ast.jml.body.JmlClassLevel <|-- com.github.javaparser.ast.jml.body.JmlFieldDeclaration -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.SignalsClause -com.github.javaparser.ast.jml.clauses.BlockContractable <|.. com.github.javaparser.ast.jml.clauses.SignalsClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.SignalsClause -com.github.javaparser.ast.expr.Expression <|-- com.github.javaparser.ast.jml.expr.JmlQuantifiedExpr -com.github.javaparser.ast.jml.stmt.JmlStatement <|-- com.github.javaparser.ast.jml.stmt.JmlStmtWithExpression -com.github.javaparser.ast.Jmlish <|.. com.github.javaparser.ast.jml.expr.JmlFunction -com.github.javaparser.ast.expr.Expression <|-- com.github.javaparser.ast.jml.expr.JmlFunction -com.github.javaparser.ast.nodeTypes.NodeWithModifiers <|.. com.github.javaparser.ast.jml.body.JmlClassAccessibleDeclaration -com.github.javaparser.ast.jml.body.JmlClassLevel <|-- com.github.javaparser.ast.jml.body.JmlClassAccessibleDeclaration -com.github.javaparser.ast.Jmlish <|.. com.github.javaparser.ast.jml.type.JmlLogicType -com.github.javaparser.ast.type.Type <|-- com.github.javaparser.ast.jml.type.JmlLogicType -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.OldClause -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.OldClause -com.github.javaparser.ast.Jmlish <|.. com.github.javaparser.ast.jml.stmt.JmlStatement -com.github.javaparser.ast.stmt.Statement <|-- com.github.javaparser.ast.jml.stmt.JmlStatement -com.github.javaparser.ast.jml.stmt.JmlStatement <|-- com.github.javaparser.ast.jml.stmt.JmlRefiningStmt -com.github.javaparser.ast.jml.clauses.MethodContractable <|.. com.github.javaparser.ast.jml.clauses.JmlClauseHL -com.github.javaparser.ast.jml.clauses.BlockContractable <|.. com.github.javaparser.ast.jml.clauses.JmlClauseHL -com.github.javaparser.ast.jml.clauses.LoopContractable <|.. com.github.javaparser.ast.jml.clauses.JmlClauseHL -com.github.javaparser.ast.jml.clauses.JmlClause <|-- com.github.javaparser.ast.jml.clauses.JmlClauseHL -com.github.javaparser.ast.nodeTypes.NodeWithIdentifier <|.. com.github.javaparser.ast.jml.expr.JmlName -com.github.javaparser.ast.Jmlish <|.. com.github.javaparser.ast.jml.expr.JmlName -com.github.javaparser.ast.Node <|-- com.github.javaparser.ast.jml.expr.JmlName -com.github.javaparser.ast.Jmlish <|.. com.github.javaparser.ast.jml.locref.LocationSetExpression -com.github.javaparser.ast.Node <|-- com.github.javaparser.ast.jml.locref.LocationSetExpression -@enduml -``` - -```plantuml -@startuml -node core { - [Java parser] <-- [AST] - [Javadoc parser] - [AST] <-- [lexical preserving printer] - [AST] <-- [concrete syntax model] - [concrete syntax model] <-- [lexical preserving printer] - events <-- [lexical preserving printer] - [AST] <-- [comments inserter] - [AST] <-- [visitors] - [AST] <-- [meta model] - [AST] <-- [pretty printer] - [visitors] <-- [pretty printer] - [AST] - symbol_resolution - [AST] - events - [visitors] <-- [code generators] - [AST] <-- [code generators] - [meta model] <-- [code generators] - [AST] <-- [JSON (de)serializer] - [Java parser] <- [source root] -} -node symbol-solver { - [AST] <- [model] - symbol_resolution <- [model] - [model] <-- [core] - [model] <-- [logic] - [logic] <-- [core] -} -@enduml -``` \ No newline at end of file diff --git a/doc/docs/readme.md b/doc/docs/readme.md deleted file mode 100644 index a5d31628b4..0000000000 --- a/doc/docs/readme.md +++ /dev/null @@ -1,145 +0,0 @@ - - -# JavaParser - -[![Maven Central](https://img.shields.io/maven-central/v/com.github.javaparser/javaparser-core.svg)](http://search.maven.org/#search%7Cgav%7C1%7Cg%3A%22com.github.javaparser%22%20AND%20a%3A%22javaparser-core%22) -[![Build Status](https://travis-ci.org/javaparser/javaparser.svg?branch=master)](https://travis-ci.org/javaparser/javaparser) -[![Coverage Status](https://codecov.io/gh/javaparser/javaparser/branch/master/graphs/badge.svg?branch=master)](https://app.codecov.io/gh/javaparser/javaparser?branch=master) -[![Join the chat at https://gitter.im/javaparser/javaparser](https://badges.gitter.im/Join%20Chat.svg)](https://gitter.im/javaparser/javaparser?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge) -[![License LGPL-3/Apache-2.0](https://img.shields.io/badge/license-LGPL--3%2FApache--2.0-blue.svg)](LICENSE) -[![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.2667378.svg)](https://doi.org/10.5281/zenodo.2667378) - -This project contains a set of libraries implementing a Java 1.0 - Java 15 Parser with advanced analysis -functionalities. This includes preview features to Java 13, with Java 14 preview features work-in-progress. - -Our main site is at [JavaParser.org](http://javaparser.org) - -## Setup - -The project binaries are available in Maven Central. - -We strongly advise users to adopt Maven, Gradle or another build system for their projects. -If you are not familiar with them we suggest taking a look at the maven quickstart projects -([javaparser-maven-sample](https://github.com/javaparser/javaparser-maven-sample), -[javasymbolsolver-maven-sample](https://github.com/javaparser/javasymbolsolver-maven-sample)). - -Just add the following to your maven configuration or tailor to your own dependency management system. - -[Please refer to the Migration Guide when upgrading from 2.5.1 to 3.0.0+](https://github.com/javaparser/javaparser/wiki/Migration-Guide) - -**Maven**: - -```xml - - - com.github.javaparser - javaparser-symbol-solver-core - ${project.version} - -``` - -**Gradle**: - -``` -implementation 'com.github.javaparser:javaparser-symbol-solver-core:${project.version}' -``` - -Since Version 3.5.10, the JavaParser project includes the JavaSymbolSolver. -While JavaParser generates an Abstract Syntax Tree, JavaSymbolSolver analyzes that AST and is able to find -the relation between an element and its declaration (e.g. for a variable name it could be a parameter of a method, -providing information about its type, position in the AST, ect). - -Using the dependency above will add both JavaParser and JavaSymbolSolver to your project. If you only need the core -functionality of parsing Java source code in order to traverse and manipulate the generated AST, you can reduce your -projects boilerplate by only including JavaParser to your project: - -**Maven**: - -```xml - - - com.github.javaparser - javaparser-core - ${project.version} - -``` - -**Gradle**: - -``` -implementation 'com.github.javaparser:javaparser-core:${project.version}' -``` - -Since version 3.6.17 the AST can be serialized to JSON. -There is a separate module for this: - -**Maven**: - -```xml - - - com.github.javaparser - javaparser-core-serialization - ${project.version} - -``` - -**Gradle**: - -``` -implementation 'com.github.javaparser:javaparser-core-serialization:${project.version}' -``` - -## How To Compile Sources - -If you checked out the project's source code from GitHub, you can build the project with maven using: - -``` -mvnw clean install -``` - -If you want to generate the packaged jar files from the source files, you run the following maven command: - -``` -mvnw package -``` - -**NOTE** the jar files for the two modules can be found in: - -- `javaparser/javaparser-core/target/javaparser-core-\.jar` -- `javaparser-symbol-solver-core/target/javaparser-symbol-solver-core-\.jar` - -If you checkout the sources and want to view the project in an IDE, it is best to first generate some of the source -files; -otherwise you will get many compilation complaints in the IDE. (`mvnw clean install` already does this for you.) - -``` -mvnw javacc:javacc -``` - -If you modify the code of the AST nodes, specifically if you add or remove fields or node classes, -the code generators will update a lot of code for you. -The `run_metamodel_generator.sh` script will rebuild the metamodel, -which is used by the code generators which are run by `run_core_generators.sh` -Make sure that `javaparser-core` at least compiles before you run these. - -**Note**: for Eclipse IDE follow the steps described in the -wiki: https://github.com/javaparser/javaparser/wiki/Eclipse-Project-Setup-Guide - -## More information - -#### [JavaParser.org](https://javaparser.org) is the main information site. - -## License - -JavaParser is available either under the terms of the LGPL License or the Apache License. You as the user are entitled -to choose the terms under which adopt JavaParser. - -For details about the LGPL License please refer -to [LICENSE.LGPL](ttps://github.com/javaparser/javaparser/blob/master/LICENSE.LGPL). - -For details about the Apache License please refer -to [LICENSE.APACHE](ttps://github.com/javaparser/javaparser/blob/master/LICENSE.APACHE). diff --git a/doc/jmlmm.plantuml b/doc/jmlmm.plantuml deleted file mode 100644 index a5134caa44..0000000000 --- a/doc/jmlmm.plantuml +++ /dev/null @@ -1,52 +0,0 @@ -@startuml -class java.Class { -} - -class java.Method {} - -class jml.Expression {} -class jml.Formula {} -class jml.Method { - + visibility : VisibilityModifier - + kind : {GHOST, MODEL} - + name : String} - + params : List - + body : jml.BlockStmt -} - -class jml.Field { - + visibility : VisibilityModifier - + kind : {GHOST, MODEL} - + name : String - + params : List -} - - -class jml.Class { - +\inv : Formula - +\initially : Formula -} - -class jml.Contract { - + name : String - + assignable : Expression -} - -jml.Contract -- "1..*" jml.FClause : +requires -jml.Contract -- "1..*" jml.FClause : +ensures -jml.Contract -- "1..*" jml.EClause : +diverges -jml.Contract -- "1..*" jml.EClause : +assignable - -class jml.FClause {} -class jml.EClause {} - -jml.EClause o-- "1..*" jml.Expression - -java.Class --> "0..*" jml.Field -jml.FClause --> jml.Formula : +/all -jml.FClause o-- "1..*" jml.Formula -java.Class --> jml.Class -java.Class --> "0..*" jml.Method -java.Method --> "0..*" jml.Contract -jml.Field --> "0..1" jml.Expression : "representsBy" -@enduml \ No newline at end of file diff --git a/doc/mkdocs.yml b/doc/mkdocs.yml deleted file mode 100644 index 1b745c435b..0000000000 --- a/doc/mkdocs.yml +++ /dev/null @@ -1,37 +0,0 @@ -site_name: JML Parser -plugins: - - search -markdown_extensions: - - admonition - - codehilite: - guess_lang: false - - footnotes - - meta - - pymdownx.arithmatex - - pymdownx.betterem: - smart_enable: all - - pymdownx.caret - - pymdownx.critic - - pymdownx.details - - pymdownx.emoji: - emoji_generator: !!python/name:pymdownx.emoji.to_svg - - pymdownx.inlinehilite - - pymdownx.magiclink - - pymdownx.mark - - pymdownx.smartsymbols - - pymdownx.superfences - - pymdownx.tasklist: - custom_checkbox: true - - pymdownx.tilde - - attr_list - - plantuml_markdown - - toc: - permalink: true - - markdown_aafigure: - format: svg - - markdown_blockdiag: - format: svg -extra_javascript: - - 'https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.0/MathJax.js?config=TeX-MML-AM_CHTML' -# - "js/javajml.js" -