Extending the EDSL a bit, adding example files

examples/javawlp_edsl/src/nl/uu/javawlp_edsl/GetMax.java

+package nl.uu.javawlp_edsl;
+
+import static nl.uu.impress.EDSL.*;
+
+/**
+ * An example of a simple program and its specification, written by a teacher.
+ */
+public class GetMax {
+
+	/**
+	 * A program to obtain the maximum value of an array.
+	 */
+	public static int getMax(int[] a) {
+        if (a.length == 0)
+            throw new IllegalArgumentException();
+        int m = a[0];
+        for (int i = 1; i < a.length; i++)
+            m = a[i] > m ? a[i] : m;
+        return m;
+    }
+	
+    /**
+     * Teacher's specification of getMax.
+     */
+    public static void getMax_teacherspec(int[] a) {
+        pre(a != null && a.length > 0);
+        int retval = getMax(a);
+        post(exists(a, i -> a[i] == retval) && forall(a, i -> a[i] <= retval));
+    }
+}

examples/javawlp_edsl/src/nl/uu/javawlp_edsl/GetMaxStudent.java

+package nl.uu.javawlp_edsl;
+
+import static nl.uu.impress.EDSL.*;
+
+/**
+ * Examples of incorrect specifications of the program getMax that could have been written
+ * by students.
+ */
+public class GetMaxStudent {
+
+    public static void getMax_spec2(int[] a) {
+        pre(a != null && a.length > 0);
+        int retval = GetMax.getMax(a);
+        post(forall(a, i -> a[i] <= retval));
+    }
+
+    public static void getMax_spec3(int[] a) {
+        pre(a != null && a.length > 0);
+        int retval = GetMax.getMax(a);
+        post(exists(a, i -> a[i] == retval) && forall(a, i -> a[i] < retval));
+    }
+}

examples/javawlp_edsl/src/nl/uu/javawlp_edsl/IsSorted.java

+package nl.uu.javawlp_edsl;
+
+import static nl.uu.impress.EDSL.*;
+
+public class IsSorted {
+	
+	/**
+	 * A program to check is an array is sorted.
+	 */
+	public static boolean isSorted(int[] a) {
+		if (a==null) throw new IllegalArgumentException() ;
+		if (a.length <= 1) return true ;
+		boolean ok = false ;
+		for(int i=1; i<a.length; i++) 
+			if (a[i-1]>a[i]) return false ;
+		return true ;
+	}
+
+    public static void isSorted_teacherspec(int[] a) {
+    	pre(a != null) ;
+    	boolean retval = isSorted(a) ;
+    	post(retval == forall(a, i -> forall(a, j -> imp(i<=j, a[i] <= a[j]))));
+
+    }
+    
+}

examples/javawlp_edsl/src/nl/uu/javawlp_edsl/IsSortedStudent.java

+package nl.uu.javawlp_edsl;
+
+import static nl.uu.impress.EDSL.*;
+
+/**
+ * Examples of specifications of the program isSorted that could have been written
+ * by students. Mosy of the are incorrects. Spec4 looks different that the teacher's version,
+ * but it should be equivalent.
+ */
+public class IsSortedStudent {
+
+    public static void isSorted_spec1(int[] a) {
+    	pre(a != null) ;
+    	boolean retval = IsSorted.isSorted(a) ;
+    	post(retval == forall(a, i -> forall(a, j -> imp(i<=j, a[i] < a[j]))));
+
+    }
+
+    public static void isSorted_spec2(int[] a) {
+    	pre(a != null) ;
+    	boolean retval = IsSorted.isSorted(a) ;
+    	post(retval == forall(a, i -> forall(a, j -> imp(i<=j, a[i] >= a[j]))));
+
+    }
+
+    public static void isSorted_spec3(int[] a) {
+    	pre(a != null) ;
+    	boolean retval = IsSorted.isSorted(a) ;
+    	post(retval == forall(a, i -> a[i-1] <= a[i]));
+    }
+    
+    public static void isSorted_spec4(int[] a) {
+    	pre(a != null) ;
+    	boolean retval = IsSorted.isSorted(a) ;
+    	post(retval == forall(a, i -> imp(0<i,a[i-1] <= a[i]))) ;
+    }
+    
+    // few tests
+    public static void main(String[] args) {
+    	int[] a = { 0,1,1 } ;
+    	
+    }
+
+}

examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Swap.java

+package nl.uu.javawlp_edsl;
+
+import static nl.uu.impress.EDSL.*;
+
+public class Swap {
+	
+	/**
+	 * Swap two elements of an array.
+	 */
+    public static void swap(int[] a, int i, int j) {
+        int temp = a[i];
+        a[i] = a[j];
+        a[j] = temp;
+    }
+    
+    /**
+     * Teacher's specification of Swap.
+     */
+    public static void swap_teacherspec(int[] a, int i, int j) {
+        pre(a != null);
+        pre(a.length > 0);
+        pre(i >= 0);
+        pre(j >= 0);
+        // introducing vars to remember old values
+        int oldai = a[i], oldaj = a[j];
+        swap(a, i, j);
+        post(a[j] == oldai);
+        post(a[i] == oldaj);
+    }
+
+}

