From efa003f6e3dcc10f9e1e0ca405a0f2557debd795 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 21 Feb 2024 21:06:19 +0000 Subject: [PATCH] simpler api --- build/java/run.sh | 2 +- docs/java/BuildTest.java | 80 +++++++++++++------ docs/java/CustomFIsherYatesFaulty.java | 58 ++++++++++++++ ...formSample.java => CustomFisherYates.java} | 46 ++++++++++- docs/java/CustomUniformSampleFaulty.java | 15 ---- src/Util/FisherYates/Implementation.dfy | 10 +-- src/Util/FisherYates/Interface.dfy | 6 +- src/interop/java/Full/Random.java | 46 +++-------- 8 files changed, 176 insertions(+), 87 deletions(-) create mode 100644 docs/java/CustomFIsherYatesFaulty.java rename docs/java/{CustomUniformSample.java => CustomFisherYates.java} (52%) delete mode 100644 docs/java/CustomUniformSampleFaulty.java diff --git a/build/java/run.sh b/build/java/run.sh index bc262468..94fd5695 100755 --- 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 index 03970c41..6c570dcb 100644 --- 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 new file mode 100644 index 00000000..82fb57ea --- /dev/null +++ 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 b/docs/java/CustomFisherYates.java similarity index 52% rename from docs/java/CustomUniformSample.java rename to docs/java/CustomFisherYates.java index 8ecb3f0d..1d3b12b6 100644 --- a/docs/java/CustomUniformSample.java +++ b/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 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); } -} \ No newline at end of file +} + + +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 deleted file mode 100644 index d6ec88fe..00000000 --- a/docs/java/CustomUniformSampleFaulty.java +++ /dev/null @@ -1,15 +0,0 @@ -import Uniform.Interface.TraitMinus; -import Uniform.Interface.Trait; -import java.math.BigInteger; - -class CustomUniformSampleFaultyMinus implements Uniform.Interface.TraitMinus { - public BigInteger UniformSample(BigInteger n) { - return BigInteger.valueOf(0); // Faulty; only for demonstration purposes - } -} - -public class CustomUniformSampleFaulty 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); - } -} \ No newline at end of file diff --git a/src/Util/FisherYates/Implementation.dfy b/src/Util/FisherYates/Implementation.dfy index 727e9fe2..20a1b5b1 100644 --- 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(a: array, t: Uniform.Interface.Trait := this) + method Shuffle(a: array) 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 index f02d92ab..1571870d 100644 --- 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(a: array, t: Uniform.Interface.Trait := this) + method Shuffle(a: array) 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) } } \ No newline at end of file diff --git a/src/interop/java/Full/Random.java b/src/interop/java/Full/Random.java index 7a0c60f0..a186e8ca 100644 --- 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) {