Merge branch 'main' into fabian

dafny-lang · Sep 29, 2023 · d6a358b · d6a358b
2 parents 434c932 + beca2ef
commit d6a358b
Show file tree

Hide file tree

Showing 36 changed files with 172 additions and 178 deletions.
diff --git a/src/Distributions/Base/Interface.dfy b/src/Distributions/Base/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
 include "Model.dfy"

diff --git a/src/Distributions/Base/Model.dfy b/src/Distributions/Base/Model.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
 include "../../ProbabilisticProgramming/Monad.dfy"

diff --git a/src/Distributions/Bernoulli/Correctness.dfy b/src/Distributions/Bernoulli/Correctness.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../Math/MeasureTheory.dfy"
 include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
@@ -13,7 +13,7 @@ module BernoulliCorrectness {
   import RandomNumberGenerator
   import Independence
   import BernoulliModel
-  
+
   /*******
    Lemmas
   *******/

diff --git a/src/Distributions/Bernoulli/Implementation.dfy b/src/Distributions/Bernoulli/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../Math/MeasureTheory.dfy"
 include "Interface.dfy"

diff --git a/src/Distributions/Bernoulli/Interface.dfy b/src/Distributions/Bernoulli/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Base/Interface.dfy"
 include "Model.dfy"

diff --git a/src/Distributions/Bernoulli/Model.dfy b/src/Distributions/Bernoulli/Model.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../Math/MeasureTheory.dfy"
 include "../../ProbabilisticProgramming/Monad.dfy"
@@ -16,15 +16,9 @@ module BernoulliModel {
     var f :=
       (b: bool) =>
         if b then
-          if p <= 0.5 then
-            Monad.Return(false)
-          else
-            ProbBernoulli(2.0 * p - 1.0)
+          (if p <= 0.5 then Monad.Return(false) else ProbBernoulli(2.0 * p - 1.0))
         else
-          if p <= 0.5 then
-            ProbBernoulli(2.0 * p)
-          else
-            Monad.Return(true);
+          (if p <= 0.5 then ProbBernoulli(2.0 * p) else Monad.Return(true));
     Monad.Bind(Monad.Deconstruct, f)
   }
 }
diff --git a/src/Distributions/BernoulliExpNeg/Implementation.dfy b/src/Distributions/BernoulliExpNeg/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Bernoulli/Interface.dfy"
 include "Interface.dfy"

diff --git a/src/Distributions/BernoulliExpNeg/Interface.dfy b/src/Distributions/BernoulliExpNeg/Interface.dfy
@@ -1,13 +1,13 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Bernoulli/Interface.dfy"
 
 module BernoulliExpNegInterface {
   import BernoulliInterface
-  
+
   trait {:termination false} IBernoulliExpNeg extends BernoulliInterface.IBernoulli {
 
     method BernoulliExpNeg(gamma: real) returns (c: bool)

diff --git a/src/Distributions/BernoulliRational/Correctness.dfy b/src/Distributions/BernoulliRational/Correctness.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../Math/MeasureTheory.dfy"
 include "../../Math/Helper.dfy"

diff --git a/src/Distributions/BernoulliRational/Implementation.dfy b/src/Distributions/BernoulliRational/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "Interface.dfy"
 include "Model.dfy"
@@ -12,7 +12,7 @@ module BernoulliRationalImplementation {
 
   trait {:termination false} TBernoulliRational extends BernoulliRationalInterface.IBernoulliRational {
 
-   method BernoulliRational(m: nat, n: nat) returns (c: bool)
+    method BernoulliRational(m: nat, n: nat) returns (c: bool)
       modifies this
       decreases *
       requires n != 0

diff --git a/src/Distributions/BernoulliRational/Interface.dfy b/src/Distributions/BernoulliRational/Interface.dfy
@@ -1,15 +1,15 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Uniform/Interface.dfy"
 include "Model.dfy"
 
 module BernoulliRationalInterface {
   import UniformInterface
   import BernoulliRationalModel
-  
+
   trait {:termination false} IBernoulliRational extends UniformInterface.IUniform {
 
     method BernoulliRational(m: nat, n: nat) returns (c: bool)

diff --git a/src/Distributions/BernoulliRational/Model.dfy b/src/Distributions/BernoulliRational/Model.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Uniform/Model.dfy"
 include "../../ProbabilisticProgramming/Monad.dfy"

diff --git a/src/Distributions/DiscreteGaussian/Implementation.dfy b/src/Distributions/DiscreteGaussian/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "Interface.dfy"
 

diff --git a/src/Distributions/DiscreteGaussian/Interface.dfy b/src/Distributions/DiscreteGaussian/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../BernoulliExpNeg/Interface.dfy"
 include "../DiscreteLaplace/Interface.dfy"

diff --git a/src/Distributions/DiscreteLaplace/Implementation.dfy b/src/Distributions/DiscreteLaplace/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "Interface.dfy"
 

diff --git a/src/Distributions/DiscreteLaplace/Interface.dfy b/src/Distributions/DiscreteLaplace/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Bernoulli/Interface.dfy"
 include "../Uniform/Interface.dfy"

diff --git a/src/Distributions/Geometric/Correctness.dfy b/src/Distributions/Geometric/Correctness.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../Math/Helper.dfy"
 include "../../ProbabilisticProgramming/Monad.dfy"
@@ -20,7 +20,7 @@ module GeometricCorrectness {
   /*******
    Lemmas
   *******/
-  
+
   // Equation (4.19)
   lemma {:axiom} ProbGeometricIsIndepFn()
     ensures Independence.IsIndepFn(GeometricModel.ProbGeometric())

diff --git a/src/Distributions/Geometric/Implementation.dfy b/src/Distributions/Geometric/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/Monad.dfy"
 include "Interface.dfy"

diff --git a/src/Distributions/Geometric/Interface.dfy b/src/Distributions/Geometric/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/Monad.dfy"
 include "../Base/Interface.dfy"

diff --git a/src/Distributions/Geometric/Model.dfy b/src/Distributions/Geometric/Model.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/Monad.dfy"
 include "../../ProbabilisticProgramming/WhileAndUntil.dfy"
@@ -19,7 +19,7 @@ module GeometricModel {
     Monad.Bind(g, f)
   }
 
-    // Equation (4.17)
+  // Equation (4.17)
   function ProbGeometricIter(t: (bool, int)): (f: Monad.Hurd<(bool, int)>)
     ensures forall s :: f(s) == ((Monad.Head(s), t.1 + 1), Monad.Tail(s))
   {

diff --git a/src/Distributions/Uniform/Implementation.dfy b/src/Distributions/Uniform/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../UniformPowerOfTwo/Interface.dfy"
 include "../UniformPowerOfTwo/Implementation.dfy"

diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Base/Interface.dfy"
 include "../UniformPowerOfTwo/Interface.dfy"

diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
 include "../../ProbabilisticProgramming/Monad.dfy"