From 38e583e022484ebeb9997f193b0baa5a4f6faf86 Mon Sep 17 00:00:00 2001 From: Stefan Zetzsche <120379523+stefan-aws@users.noreply.github.com> Date: Mon, 18 Mar 2024 17:04:40 +0000 Subject: [PATCH] Fix documentation and comments (#167) By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- audit.log | 2 +- docs/dafny/index.html | 2 +- docs/index.html | 4 +++- docs/java/index.html | 6 ++++-- docs/py/index.html | 7 +++++++ scripts/gendoc.sh | 15 ++++++++++++--- src/Distributions/Uniform/Model.dfy | 1 - src/Math/Analysis/Reals.dfy | 5 ----- src/Math/Helper.dfy | 1 + src/ProbabilisticProgramming/Monad.dfy | 3 +-- 10 files changed, 30 insertions(+), 16 deletions(-) create mode 100644 docs/py/index.html diff --git a/audit.log b/audit.log index 5bda4eaf..4818bc54 100644 --- a/audit.log +++ b/audit.log @@ -1,3 +1,3 @@ src/DafnyVMC.dfy(35,27): UniformSample32: Declaration has `{:verify false}` attribute. -src/Distributions/Uniform/Model.dfy(19,26): Sample: Declaration has explicit `{:axiom}` attribute. +src/Distributions/Uniform/Model.dfy(18,26): Sample: Declaration has explicit `{:axiom}` attribute. src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. diff --git a/docs/dafny/index.html b/docs/dafny/index.html index e14e17a7..400f58fa 100644 --- a/docs/dafny/index.html +++ b/docs/dafny/index.html @@ -2,4 +2,4 @@
Dafny documentation
-Example using the foundational uniform sampler \ No newline at end of file +Examples of Sampling \ No newline at end of file diff --git a/docs/index.html b/docs/index.html index b1e237c7..d7d9b14c 100644 --- a/docs/index.html +++ b/docs/index.html @@ -3,4 +3,6 @@
Using Dafny-VMC from Dafny
-Using Dafny-VMC from Java \ No newline at end of file +Using Dafny-VMC from Java +
+Using Dafny-VMC from Python \ No newline at end of file diff --git a/docs/java/index.html b/docs/java/index.html index 4bf2b290..b85d619f 100644 --- a/docs/java/index.html +++ b/docs/java/index.html @@ -1,5 +1,7 @@ Using the Dafny-VMC library in a Java application.
-Java documentation +Java documentation
-Example \ No newline at end of file +Examples of Sampling +
+Examples of Shuffling \ No newline at end of file diff --git a/docs/py/index.html b/docs/py/index.html new file mode 100644 index 00000000..5552bed7 --- /dev/null +++ b/docs/py/index.html @@ -0,0 +1,7 @@ +Using the Dafny-VMC library in a Python application. +
+Python documentation +
+Examples of Sampling +
+Examples of Shuffling \ No newline at end of file diff --git a/scripts/gendoc.sh b/scripts/gendoc.sh index f5473dad..e4678af3 100755 --- a/scripts/gendoc.sh +++ b/scripts/gendoc.sh @@ -18,6 +18,15 @@ echo Generating Dafny documentation... $DAFNY doc dfyconfig.toml --output docs/dafny/dafny-doc/ echo Generating Java documentation... -$DAFNY translate java src/Dafny-VMC.dfy --no-verify -cp $DAFNYSOURCE/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/*.java src/Dafny-VMC-java/dafny/ -javadoc -d docs/java/java-doc/ -sourcepath src/Dafny-VMC-java -package DafnyVMC +dafny translate java src/interop/java/Full/CustomRandom.java src/interop/java/Full/Random.java dfyconfig.toml -o src/DafnyVMC --no-verify --include-runtime +mkdir src/DafnyVMC-java/DafnyVMC +cp src/interop/java/Full/CustomRandom.java src/DafnyVMC-java/DafnyVMC +cp src/interop/java/Full/Random.java src/DafnyVMC-java/DafnyVMC +find src/DafnyVMC-java/ -type f -name "*.java" | xargs javadoc -d docs/java/java-doc/ + +echo Generating Python documentation... +export TARGET_LANG=py +bash scripts/build.sh +PYTHONPATH=.:build/py/DafnyVMC-py pydoc3 -w build/py/DafnyVMC-py/DafnyVMC.py +mkdir docs/py/py-doc +mv DafnyVMC.html docs/py/py-doc \ No newline at end of file diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy index 1ae97e26..36392373 100644 --- a/src/Distributions/Uniform/Model.dfy +++ b/src/Distributions/Uniform/Model.dfy @@ -15,7 +15,6 @@ module Uniform.Model { Definitions ************/ - // Definition 49 ghost function {:axiom} Sample(n: nat): (h: Monad.Hurd) requires n > 0 ensures Independence.IsIndepFunction(h) diff --git a/src/Math/Analysis/Reals.dfy b/src/Math/Analysis/Reals.dfy index 44363353..e9a6fa00 100644 --- a/src/Math/Analysis/Reals.dfy +++ b/src/Math/Analysis/Reals.dfy @@ -3,11 +3,6 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -// Fundamental properties of the real numbers. -// * States the completeness of the reals in terms of a variation of Dedekind cuts. -// Dafny should include such an axiom, but doesn't. -// See: https://en.wikipedia.org/wiki/Completeness_of_the_real_numbers -// * Proves existence and uniqueness of infima and suprema module Reals { import RealArith diff --git a/src/Math/Helper.dfy b/src/Math/Helper.dfy index 3acd5378..2935f581 100644 --- a/src/Math/Helper.dfy +++ b/src/Math/Helper.dfy @@ -4,6 +4,7 @@ *******************************************************************************/ module Helper { + /************ Definitions ************/ diff --git a/src/ProbabilisticProgramming/Monad.dfy b/src/ProbabilisticProgramming/Monad.dfy index 715459af..96923f51 100644 --- a/src/ProbabilisticProgramming/Monad.dfy +++ b/src/ProbabilisticProgramming/Monad.dfy @@ -16,8 +16,7 @@ module Monad { type Hurd = Rand.Bitstream -> Result // The result of a probabilistic computation on a bitstream. - // It either consists of the computed value and the (unconsumed) rest of the bitstream or indicates nontermination. - // It differs from Hurd's definition in that the result can be nontermination, which Hurd does not model explicitly. + // It consists of the computed value and the (unconsumed) rest of the bitstream. datatype Result = Result(value: A, rest: Rand.Bitstream) { function Map(f: A -> B): Result {