examples/javawlp_edsl/src/nl/uu/javawlp_edsl/SwapStudent.java

+package nl.uu.javawlp_edsl;
+
+import static nl.uu.impress.EDSL.*;
+
+/**
+ * Examples of incorrect specifications of the program swap that could have been written
+ * by students.
+ */
+public class SwapStudent {
+	
+	public static void swap_spec1(int[] a, int i, int j) {
+        pre(a != null);
+        pre(a.length > 0);
+        pre(i >= 0);
+        pre(j >= 0);
+        // introducing vars to remember old values
+        int oldai = a[i], oldaj = a[j];
+        Swap.swap(a, i, j);
+        post(a[j] == oldai);
+        post(a[i] == oldaj);
+    }
+	
+	 public static void swap_spec2(int[] a, int i, int j) {
+	    pre(a != null && a[0] == 0);
+	    pre(a != null && a.length > 0 && i >= 0 && j > 0);
+	    // introducing vars to remember old values
+	    int oldai = a[i], oldaj = a[j];
+	    Swap.swap(a, i, j);
+	    post(a[j] == oldai && a[i] == oldaj);
+	}
+
+	public static void swap_spec3(int[] a, int i, int j) {
+        pre(a == null);
+        pre(a.length > 0);
+        pre(i >= 0);
+        pre(j >= 0);
+        // introducing vars to remember old values
+        int oldai = a[i], oldaj = a[j];
+        Swap.swap(a, i, j);
+        post(a[j] == oldai);
+        post(a[i] == oldaj);
+	}
+
+    public static void swap_spec4(int[] a, int i, int j) {
+        pre(a.length > 0);
+        pre(i >= 0);
+        pre(j >= 0);
+        // introducing vars to remember old values
+        int oldai = a[i], oldaj = a[j];
+        Swap.swap(a, i, j);
+        post(a[j] == oldai);
+        post(a[i] == oldaj);
+    }
+
+}

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

@@ -2,15 +2,20 @@ package nl.uu.impress;
 
 public class EDSL {
     public interface IntPred {
-        boolean invoke(int n);
+        boolean invoke(int i);
     }
 
+    public interface IntPred2 {
+        boolean invoke(int i, int j);
+    }
+    
     private static boolean g_forall(int aLength, int rBegin, int rEnd, IntPred pred) {
         for (int index = rBegin; index < rEnd; index++) {
             //TODO: determine if pred should be called with indices outside of the array range
             //NOTE: only relevant for the runtime implementation
             if (index < 0 || index >= aLength)
-                continue; //assert false;
+            	throw new ArrayIndexOutOfBoundsException("index=" + index + ", array length=" + aLength) ;
+                // continue; //assert false;
             if (!pred.invoke(index))
                 return false;
         }
@@ -22,13 +27,17 @@ public class EDSL {
             //TODO: determine if pred should be called with indices outside of the array range
             //NOTE: only relevant for the runtime implementation
             if (index < 0 || index >= aLength)
-                continue; //assert false;
+            	throw new ArrayIndexOutOfBoundsException("index=" + index + ", array length=" + aLength) ;
+                //continue; //assert false;
             if (pred.invoke(index))
                 return true;
         }
         return false;
     }
 
+    public static boolean imp(boolean p, boolean q) {
+    	return !p || p ;
+    }
     public static boolean forall(Object[] array, IntPred pred) {
         return g_forall(array.length, 0, array.length, pred);
     }
@@ -36,6 +45,10 @@ public class EDSL {
     public static boolean forall(int[] array, IntPred pred) {
         return g_forall(array.length, 0, array.length, pred);
     }
+    
+    //public static boolean forall(int[][] array, IntPred2 pred) {
+    //    return g_forall(array.length, 0, array.length, pred);
+    //}
 
     public static boolean forallr(Object[] array, int rBegin, int rEnd, IntPred pred) {
         return g_forall(array.length, rBegin, rEnd, pred);
@@ -61,11 +74,14 @@ public class EDSL {
         return g_exists(array.length, rBegin, rEnd, pred);
     }
 
+    public static class PreConditionError extends AssertionError { }
+    public static class PostConditionError extends AssertionError { }
+    
     public static void pre(boolean pre) {
-        assert pre;
+        if(!pre) throw new PreConditionError() ;
     }
 
     public static void post(boolean post) {
-        assert post;
+        if (!post) throw new PostConditionError() ;
     }
 }