Remove support for C# and update readme

README.md

@@ -1,6 +1,6 @@
 # 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 C# and 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. For the future, we plan to extend both the functionality and the range of supported languages.
 
 There are two ways to use the library:
 - The trait `DRandomFoundational` only needs fair coin flips as a primitive.
@@ -9,31 +9,21 @@ There are two ways to use the library:
 To run the examples in the `docs` directory, use one of the following commands:
 
 ```bash
-# C# ExamplesFoundational
-$ dafny build docs/dafny/ExamplesFoundational.dfy --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs dfyconfig.toml --no-verify
-$ dotnet docs/dafny/ExamplesFoundational.dll
-# C# ExamplesExternUniform
-$ dafny build docs/dafny/ExamplesExternUniform.dfy --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs dfyconfig.toml --no-verify
-$ dotnet docs/dafny/ExamplesExternUniform.dll
 # Java ExamplesFoundational
-$ dafny build docs/dafny/ExamplesFoundational.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java dfyconfig.toml --no-verify
+$ dafny build docs/dafny/ExamplesFoundational.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java dfyconfig.toml --no-verify
 $ java -jar docs/dafny/ExamplesFoundational.jar
 # Java ExamplesExternUniform
-$ dafny build docs/dafny/ExamplesExternUniform.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java dfyconfig.toml --no-verify
-$ java -jar docs/dafny/ExamplesExternUniform.jar
+$ dafny build docs/dafny/ExamplesExternUniformPowerOfTwo.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java dfyconfig.toml --no-verify
+$ java -jar docs/dafny/ExamplesExternUniformPowerOfTwo.jar
 ```
 
 # Testing
 
 To run the statistical tests in the `tests` diretory, use one of the following commands:
 
 ```bash
-# C# TestsFoundational
-$ dafny test --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
-# C# TestsExternUniform
-$ dafny test --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs tests/TestsExternUniform.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 # Java TestsFoundational
-$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java tests/TestsFoundationalPowerOfTwo.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 # Java TestsExternUniform
-$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java tests/TestsExternUniform.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java tests/TestsExternUniformPowerOfTwo.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 ```

docs/index.html

@@ -3,6 +3,4 @@
 <br>
 <a href="dafny/index.html">Using Dafny-VMC from Dafny</a>
 <br>
-<a href="java/index.html">Using Dafny-VMC from Java </a>
-<br>
-<a href="csharp/index.html">Using Dafny-VMC from C#</a>
+<a href="java/index.html">Using Dafny-VMC from Java </a>

scripts/test.sh

@@ -25,19 +25,15 @@ echo Running $TARGET_LANG documentation...
 echo "Building docs/dafny/ExamplesFoundational.dfy..." 
 $DAFNY build docs/dafny/ExamplesFoundational.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG dfyconfig.toml --no-verify
 echo "Executing compiled docs/dafny/ExamplesFoundational.dfy:" 
-if [ "$TARGET_LANG" = "cs" ]
+if [ "$TARGET_LANG" = "java" ]
 then
-  dotnet docs/dafny/ExamplesFoundational.dll
-else
   java -jar docs/dafny/ExamplesFoundational.jar
 fi
 
 echo "Building docs/dafny/ExamplesExternUniformPowerOfTwo.dfy..." 
 $DAFNY build docs/dafny/ExamplesExternUniformPowerOfTwo.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG dfyconfig.toml --no-verify
 echo "Executing compiled docs/dafny/ExamplesExternUniformPowerOfTwo.dfy:" 
-if [ "$TARGET_LANG" = "cs" ]
+if [ "$TARGET_LANG" = "java" ]
 then
-  dotnet docs/dafny/ExamplesExternUniformPowerOfTwo.dll
-else
   java -jar docs/dafny/ExamplesExternUniformPowerOfTwo.jar
 fi