Testcase for bug in termmatcher

matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java

@@ -196,7 +196,7 @@ public class MatcherFacadeTest {
                 "fint2(1,2), fint2(2,3), !p ==> pred(a), p",
                 "fint2(1, ?X), fint2(?X, ?Y) ==> p",
                 "[{EMPTY_MATCH=null, ?X=Z(2(#)), ?Y=Z(3(#))}]");
-
+        shouldMatchSeq("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{?X= h2(2,3)}]");
     }
 
     private void shouldMatchSeq(String seq, String seqPattern, String exp) throws ParserException {

matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/test.key

@@ -22,7 +22,7 @@
    S f(S);
    S g(S);
    S h(S, S);
-
+   int h2(int, int);
    int fint(int);
 
 }

rt-key/pom.xml

@@ -24,5 +24,10 @@
 			<artifactId>keydeps</artifactId>
 			<version>1.0</version>
 		</dependency>
+        <dependency>
+            <groupId>edu.kit.iti.formal.psdbg</groupId>
+            <artifactId>matcher</artifactId>
+            <version>0.1-SNAPSHOT</version>
+        </dependency>
 	</dependencies>
 </project>

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/Example.java

@@ -46,6 +46,7 @@ public abstract class Example {
                 String content = IOUtils.toString(helpText, Charset.defaultCharset());
                 debuggerMain.openNewHelpDock(getName() + " Example", content);
             }
+            debuggerMain.getWelcomePaneDock().close();
         } catch (IOException e) {
             e.printStackTrace();
         }

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/JavaExample.java

