add more some examples

src/SimpleFormulaChecker.hs

@@ -222,4 +222,10 @@ blob = compareSpec (edslSrc, "blob1") (edslSrc, "blob1")
 nullTest1 = compareSpec (edslSrc, "null1") (edslSrc, "null2")
 nullTest2 = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec3")
 nullTest3 = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec4")
-nullTest4 = compareSpec (edslSrc, "null3") (edslSrc, "test2")
\ No newline at end of file
+nullTest4 = compareSpec (edslSrc, "null3") (edslSrc, "test2")
+sort1 = compareSpec (edslSrc, "sorted1") (edslSrc, "test2")
+sort2 = compareSpec (edslSrc, "sorted1") (edslSrc, "sorted2")
+sort3 = compareSpec (edslSrc, "sorted1") (edslSrc, "sorted3")
+sort4 = compareSpec (edslSrc, "test2") (edslSrc, "sorted3")
+sort5 = compareSpec (edslSrc, "sorted3") (edslSrc, "sorted4")
+sort6 = compareSpec (edslSrc, "sorted1") (edslSrc, "sorted4") -- does not terminate
\ No newline at end of file

src/impress/src/nl/uu/impress/EDSL.java

@@ -41,6 +41,10 @@ public class EDSL {
         return g_forall(array.length, rBegin, rEnd, pred);
     }
 
+    public static boolean forallr(int[] array, int rBegin, int rEnd, IntPred pred) {
+        return g_forall(array.length, rBegin, rEnd, pred);
+    }
+
     public static boolean exists(Object[] array, IntPred pred) {
         return g_exists(array.length, 0, array.length, pred);
     }
@@ -53,6 +57,10 @@ public class EDSL {
         return g_exists(array.length, rBegin, rEnd, pred);
     }
 
+    public static boolean existsr(int[] array, int rBegin, int rEnd, IntPred pred) {
+        return g_exists(array.length, rBegin, rEnd, pred);
+    }
+
     public static void pre(boolean pre) {
         assert pre;
     }

src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java

@@ -137,13 +137,28 @@ public class Main {
         post(true);
     }
 
-    public static void main(String[] args) {
-//        assert forall(args, i -> args[i].toLowerCase().equals(args[i]));
-//        assert forallr(args, 1, 3, i -> args[i].contains("x"));
+    //http://www.cs.uu.nl/docs/vakken/pc/1617/supplements/proofasg_1617.pdf
+    public static void sorted1(int[] a) {
+        pre(forall(a, i -> forallr(a, i, a.length, j -> a[i] <= a[j])));
+        post(true);
+    }
+
+    public static void sorted2(int[] a) {
+        pre(forall(a, i -> forallr(a, i, a.length, j -> a[i] < a[j])));
+        post(true);
+    }
 
-//        assert !exists(args, i -> !args[i].toLowerCase().equals(args[i]));
-//        assert !existsr(args, 1, 3, i -> !args[i].contains("x"));
+    public static void sorted3(int[] a) {
+        pre(forall(a, i -> forallr(a, i + 1, a.length, j -> a[i] < a[j])));
+        post(true);
+    }
+
+    public static void sorted4(int[] a) {
+        pre(forall(a, i -> forallr(a, i + 1, a.length, j -> a[i] <= a[j])));
+        post(true);
+    }
 
+    public static void main(String[] args) {
         System.out.println("Hello, world!");
     }
 }