Example Docu

9260f35a · Sarah Grebing · 4e279984 · 9260f35a · 9260f35a · 9260f35a
Commit 9260f35a authored Jan 23, 2018 by Sarah Grebing
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/quicksort/QuickSort.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/quicksort/QuickSort.java
@@ -9,7 +9,7 @@ public class QuickSort extends JavaExample {

        setName("Quicksort example");

-        setHelpText(null);
+        setHelpText(getClass().getResource("help.html"));

        setJavaFile(getClass().


--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/simple/JavaSimpleExample.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/simple/JavaSimpleExample.java
@@ -6,7 +6,7 @@ public class JavaSimpleExample extends JavaExample {

    public JavaSimpleExample() {
        setName("Simple Java Example");
-        setJavaFile(this.getClass().getResource("Test.java"));
+        setJavaFile(this.getClass().getResource("Simple.java"));
        defaultInit(getClass());
    }
 }
--- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/Test.java
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/Test.java
-public class Test{
+public class Simple{



@@ -6,7 +6,7 @@ public class Test{
      @ requires x >= 0;
      @ ensures \result >0;
      @*/
-    public int foo(int x){
+    public int very_simple(int x){
        if(x > 0){
            x--;
        }else{

--- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/help.html
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/help.html
@@ -3,7 +3,10 @@
 <head>
    <meta charset="UTF-8">
    <title>Java Simple Test Example</title>
-    This is a simple Java example.
+    <h1>Very Simple Java Example</h1>
+    This is a very simple Java example.
+
+    Please select the contract <em>Simple:very_simple</em> from the contract list.
 </head>
 <body>


--- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps
 script t1(){
    symbex;
    foreach{
-       onestep;
-       andRight;
-       foreach{
-            tryclose;
-            }
+      tryclose;
    }
-//    cases{
-//       case match `?X >= 0,?X > 0  ==>`:
-//           cut `?X = 0`[?X \ X];
-//           foreach{
-//             auto;
-//           }
-//    }
 }
--- a/website/docs/index.md
+++ b/website/docs/index.md
@@ -89,7 +89,7 @@ Java method `split` has to be selected. After loading the problem the program to
 shown in an own view on the right side, the script is shown on the left side and in the middle the proof obligation and the list of open goals is shown. 
 Views can be selected and docked to other places on the screen.

-Please note that after a succesful loadthe statusbar indicates that the contract was loaded.
+Please note that after a succesful load the statusbar indicates that the contract was loaded.

 ### Setting a breakpoint and starting the Interpreter

@@ -136,7 +136,7 @@ Your browser does not support the video tag or WebM.
 </video>
 </center>

-In this video we demonstrate the interactive point and click rule applications after selecting the interactive button.We further demonstrate how the interaction is included to the original script.
+In this video we demonstrate the interactive point and click rule applications after selecting the interactive button. We further demonstrate how the interaction is included to the original script.

 <center>
 <video width="80%"  controls>