@@ -27,14 +27,17 @@ public class JavaExample extends Example {
         //     Loading via key file, or using an automatic contract selector?
 
         try {
+
             File script = newTempFile(scriptFile, getName() + ".kps");
             debuggerMain.openScript(script);
-
+            debuggerMain.getWelcomePaneDock().close();
             //File key = newTempFile(keyFile, "project.key");
             File java = newTempFile(javaFile, getName() + ".java");
             //System.out.println(java.getAbsolutePath());
             //debuggerMain.openKeyFile(key);
             debuggerMain.openJavaFile(java);
+
+            debuggerMain.showActiveInspector(null);
             if (helpText != null) {
                 String content = IOUtils.toString(helpText, Charset.defaultCharset());
                 debuggerMain.openNewHelpDock(getName() + " Example", content);

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/JavaSimpleExample.java → ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/simple/JavaSimpleExample.java

-package edu.kit.iti.formal.psdbg.examples.java;
+package edu.kit.iti.formal.psdbg.examples.java.simple;
 
 import edu.kit.iti.formal.psdbg.examples.JavaExample;
 
 public class JavaSimpleExample extends JavaExample {
 
     public JavaSimpleExample() {
-        setName("Test");
+        setName("Simple Java Example");
         setJavaFile(this.getClass().getResource("Test.java"));
 
 

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/transitive/PaperExample.java

+package edu.kit.iti.formal.psdbg.examples.java.transitive;
+
+import edu.kit.iti.formal.psdbg.examples.JavaExample;
+
+public class PaperExample extends JavaExample {
+    public PaperExample() {
+        setName("Transitive Permutation");
+        setJavaFile(this.getClass().getResource("Simple.java"));
+
+
+        defaultInit(getClass());
+
+        System.out.println(this);
+    }
+
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java

@@ -39,7 +39,7 @@ public class WelcomePane extends AnchorPane {
         proofScriptDebugger.getWelcomePaneDock().close();
         proofScriptDebugger.showActiveInspector(null);
         Examples.loadExamples().forEach(example -> {
-            if (example.getName().equals("Test"))
+            if (example.getName().equals("Transitive Permutation"))
                 example.open(proofScriptDebugger);
 
         });

ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example

 edu.kit.iti.formal.psdbg.examples.contraposition.ContrapositionExample
 edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample
-edu.kit.iti.formal.psdbg.examples.java.JavaSimpleExample
\ No newline at end of file
+edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample
+edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample
\ No newline at end of file

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/script.kps → ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps

+script t(){
+    symbex;
+    cases{
+       case match `?X = 0 ==>`:
+            eqSymm on=`?X=0`[?X/?X];
+
+    }
+
+}
+
 script t1(){
     symbex;
     cases{

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/transitive/Simple.java

+ public final class Simple {
+ 
+ 
+    boolean b1;
+    boolean b2;
+    
+    /*@ public normal_behavior
+      @ ensures \dl_seqPerm(\dl_array2seq(\result), \old(\dl_array2seq(aarr)));
+      @ assignable \everything;
+     */
+    public int[] transitive(int[] aarr){
+        aarr = Simple.copyArray(aarr); 
+        sort(aarr); 
+        int[] barr = Simple.copyArray(aarr);
+        
+        if(b1){barr = Simple.copyArray(aarr);} 
+        if(b2){log(barr);}
+        return barr;
+    }
+
+    /*@ public normal_behavior
+      @ ensures \dl_seqPerm(\dl_array2seq(a), \old(\dl_array2seq(a)));
+      @ assignable a[*];
+      */
+    public void sort(int[] a){};
+
+    /*@ public normal_behavior
+      @ ensures (\forall int i; 0 <= i < input.length; input[i] == \result[i]) 
+      @ && \result.length == input.length;
+      @ ensures \fresh(\result);
+      @ ensures \dl_seqPerm(\dl_array2seq(\result), \dl_array2seq(input));
+      @ assignable \nothing;
+      */
+    public /*@helper@*/ static int[] copyArray(int[] input){}
+
+    /*@ public normal_behavior
+      @ assignable \strictly_nothing;
+      */
+    public void log(int[] a){};
+
+}

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/transitive/help.html

+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="UTF-8">
+    <title>Java Example: Transitive Permutation</title>
+    This is a simple Java example showing that the method transitive() preserves the permutation of teh input array.
+</head>
+<body>
+
+</body>
+</html>
\ No newline at end of file

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/transitive/script.kps

+ 
+script prove_transitive(){
+ symbex;  			
+ cases{
+   case match
+    `seqPerm(?Res0Copy, ?Arr),
+    seqPerm(?Res0Sort, ?Res0Copy), 
+    seqPerm(?Res1Copy0, ?Res0Sort), 
+    seqPerm(?Res2Copy1, ?Res0Sort) ==> 
+        seqPerm(?Res2Copy1, ?Arr)` using [ ?Res0Copy: Seq, ?Arr: Seq,?Res0Sort: Seq, ?Res1Copy0: Seq, ?Res2Copy1: Seq, ?Res0Sort: Seq  ]:
+   {SeqPermSym on=`seqPerm(?Res0Copy, ?Arr) ==>`;
+    SeqPermSym on=`seqPerm(?Res0Sort, ?Res0Copy) ==>`;
+    SeqPermSym on=`seqPerm(?Res1Copy0, ?Res0Sort)==>`;
+    SeqPermSym on=`seqPerm(?Res2Copy1, ?Res0Sort) ==>`;
+    SeqPermTrans on=`seqPerm(?Res0Copy, ?Arr) ==>`;
+    SeqPermTrans on=`seqPerm(?Arr, ?Res0Sort) ==>`
+                 with=`seqPerm(?Arr,?Res2Copy1)`;
+    SeqPermSym on=`seqPerm(?Arr,?Res2Copy1)`;
+    auto; 
+   }
+   case match
+    `seqPerm(?Res0Copy, ?Arr),
+    seqPerm(?Res0Sort, ?Res0Copy), 
+    seqPerm(?Res1Copy0, ?Res0Sort) ==> 
+             seqPerm(?Res1Copy0, ?Arr)`  using [ ?Res0Copy: Seq, ?Arr: Seq,?Res0Sort: Seq, ?Res1Copy0: Seq, ?Res0Sort: Seq ]:
+    {SeqPermSym on=`seqPerm(?Res0Copy, ?Arr)`;
+     SeqPermSym on=`seqPerm(?Res0Sort, ?Res0Copy)`;
+     SeqPermSym on=`seqPerm(?Res1Copy0, ?Res0Sort)`;
+     SeqPermTrans on=`seqPerm(?Res0Copy, ?Arr)`;
+     SeqPermTrans on=`seqPerm(?Arr, ?Res0Sort)`
+     SeqPermSym on=`==> seqPerm(?Res1Copy0, ?Arr)`;
+     auto;
+     }
+     default:{ 
+        auto;
+    }
+  } 
+}

website/index.html

@@ -34,30 +34,31 @@
 <div id="content">
 
 
-    <h1>Proof Script Debugger</h1>
-
-    <p>Lorem ipsum dolor sit amet, consetetur sadipscing elitr, sed diam nonumy eirmod tempor invidunt ut labore et
-        dolore magna aliquyam erat, sed diam voluptua. At vero eos et accusam et justo duo dolores et ea rebum. Stet
-        clita kasd gubergren, no sea takimata sanctus est Lorem ipsum dolor sit amet. Lorem ipsum dolor sit amet,
-        consetetur sadipscing elitr, sed diam nonumy eirmod tempor invidunt ut labore et dolore magna aliquyam erat, sed
-        diam voluptua. At vero eos et accusam et justo duo dolores et ea rebum. Stet clita kasd gubergren, no sea
-        takimata sanctus est Lorem ipsum dolor sit amet. Lorem ipsum dolor sit amet, consetetur sadipscing elitr, sed
-        diam nonumy eirmod tempor invidunt ut labore et dolore magna aliquyam erat, sed diam voluptua. At vero eos et
-        accusam et justo duo dolores et ea rebum. Stet clita kasd gubergren, no sea takimata sanctus est Lorem ipsum
-        dolor sit amet.
+    <h1>Proof Script Debugger for the KeY System</h1>
+
+    <p>The proof script debugger is a prototypical implementation
+        of an interaction concept for program verification systems that are rule based and
+        use a program logic.
+        The prototype is implemented on top of the interactive program verification system
+        <a href="http://www.key-project.org">KeY</a>. KeY is an interactive program verification
+        system for Java program annotated with the Java Modeling Language (JML).
     </p>
 
     <p>
-        Duis autem vel eum iriure dolor in hendrerit in vulputate velit esse molestie consequat, vel illum dolore eu
-        feugiat nulla facilisis at vero eros et accumsan et iusto odio dignissim qui blandit praesent luptatum zzril
-        delenit augue duis dolore te feugait nulla facilisi. Lorem ipsum dolor sit amet, consectetuer adipiscing elit,
-        sed diam nonummy nibh euismod tincidunt ut laoreet dolore magna aliquam erat volutpat.
+        The protypical implementation includes a proof scripting language that is tailored to the
+        problem domain of program verification.
+        The language particualrily allows to:
+    <ol>
+        <li></li>
+        <li></li>
+        <li></li>
+        <li></li>
+
+    </ol>
+    Together with the proof scripting language a debugging concept for failed proof attempts
+    is implemented that leverages well-known concepts from program debugging to
+    the analysis of failed proof attempts.
     </p>
-    <p> Ut wisi enim ad minim veniam, quis nostrud exerci tation ullamcorper suscipit lobortis nisl ut aliquip ex ea
-        commodo consequat. Duis autem vel eum iriure dolor in hendrerit in vulputate velit esse molestie consequat, vel
-        illum dolore eu feugiat nulla facilisis at vero eros et accumsan et iusto odio dignissim qui blandit praesent
-        luptatum zzril delenit augue duis dolore te feugait nulla facilisi. </p>
-
     <h2>Features</h2>
 
     <div class="column">
@@ -103,19 +104,20 @@
     </div>
     <div style="clear: both;"/>
 
-    <h2>Getting Started</h2>
 
+    <!--    <h2>Getting Started</h2>
 
-    <h2>Downloads</h2>
 
-    <ul>
-        <li>Version 1.0
-        <p>
-            <a href="#">psdb-0.9-alpha.jar</a>
-        </p>
-        </li>
-    </ul>
+        <h2>Downloads</h2>
 
+        <ul>
+            <li>Version 1.0
+            <p>
+                <a href="#">psdb-0.9-alpha.jar</a>
+            </p>
+            </li>
+        </ul>
+    -->
     <footer style="border-top: #ccc 1px solid">
         Contact: <a href="https://formal.iti.kit.edu/~grebing/">Sarah Grebing</a>
     </footer>