simpler api

dafny-lang · Feb 21, 2024 · efa003f · efa003f
1 parent 51c8738
commit efa003f
Show file tree

Hide file tree

Showing 8 changed files with 176 additions and 87 deletions.
diff --git a/build/java/run.sh b/build/java/run.sh
@@ -1,3 +1,3 @@
 #1/bin/bash
-javac -classpath "build/java/DafnyVMC.jar:docs/java/" docs/java/CustomUniformSample.java docs/java/CustomUniformSampleFaulty.java
+javac -classpath "build/java/DafnyVMC.jar:docs/java/" docs/java/CustomFisherYates.java docs/java/CustomFisherYatesFaulty.java
 java -classpath "build/java/DafnyVMC.jar:docs/java/" docs/java/BuildTest.java 
diff --git a/docs/java/BuildTest.java b/docs/java/BuildTest.java
@@ -1,27 +1,35 @@
-import java.security.SecureRandom;
 import java.math.BigInteger;
 import java.util.Arrays;
 
-import DafnyVMC.Random;
-import Uniform.Interface.TraitMinus;
-import Uniform.Interface.Trait;
-
 public class BuildTest {
     public static void main(String[] args) {
         BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)};
-        BigInteger[] arr1b = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)};
+        BigInteger[] arr1_custom = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)};
+        BigInteger[] arr1_faulty = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)};
         int[] arr2 = {0, 1, 2};
+        int[] arr2_custom = {0, 1, 2};
+        int[] arr2_faulty = {0, 1, 2};
         String[] arr3 = {"aa", "bb", "cc"};
+        String[] arr3_custom = {"aa", "bb", "cc"};
+        String[] arr3_faulty = {"aa", "bb", "cc"};
         char[] arr4 = {'a', 'b', 'c'};
+        char[] arr4_custom = {'a', 'b', 'c'};
+        char[] arr4_faulty = {'a', 'b', 'c'};
         boolean[] arr5 = {true, false, false, true};
+        boolean[] arr5_custom = {true, false, false, true};
+        boolean[] arr5_faulty = {true, false, false, true};
         long[] arr6 = {111111L, 333333L, 999999L};
+        long[] arr6_custom = {111111L, 333333L, 999999L};
+        long[] arr6_faulty = {111111L, 333333L, 999999L};
         short[] arr7 = {-3, 0, 3};
+        short[] arr7_custom = {-3, 0, 3};
+        short[] arr7_faulty = {-3, 0, 3};
         BigInteger num = BigInteger.valueOf(3);
         BigInteger den = BigInteger.valueOf(5);
 
         DafnyVMC.Random r = new DafnyVMC.Random();
-        Uniform.Interface.Trait t = new CustomUniformSample();
-        Uniform.Interface.Trait t_faulty = new CustomUniformSampleFaulty();
+        CustomFisherYates r_custom = new CustomFisherYates();
+        CustomFisherYatesFaulty r_faulty = new CustomFisherYatesFaulty();
 
         System.out.println("Example of Uniform sampling");
         System.out.println(r.UniformSample(BigInteger.valueOf(4)));
