constructor without arguments

docs/java/BuildTest.java

@@ -24,6 +24,57 @@ public static void main(String[] args) {
         short[] arr7 = {-3, 0, 3};
         Rationals.Rational gamma = new Rationals.Rational(BigInteger.valueOf(3), BigInteger.valueOf(5));
 
+        /* STANDARD RNG */
+        System.out.println("\nSTANDARD RNG TESTS\n");
+
+        DafnyVMC.Random r = new DafnyVMC.Random();
+
+        System.out.println("Example of Coin sampling");
+        System.out.println(r.CoinSample());
+
+        System.out.println("Example of Uniform sampling");
+        System.out.println(r.UniformSample(BigInteger.valueOf(4)));
+
+        System.out.println("Example of Bernoulli sampling");
+        System.out.println(r.BernoulliSample(gamma));
+
+        System.out.println("Example of BernoulliExpNeg sampling");
+        System.out.println(r.BernoulliExpNegSample(gamma));
+
+        System.out.println("Example of DiscreteGaussian sampling");
+        System.out.println(r.DiscreteGaussianSample(gamma));
+
+        System.out.println("Example of DiscreteLaplace sampling");
+        System.out.println(r.DiscreteLaplaceSample(gamma));
+
+        System.out.println("Example of Fisher-Yates: BigInteger");
+        r.Shuffle(arr1);
+        System.out.println(Arrays.toString(arr1));
+
+        System.out.println("Example of Fisher-Yates: int");
+        r.Shuffle(arr2);
+        System.out.println(Arrays.toString(arr2));
+
+        System.out.println("Example of Fisher-Yates: String");
+        r.Shuffle(arr3);
+        System.out.println(Arrays.toString(arr3));
+
+        System.out.println("Example of Fisher-Yates: char");
+        r.Shuffle(arr4);
+        System.out.println(Arrays.toString(arr4));
+
+        System.out.println("Example of Fisher-Yates: boolean");
+        r.Shuffle(arr5);
+        System.out.println(Arrays.toString(arr5));
+
+        System.out.println("Example of Fisher-Yates: long");
+        r.Shuffle(arr6);
+        System.out.println(Arrays.toString(arr6));
+
+        System.out.println("Example of Fisher-Yates: short");
+        r.Shuffle(arr7);
+        System.out.println(Arrays.toString(arr7));
+
         /* CUSTOM RNG */
         System.out.println("\nCUSTOM RNG TESTS\n");
 

src/interop/java/Full/Random.java

@@ -2,19 +2,40 @@
 
 import dafny.TypeDescriptor;
 import java.math.BigInteger;
+import java.security.SecureRandom;
 import java.util.function.Function;
 
 public class Random implements DafnyVMCTrait.RandomTrait {  
   static Function<BigInteger, BigInteger> unif;
 
+  public Random() {
+    ThreadLocal<SecureRandom> rng = ThreadLocal.withInitial(Random::createSecureRandom); 
+    Random.unif = n -> UniformPowerOfTwoSample(n, rng);
+  }
+
   public Random(Function<BigInteger, BigInteger> unif) {
     Random.unif = unif;
   }
 
+  private static final SecureRandom createSecureRandom() {
+    final SecureRandom rng = new SecureRandom();
+    // Required for proper initialization
+    rng.nextBoolean(); 
+    return rng;
+  }
+
   public BigInteger UniformPowerOfTwoSample(BigInteger n) {
     return unif.apply(n);
   }
 
+  public BigInteger UniformPowerOfTwoSample(BigInteger n, ThreadLocal<SecureRandom> rng) {
+    if (n.compareTo(BigInteger.ONE) < 0) {
+      throw new IllegalArgumentException("n must be positive");
+    }
+
+    return new BigInteger(n.bitLength()-1, rng.get());
+  }
+
   public java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.math.BigInteger b) {
     return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b);
   }