disable features for release

Author: wadoon

README.md

@@ -29,33 +29,24 @@ following requests:
 
 * Code Outline (`documentSymbols`)
 
+* Error reporting (``)
 
+* Code Actions
+  * [ ] Check well-definedness (requires z3)
+  * [ ] Normalise formula
+  * [ ] ...
 
-* Support for KeY files
+* Code Lenses
+  * [ ] Prove refinment of contracts
+  * [ ] 
 
-  Syntax highlighting and snippets.
-
-## Changelog
-
-* **0.3.0** (upcoming-2022)
-  - Changing to `SemanticTokenProvider` interface to highlight JML annotation texts inside Java files. 
-    There is no text mate grammar anymore. 
-    
-  - Language Server added on the basis of the [jmlparser
-    project](https://github.com/wadoon/jmlparser).
-  
-  - Simple support for KeY files
+* Snippets
 
-    Syntax highlighting and snippets.
+* Support for [KeY files](https://key-project.org/)
 
-* **0.2.0** (04.04.2019)
-  - Fixes by @csicar
-
-* **0.1.0** (14.02.2019)
-  - First release
+  Syntax highlighting and snippets.
 
-* **0.0.0** (unpublished)
-  - Start with the `java` language definition of VS Code.
+ 
 
 ## Authors
 

example_workspace/Errors.java

@@ -20,4 +20,19 @@ public void bar(int x) {
     public final int x;
     /*@ assignable x; */
     public void bear() {}
+
+
+    /*@
+    public normal_behavior 
+    ensures true;
+    {|
+        also 
+            requires a<0;
+        also
+            requires a>0;
+        also 
+            requires a==0; 
+    |}
+    */
+    public void bbbbb() {}
 }

examples/project.key

@@ -1,5 +1,19 @@
 \chooseContract
 
+\rules {
+    \lemma
+    eqTermCut {
+        \find(t)
+        \sameUpdateLevel
+        "Assume #t  = #s":
+            \add(t = s ==>);
+        "Assume #t != #s":
+            \add(t != s ==>)
+    };
+
+    
+}
+
 \problem {
     true -> \forall int x; x>2
 }

lsp/.idea/.name

@@ -1,7 +1,7 @@
 import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
 
 plugins {
-    kotlin("jvm") version "1.7.20"
+    kotlin("jvm") version "2.0.0-Beta3"
     id("com.github.johnrengelman.shadow") version "7.1.2"
     id("application")
 }
@@ -21,18 +21,21 @@ version = "1.0-SNAPSHOT"
 
 repositories {
     mavenCentral()
+    maven(url = "https://s01.oss.sonatype.org/content/repositories/snapshots/")
 }
 
 dependencies {
     testImplementation(kotlin("test"))
     implementation("org.tinylog:tinylog-api-kotlin:2.5.0")
     implementation("org.tinylog:tinylog-api:2.5.0-M2.1")
     implementation("org.tinylog:tinylog-impl:2.5.0")
-    implementation("org.eclipse.lsp4j:org.eclipse.lsp4j:0.15.0")
+    implementation("org.eclipse.lsp4j:org.eclipse.lsp4j:0.21.2")
     implementation("com.github.ajalt.clikt:clikt:3.5.0")
 
-    implementation("io.github.wadoon:jmlparser-symbol-solver-core:3.24.7-SNAPSHOT")
-    implementation("io.github.wadoon:jmlparser-jml-tools:3.24.7-SNAPSHOT")
+    implementation("io.github.jmltoolkit:jmlparser-symbol-solver-core:3.25.8-SNAPSHOT")
+    implementation("io.github.jmltoolkit:jmlparser-jml-tools:3.25.8-SNAPSHOT")
+
+    implementation("org.apache.groovy:groovy:4.0.6")
 
     testImplementation("com.google.truth:truth:1.1.3")
     testImplementation("org.junit.jupiter:junit-jupiter-api:5.9.0")
@@ -44,9 +47,9 @@ tasks.test {
 }
 
 tasks.withType<KotlinCompile> {
-    kotlinOptions.jvmTarget = "17"
+    kotlinOptions.jvmTarget = "21"
 }
 
 application {
-    mainClassName="jml.lsp.Main"
+    mainClass = "jml.lsp.Main"
 }

lsp/.idea/gradle.xml

@@ -1,17 +1,25 @@
 package jml.lsp
 
-import com.github.javaparser.ast.*
+import com.github.javaparser.ast.CompilationUnit
+import com.github.javaparser.ast.Node
+import com.github.javaparser.ast.NodeList
 import com.github.javaparser.ast.body.*
 import com.github.javaparser.ast.expr.VariableDeclarationExpr
 import com.github.javaparser.ast.jml.body.*
 import com.github.javaparser.ast.jml.clauses.*
 import com.github.javaparser.ast.modules.ModuleDeclaration
 import com.github.javaparser.ast.visitor.GenericVisitorAdapter
-import org.eclipse.lsp4j.*
+import org.eclipse.lsp4j.DocumentSymbol
+import org.eclipse.lsp4j.SymbolKind
 import java.util.*
 
+/**
+ * Runs through an AST and gathers symbols within JML annotations.
+ *
+ * @author Alexander Weigl
+ */
 class CatchSymbols : GenericVisitorAdapter<MutableList<DocumentSymbol>?, Unit?>() {
-    override fun visit(n: CompilationUnit, arg: Unit?): MutableList<DocumentSymbol>? {
+    override fun visit(n: CompilationUnit, arg: Unit?): MutableList<DocumentSymbol> {
         val children = acceptAll(n.types)
         return arrayListOf(
             DocumentSymbol(
@@ -33,7 +41,7 @@ class CatchSymbols : GenericVisitorAdapter<MutableList<DocumentSymbol>?, Unit?>(
         )
     }
 
-    override fun visit(n: AnnotationMemberDeclaration, arg: Unit?): MutableList<DocumentSymbol>? {
+    override fun visit(n: AnnotationMemberDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
         return arrayListOf(
             DocumentSymbol(
                 n.nameAsString,
@@ -95,7 +103,7 @@ class CatchSymbols : GenericVisitorAdapter<MutableList<DocumentSymbol>?, Unit?>(
         )
     }
 
-    override fun visit(n: FieldDeclaration, arg: Unit?): MutableList<DocumentSymbol>? {
+    override fun visit(n: FieldDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
         return n.variables.map {
             DocumentSymbol(
                 it.nameAsString,
@@ -105,7 +113,7 @@ class CatchSymbols : GenericVisitorAdapter<MutableList<DocumentSymbol>?, Unit?>(
         }.toMutableList()
     }
 
-    override fun visit(n: MethodDeclaration, arg: Unit?): MutableList<DocumentSymbol>? {
+    override fun visit(n: MethodDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
         val children = acceptAllo(n.contracts)
         return arrayListOf(
             DocumentSymbol(
@@ -124,7 +132,7 @@ class CatchSymbols : GenericVisitorAdapter<MutableList<DocumentSymbol>?, Unit?>(
         return super.visit(n, arg)
     }
 
-    override fun visit(n: ModuleDeclaration, arg: Unit?): MutableList<DocumentSymbol>? {
+    override fun visit(n: ModuleDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
         return arrayListOf(
             DocumentSymbol(
                 n.nameAsString,
@@ -134,7 +142,7 @@ class CatchSymbols : GenericVisitorAdapter<MutableList<DocumentSymbol>?, Unit?>(
         )
     }
 
-    override fun visit(n: JmlContract, arg: Unit?): MutableList<DocumentSymbol>? {
+    override fun visit(n: JmlContract, arg: Unit?): MutableList<DocumentSymbol> {
         val children = acceptAll(n.subContracts) + acceptAll(n.clauses)
         return arrayListOf(
             DocumentSymbol(
@@ -145,12 +153,12 @@ class CatchSymbols : GenericVisitorAdapter<MutableList<DocumentSymbol>?, Unit?>(
         )
     }
 
-    override fun visit(n: JmlRepresentsDeclaration?, arg: Unit?): MutableList<DocumentSymbol>? {
-        return arrayListOf();//return super.visit(n, arg)
+    override fun visit(n: JmlRepresentsDeclaration?, arg: Unit?): MutableList<DocumentSymbol> {
+        return arrayListOf()//return super.visit(n, arg)
     }
 
     override fun visit(n: JmlFieldDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
-        var decl = n.decl
+        val decl = n.decl
         return decl.variables.map { v ->
             DocumentSymbol(
                 v.nameAsString,
@@ -165,7 +173,7 @@ class CatchSymbols : GenericVisitorAdapter<MutableList<DocumentSymbol>?, Unit?>(
         return arrayListOf() //super.visit(n, arg)
     }
 
-    override fun visit(n: JmlClassExprDeclaration, arg: Unit?): MutableList<DocumentSymbol>? {
+    override fun visit(n: JmlClassExprDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
         return arrayListOf(
             DocumentSymbol(
                 n.name.map { it.asString() }.orElse("anon invariant"),

lsp/.idea/kotlinc.xml

@@ -2,18 +2,21 @@ package jml.lsp
 
 import com.github.javaparser.ast.Node
 import com.github.javaparser.ast.expr.Expression
+import com.github.javaparser.ast.jml.body.JmlClassExprDeclaration
 import com.github.javaparser.ast.jml.clauses.JmlSignalsClause
 import com.github.javaparser.ast.jml.clauses.JmlSimpleExprClause
 import com.github.javaparser.ast.jml.expr.JmlQuantifiedExpr
 import com.github.javaparser.ast.jml.expr.JmlQuantifiedExpr.JmlDefaultBinder
 import com.github.javaparser.ast.jml.stmt.JmlExpressionStmt
-import jml.lsp.actions.WellDefinednessCheck
 import org.eclipse.lsp4j.CodeAction
 import org.eclipse.lsp4j.CodeActionContext
 import org.eclipse.lsp4j.Command
 import org.eclipse.lsp4j.jsonrpc.messages.Either
 import kotlin.jvm.optionals.getOrNull
 
+/**
+ * This visitor gathers actions, that can be executed on nodes within the given range.
+ */
 class CodeActionCollector(val context: CodeActionContext?, private val range: com.github.javaparser.Range) :
     ResultingVisitor<MutableList<Either<Command, CodeAction>>>() {
     override val result = arrayListOf<Either<Command, CodeAction>>()
@@ -36,14 +39,21 @@ class CodeActionCollector(val context: CodeActionContext?, private val range: co
         super.visit(n, arg)
     }
 
+    override fun visit(n: JmlClassExprDeclaration, arg: Unit?) {
+        addWelldefinedCheck(n.invariant)
+        super.visit(n, arg)
+    }
+
     private fun addWelldefinedCheck(n: Expression): Boolean {
-        if (inRange(n))
-            return add(WellDefinednessCheck.createCommand(n))
+        /*if (inRange(n)) {
+            return add(WellDefinednessCheck.createCodeAction(n))
+        }*/
         return false
     }
 
-    @OptIn(ExperimentalStdlibApi::class)
-    private fun inRange(n: Node): Boolean = n.range.getOrNull()?.contains(range) ?: false
+    private fun inRange(n: Node): Boolean {
+        return n.range.getOrNull()?.contains(range) ?: false
+    }
 
     override fun visit(n: JmlQuantifiedExpr, arg: Unit?) {
         if (n.binder == JmlDefaultBinder.FORALL || n.binder == JmlDefaultBinder.EXISTS) {

lsp/.idea/misc.xml

@@ -5,12 +5,15 @@ import jml.lsp.actions.VerifyAgainstParent
 import org.eclipse.lsp4j.CodeLens
 import org.eclipse.lsp4j.Command
 
+/**
+ * Runs through the AST and collect code lens actions.
+ */
 class CodeLensCollector : ResultingVisitor<MutableList<out CodeLens>>() {
     override val result = arrayListOf<CodeLens>()
 
     override fun visit(n: JmlContract, arg: Unit?) {
         if (n.type == JmlContract.Type.METHOD) {
-            result.add(VerifyAgainstParent.createCodeLens(n))
+            //result.add(VerifyAgainstParent.createCodeLens(n))
         }
     }
 }