@@ -43,60 +51,84 @@ public static void main(String[] args) {
         System.out.println(Arrays.toString(arr1));
 
         System.out.println("Example of custom Fisher-Yates: BigInteger");
-        r.Shuffle(arr1, t);
-        System.out.println(Arrays.toString(arr1));
+        r_custom.Shuffle(arr1_custom);
+        System.out.println(Arrays.toString(arr1_custom));
 
         System.out.println("Example of faulty custom Fisher-Yates: BigInteger");
-        r.Shuffle(arr1b, t_faulty);
-        System.out.println(Arrays.toString(arr1b));
+        r_faulty.Shuffle(arr1_faulty);
+        System.out.println(Arrays.toString(arr1_faulty));
 
         System.out.println("Example of Fisher-Yates: int");
         r.Shuffle(arr2);
         System.out.println(Arrays.toString(arr2));
 
         System.out.println("Example of custom Fisher-Yates: int");
-        r.Shuffle(arr2, t);
-        System.out.println(Arrays.toString(arr2));
+        r_custom.Shuffle(arr2_custom);
+        System.out.println(Arrays.toString(arr2_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: int");
+        r_faulty.Shuffle(arr2_faulty);
+        System.out.println(Arrays.toString(arr2_faulty));
 
         System.out.println("Example of Fisher-Yates: String");
         r.Shuffle(arr3);
         System.out.println(Arrays.toString(arr3));
 
         System.out.println("Example of custom Fisher-Yates: String");
-        r.Shuffle(arr3, t);
-        System.out.println(Arrays.toString(arr3));
+        r_custom.Shuffle(arr3_custom);
+        System.out.println(Arrays.toString(arr3_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: String");
+        r_faulty.Shuffle(arr3_faulty);
+        System.out.println(Arrays.toString(arr3_faulty));
 
         System.out.println("Example of Fisher-Yates: char");
         r.Shuffle(arr4);
         System.out.println(Arrays.toString(arr4));
 
         System.out.println("Example of custom Fisher-Yates: char");
-        r.Shuffle(arr4, t);
-        System.out.println(Arrays.toString(arr4));
+        r_custom.Shuffle(arr4_custom);
+        System.out.println(Arrays.toString(arr4_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: char");
+        r_faulty.Shuffle(arr4_faulty);
+        System.out.println(Arrays.toString(arr4_faulty));
 
         System.out.println("Example of Fisher-Yates: boolean");
         r.Shuffle(arr5);
         System.out.println(Arrays.toString(arr5));
 
         System.out.println("Example of custom Fisher-Yates: boolean");
-        r.Shuffle(arr5, t);
-        System.out.println(Arrays.toString(arr5));
+        r_custom.Shuffle(arr5_custom);
+        System.out.println(Arrays.toString(arr5_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: boolean");
+        r_faulty.Shuffle(arr5_faulty);
+        System.out.println(Arrays.toString(arr5_faulty));
 
         System.out.println("Example of Fisher-Yates: long");
         r.Shuffle(arr6);
         System.out.println(Arrays.toString(arr6));
 
         System.out.println("Example of custom Fisher-Yates: long");
-        r.Shuffle(arr6, t);
-        System.out.println(Arrays.toString(arr6));
+        r_custom.Shuffle(arr6_custom);
+        System.out.println(Arrays.toString(arr6_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: long");
+        r_faulty.Shuffle(arr6_faulty);
+        System.out.println(Arrays.toString(arr6_faulty));
 
         System.out.println("Example of Fisher-Yates: short");
         r.Shuffle(arr7);
         System.out.println(Arrays.toString(arr7));
 
         System.out.println("Example of custom Fisher-Yates: short");
-        r.Shuffle(arr7, t);
-        System.out.println(Arrays.toString(arr7));
+        r_custom.Shuffle(arr7_custom);
+        System.out.println(Arrays.toString(arr7_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: short");
+        r_faulty.Shuffle(arr7_faulty);
+        System.out.println(Arrays.toString(arr7_faulty));
     }
 }
 
diff --git a/docs/java/CustomFIsherYatesFaulty.java b/docs/java/CustomFIsherYatesFaulty.java
@@ -0,0 +1,58 @@
+import Uniform.Interface.TraitMinus;
+import Uniform.Interface.Trait;
+import java.math.BigInteger;
+import java.security.SecureRandom;
+import java.util.Random;
+import dafny.TypeDescriptor;
+
+class CustomUniformSampleFaultyMinus implements Uniform.Interface.TraitMinus {  
+  public BigInteger UniformSample(BigInteger n) {
+    return BigInteger.valueOf(0);
+  }
+}
+
+class CustomUniformFaulty extends CustomUniformSampleFaultyMinus implements Uniform.Interface.Trait {
+  public java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.math.BigInteger b) {
+    return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b);
+  }
+}
+
+class CustomFisherYatesMinusFaulty extends CustomUniformFaulty implements FisherYates.Implementation.Trait {
+  public <__T> void Shuffle(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a) {
+    FisherYates.Implementation._Companion_Trait.Shuffle(_td___T, this, a);
+  }
+
+  public <__T> void Swap(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, java.math.BigInteger i, java.math.BigInteger j) {
+    FisherYates.Implementation._Companion_Trait.Swap(_td___T, this, a, i, j);
+  }
+}
+
+public class CustomFisherYatesFaulty extends CustomFisherYatesMinusFaulty {
+  public void Shuffle(BigInteger[] arr) {
+    this.Shuffle(TypeDescriptor.BIG_INTEGER, arr);
+  }
+
+  public void Shuffle(int[] arr) {
+    this.Shuffle(TypeDescriptor.INT, arr);
+  }
+
+  public void Shuffle(String[] arr) {
+    this.Shuffle(TypeDescriptor.CHAR_ARRAY, arr);
+  }
+
+  public void Shuffle(char[] arr) {
+    this.Shuffle(TypeDescriptor.CHAR, arr);
+  }
+
+  public void Shuffle(boolean[] arr) {
+    this.Shuffle(TypeDescriptor.BOOLEAN, arr);
+  }
+
+  public void Shuffle(long[] arr) {
+    this.Shuffle(TypeDescriptor.LONG, arr);
+  }
+
+  public void Shuffle(short[] arr) {
+    this.Shuffle(TypeDescriptor.SHORT, arr);
+  }
+}
diff --git a/docs/java/CustomUniformSample.java → docs/java/CustomFisherYates.java b/docs/java/CustomUniformSample.java → docs/java/CustomFisherYates.java
@@ -3,6 +3,7 @@
 import java.math.BigInteger;
 import java.security.SecureRandom;
 import java.util.Random;
+import dafny.TypeDescriptor;
 
 class CustomUniformSampleMinus implements Uniform.Interface.TraitMinus {
   static ThreadLocal<SecureRandom> rng;
@@ -40,8 +41,49 @@ public BigInteger UniformSample(BigInteger n) {
   }
 }
 
-public class CustomUniformSample extends CustomUniformSampleMinus implements Uniform.Interface.Trait {
+class CustomUniform extends CustomUniformSampleMinus implements Uniform.Interface.Trait {
   public java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.math.BigInteger b) {
     return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b);
   }
-}
+}
+
+
+class CustomFisherYatesMinus extends CustomUniform implements FisherYates.Implementation.Trait {
+  public <__T> void Shuffle(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a) {
+    FisherYates.Implementation._Companion_Trait.Shuffle(_td___T, this, a);
+  }
+
+  public <__T> void Swap(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, java.math.BigInteger i, java.math.BigInteger j) {
+    FisherYates.Implementation._Companion_Trait.Swap(_td___T, this, a, i, j);
+  }
+}
+
+public class CustomFisherYates extends CustomFisherYatesMinus {
+  public void Shuffle(BigInteger[] arr) {
+    this.Shuffle(TypeDescriptor.BIG_INTEGER, arr);
+  }
+
+  public void Shuffle(int[] arr) {
+    this.Shuffle(TypeDescriptor.INT, arr);
+  }
+
+  public void Shuffle(String[] arr) {
+    this.Shuffle(TypeDescriptor.CHAR_ARRAY, arr);
+  }
+
+  public void Shuffle(char[] arr) {
+    this.Shuffle(TypeDescriptor.CHAR, arr);
+  }
+
+  public void Shuffle(boolean[] arr) {
+    this.Shuffle(TypeDescriptor.BOOLEAN, arr);
+  }
+
+  public void Shuffle(long[] arr) {
+    this.Shuffle(TypeDescriptor.LONG, arr);
+  }
+
+  public void Shuffle(short[] arr) {
+    this.Shuffle(TypeDescriptor.SHORT, arr);
+  }
+}
diff --git a/docs/java/CustomUniformSampleFaulty.java b/docs/java/CustomUniformSampleFaulty.java
diff --git a/src/Util/FisherYates/Implementation.dfy b/src/Util/FisherYates/Implementation.dfy
@@ -12,18 +12,18 @@ module FisherYates.Implementation {
 
   trait {:termination false} Trait extends Interface.Trait {
 
-    method Shuffle<T>(a: array<T>, t: Uniform.Interface.Trait := this)
+    method Shuffle<T>(a: array<T>)
       decreases *
-      modifies this, a, t
-      ensures (t == this) ==> Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s)
+      modifies `s, a
+      ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s)
     {
       ghost var prevI, prevASeq, prevS := 0, a[..], s; // ghost
       if a.Length > 1 {
         for i := 0 to a.Length - 1
-          invariant (t == this) ==> Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s)
+          invariant Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s)
         {
           prevI, prevASeq, prevS := i, a[..], s; // ghost
-          var j := t.UniformIntervalSample(i, a.Length);
+          var j := UniformIntervalSample(i, a.Length);
           assert prevASeq == a[..]; // ghost
           Swap(a, i, j);
         }

diff --git a/src/Util/FisherYates/Interface.dfy b/src/Util/FisherYates/Interface.dfy
@@ -10,10 +10,10 @@ module FisherYates.Interface {
 
   trait {:termination false} Trait extends Uniform.Interface.Trait {
 
-    method Shuffle<T>(a: array<T>, t: Uniform.Interface.Trait := this)
+    method Shuffle<T>(a: array<T>)
       decreases *
-      modifies this, a, t
-      ensures (t == this) ==> Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s)
+      modifies `s, a
+      ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s)
 
   }
 }
diff --git a/src/interop/java/Full/Random.java b/src/interop/java/Full/Random.java
@@ -95,64 +95,36 @@ public java.math.BigInteger DiscreteLaplaceSample(java.math.BigInteger num, java
     return DafnyVMCTrait._Companion_RandomTrait.DiscreteLaplaceSample(this, num, den);
   }
 
-  public <__T> void Shuffle(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, Uniform.Interface.Trait t) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(_td___T, this, a, t);
+  public <__T> void Shuffle(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a) {
+    FisherYates.Implementation._Companion_Trait.Shuffle(_td___T, this, a);
   }
 
   public void Shuffle(BigInteger[] arr) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr, this);
-  }
-
-  public void Shuffle(BigInteger[] arr, Uniform.Interface.Trait t) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr, t);
+    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr);
   }
 
   public void Shuffle(int[] arr) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr, this);
-  }
-
-  public void Shuffle(int[] arr, Uniform.Interface.Trait t) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr, t);
+    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr);
   }
 
   public void Shuffle(String[] arr) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr, this);
-  }
-
-  public void Shuffle(String[] arr, Uniform.Interface.Trait t) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr, t);
+    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr);
   }
 
   public void Shuffle(char[] arr) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr, this);
-  }
-
-  public void Shuffle(char[] arr, Uniform.Interface.Trait t) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr, t);
+    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr);
   }
 
   public void Shuffle(boolean[] arr) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr, this);
-  }
-
-  public void Shuffle(boolean[] arr, Uniform.Interface.Trait t) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr, t);
+    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr);
   }
 
   public void Shuffle(long[] arr) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr, this);
-  }
-
-  public void Shuffle(long[] arr, Uniform.Interface.Trait t) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr, t);
+    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr);
   }
 
   public void Shuffle(short[] arr) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.SHORT, this, arr, this);
-  }
-
-  public void Shuffle(short[] arr, Uniform.Interface.Trait t) {
-    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.SHORT, this, arr, t);
+    FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.SHORT, this, arr);
   }
 
   public <__T> void Swap(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, java.math.BigInteger i, java.math.BigInteger j) {