From ee12d495625bca955365003b2cb349d47a954c74 Mon Sep 17 00:00:00 2001
From: stefan-aws <stefanze@amazon.com>
Date: Mon, 11 Mar 2024 12:43:59 +0000
Subject: [PATCH 1/4] fix to readme

---
 README.md                     | 60 +++++++++++++++++++++++++++++------
 docs/dafny/ExamplesRandom.dfy |  2 +-
 2 files changed, 52 insertions(+), 10 deletions(-)

diff --git a/README.md b/README.md
index 3eca5386..3de7b00a 100644
--- a/README.md
+++ b/README.md
@@ -1,8 +1,10 @@
 # VMC: a Library for Verified Monte Carlo Algorithms
 
-The `DafnyVMC` module introduces utils for probabilistic reasoning in Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java. For the future, we plan to extend both the functionality and the range of supported languages.
+The `DafnyVMC` module introduces utils for probabilistic reasoning in Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java and Python. For the future, we plan to extend both the functionality and the range of supported languages.
 
-## Java API Example
+## Java
+
+### Java API
 
 ```java
 import DafnyVMC.Random;
@@ -26,31 +28,71 @@ class Test {
 }
 ```
 
-## Dafny Examples
+### Java Examples
 
-To run the examples in the `docs/dafny` directory, use the following commands:
+To run the examples in the `docs/java` directory, use the following commands:
+
+```bash
+$ export TARGET_LANG=java
+$ bash scripts/build.sh
+$ bash build/java/run_samplers.sh
+$ bash build/java/run_shuffling.sh
+```
+
+To run the tests in the `docs/dafny` directory, use the following commands:
 
 ```bash
 $ dafny build docs/dafny/ExamplesRandom.dfy --target:java src/interop/java/Full/Random.java src/interop/java/Part/Random.java dfyconfig.toml --no-verify
 $ java -jar docs/dafny/ExamplesRandom.jar
 ```
 
-## Java Examples
+To run the statistical tests in the `tests` directory, use the following commands:
+
+```bash
+$ dafny test --target:java src/interop/java/Full/Random.java src/interop/java/Part/Random.java tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+```
+
+## Python
+
+### Python API
+
+```py
+import DafnyVMC
+
+def main():
+  r = DafnyVMC.Random()
+
+  print("Example of Fisher-Yates shuffling")
+  arr = ['a', 'b', 'c']
+  arr = r.Shuffle(arr)
+  print(arr)
+  
+  print("Example of Bernoulli sampling")
+  print(r.BernoulliSample(3, 5))
+```
+
+### Python Examples
 
 To run the examples in the `docs/java` directory, use the following commands:
 
 ```bash
-$ export TARGET_LANG=java
+$ export TARGET_LANG=py
 $ bash scripts/build.sh
-$ bash build/java/run.sh 
+$ bash build/py/run_samplers.sh
+$ bash build/py/run_shuffling.sh
 ```
 
-## Dafny Testing
+To run the tests in the `docs/dafny` directory, use the following commands:
+
+```bash
+$ dafny build docs/dafny/ExamplesRandom.dfy --target:py src/interop/py/Full/Random.py src/interop/py/Part/Random.py dfyconfig.toml --no-verify
+$ python3 docs/dafny/ExamplesRandom-py/__main__.py
+```
 
 To run the statistical tests in the `tests` directory, use the following commands:
 
 ```bash
-$ dafny test --target:java src/interop/java/Full/Random.java src/interop/java/Part/Random.java tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+$ dafny test --target:py src/interop/py/Full/Random.py src/interop/py/Part/Random.py tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 ```
 
 
diff --git a/docs/dafny/ExamplesRandom.dfy b/docs/dafny/ExamplesRandom.dfy
index 041f1ad0..be8658e3 100644
--- a/docs/dafny/ExamplesRandom.dfy
+++ b/docs/dafny/ExamplesRandom.dfy
@@ -73,7 +73,7 @@ module Examples {
       }
     }
 
-    print "Estimated parameter for BernoulliSample(5, 5): ", (t as real) / (n as real), " (should be around 1.0\n";
+    print "Estimated parameter for BernoulliSample(5, 5): ", (t as real) / (n as real), " (should be around 1.0)\n";
 
     t := 0;
     for i := 0 to n {

From 3b2e159e5788571daa0a0235daac4570ce365d43 Mon Sep 17 00:00:00 2001
From: stefan-aws <stefanze@amazon.com>
Date: Mon, 11 Mar 2024 12:47:56 +0000
Subject: [PATCH 2/4] newline

---
 README.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/README.md b/README.md
index 3de7b00a..9b360f86 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,7 @@
 
 The `DafnyVMC` module introduces utils for probabilistic reasoning in Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java and Python. For the future, we plan to extend both the functionality and the range of supported languages.
 
+
 ## Java
 
 ### Java API
@@ -52,6 +53,7 @@ To run the statistical tests in the `tests` directory, use the following command
 $ dafny test --target:java src/interop/java/Full/Random.java src/interop/java/Part/Random.java tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 ```
 
+
 ## Python
 
 ### Python API

From adff9b8acd24511b4bb18af8b0bc15f14de76b3d Mon Sep 17 00:00:00 2001
From: stefan-aws <stefanze@amazon.com>
Date: Mon, 11 Mar 2024 12:50:06 +0000
Subject: [PATCH 3/4] empty line

---
 README.md | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index 9b360f86..d443e102 100644
--- a/README.md
+++ b/README.md
@@ -1,8 +1,7 @@
 # VMC: a Library for Verified Monte Carlo Algorithms
 
 The `DafnyVMC` module introduces utils for probabilistic reasoning in Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java and Python. For the future, we plan to extend both the functionality and the range of supported languages.
-
-
+<br />
 ## Java
 
 ### Java API
@@ -53,7 +52,7 @@ To run the statistical tests in the `tests` directory, use the following command
 $ dafny test --target:java src/interop/java/Full/Random.java src/interop/java/Part/Random.java tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 ```
 
-
+<br />
 ## Python
 
 ### Python API

From 88b84fa45ac38bf8c43d87480162bbf0e4c5b817 Mon Sep 17 00:00:00 2001
From: stefan-aws <stefanze@amazon.com>
Date: Mon, 11 Mar 2024 12:50:49 +0000
Subject: [PATCH 4/4] remove tags

---
 README.md | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/README.md b/README.md
index d443e102..3de7b00a 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
 # VMC: a Library for Verified Monte Carlo Algorithms
 
 The `DafnyVMC` module introduces utils for probabilistic reasoning in Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java and Python. For the future, we plan to extend both the functionality and the range of supported languages.
-<br />
+
 ## Java
 
 ### Java API
@@ -52,7 +52,6 @@ To run the statistical tests in the `tests` directory, use the following command
 $ dafny test --target:java src/interop/java/Full/Random.java src/interop/java/Part/Random.java tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 ```
 
-<br />
 ## Python
 
 ### Python API