From 4bb490d2d33bcfb676c2dd79348dabd7d7de20d8 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 20 Mar 2024 14:47:18 +0000 Subject: [PATCH 1/4] fix tests --- tests/Tests.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/Tests.dfy b/tests/Tests.dfy index cfd6a0b0..a8b42e70 100644 --- a/tests/Tests.dfy +++ b/tests/Tests.dfy @@ -31,14 +31,14 @@ module Tests { { var empiricalMean := empiricalSum / n as real; var diff := RealArith.Abs(empiricalMean - trueMean); - var threshold := 3.0 * 3.0 * trueVariance; - if diff * diff > threshold { + var threshold := 4.0 * 4.0 * trueVariance / n as real; + if diff * diff >= threshold { print "Test failed: ", description, "\n"; print "True mean: ", trueMean, "\n"; print "Empirical mean: ", empiricalMean, "\n"; print "Difference between empirical and true mean: ", diff, "\n"; print "squared difference: ", diff * diff, "\n"; - print "sigma squared: ", trueVariance, "\n"; + print "sigma squared: ", trueVariance / n as real, "\n"; } expect diff * diff <= threshold, "Empirical mean should be within 3 sigma of true mean. This individual test may fail with probability of about 6.3e-5."; } From ef05f90443401dab7a503674c0ff1ded16bdbc27 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 20 Mar 2024 14:53:26 +0000 Subject: [PATCH 2/4] typo --- tests/Tests.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/Tests.dfy b/tests/Tests.dfy index a8b42e70..c681af57 100644 --- a/tests/Tests.dfy +++ b/tests/Tests.dfy @@ -40,7 +40,7 @@ module Tests { print "squared difference: ", diff * diff, "\n"; print "sigma squared: ", trueVariance / n as real, "\n"; } - expect diff * diff <= threshold, "Empirical mean should be within 3 sigma of true mean. This individual test may fail with probability of about 6.3e-5."; + expect diff * diff < threshold, "Empirical mean should be within 3 sigma of true mean. This individual test may fail with probability of about 6.3e-5."; } method TestUniformPowerOfTwo(n: nat, u: nat, r: DafnyVMC.Random) From 07df18f08c66b15c1a162b6a63d396c0cb74fa17 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 20 Mar 2024 14:57:27 +0000 Subject: [PATCH 3/4] revert inequality --- tests/Tests.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/Tests.dfy b/tests/Tests.dfy index c681af57..9ae4c360 100644 --- a/tests/Tests.dfy +++ b/tests/Tests.dfy @@ -32,7 +32,7 @@ module Tests { var empiricalMean := empiricalSum / n as real; var diff := RealArith.Abs(empiricalMean - trueMean); var threshold := 4.0 * 4.0 * trueVariance / n as real; - if diff * diff >= threshold { + if diff * diff > threshold { print "Test failed: ", description, "\n"; print "True mean: ", trueMean, "\n"; print "Empirical mean: ", empiricalMean, "\n"; @@ -40,7 +40,7 @@ module Tests { print "squared difference: ", diff * diff, "\n"; print "sigma squared: ", trueVariance / n as real, "\n"; } - expect diff * diff < threshold, "Empirical mean should be within 3 sigma of true mean. This individual test may fail with probability of about 6.3e-5."; + expect diff * diff <= threshold, "Empirical mean should be within 3 sigma of true mean. This individual test may fail with probability of about 6.3e-5."; } method TestUniformPowerOfTwo(n: nat, u: nat, r: DafnyVMC.Random) From e0c78d4e3808f8d409c42cac4bdc1e79caa77ede Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 20 Mar 2024 16:20:32 +0000 Subject: [PATCH 4/4] extend testing --- tests/Tests.dfy | 61 ++++++++++++------------------------------- tests/TestsRandom.dfy | 47 ++++++++++++++++++++++++++++----- 2 files changed, 58 insertions(+), 50 deletions(-) diff --git a/tests/Tests.dfy b/tests/Tests.dfy index 9ae4c360..4634032e 100644 --- a/tests/Tests.dfy +++ b/tests/Tests.dfy @@ -8,6 +8,7 @@ module Tests { import RealArith import Helper import DafnyVMC + import opened Pos method TestBernoulliIsWithin3SigmaOfTrueMean( n: nat, @@ -119,70 +120,42 @@ module Tests { TestEmpiricalIsWithin3SigmaOfTrueMean(n, sum as real, (u - 1) as real / 2.0, (u * u - 1) as real / 12.0, "mean of Uniform(" + Helper.NatToString(u) + ")"); } - method TestUniformInterval(n: nat, r: DafnyVMC.Random) + method TestUniformInterval(n: nat, a: int, b: int, r: DafnyVMC.Random) decreases * requires n > 0 + requires a < b modifies r { - var a := 0; - var b := 0; - var c := 0; + var u := b-a; + var arr := new nat[u](i => 0); for i := 0 to n { - var k := r.UniformIntervalSample(7,10); - match k { - case 7 => a := a + 1; - case 8 => b := b + 1; - case 9 => c := c + 1; - } + var l := r.UniformIntervalSample(a, b); + expect a <= l < b, "sample not in the right bound"; + var k := l-a; + assert 0 <= k < u; + arr[k] := arr[k] + 1; } - TestBernoulliIsWithin3SigmaOfTrueMean(n, a as real, 1.0 / 3.0, "p(7)"); - TestBernoulliIsWithin3SigmaOfTrueMean(n, b as real, 1.0 / 3.0, "p(8)"); - TestBernoulliIsWithin3SigmaOfTrueMean(n, c as real, 1.0 / 3.0, "p(9)"); - } - method TestBernoulli(n: nat, r: DafnyVMC.Random) - decreases * - requires n > 0 - modifies r - { - var t := 0; - for i := 0 to n { - var b := r.BernoulliSample(1, 5); - if b { - t := t + 1; - } - } - TestBernoulliIsWithin3SigmaOfTrueMean(n, t as real, 0.2, "p(true)"); - } - - method TestBernoulli2(n: nat, r: DafnyVMC.Random) - decreases * - modifies r - { - var t := 0; - for i := 0 to n { - var b := r.BernoulliSample(0, 5); - if b { - t := t + 1; - } + for i := 0 to u { + TestBernoulliIsWithin3SigmaOfTrueMean(n, arr[i] as real, 1.0 / (u as real), "p(" + Helper.NatToString(i) + ")"); } - expect t == 0; } - method TestBernoulli3(n: nat, r: DafnyVMC.Random) + method TestBernoulli(n: nat, num: nat, den: pos, r: DafnyVMC.Random) decreases * + requires n > 0 + requires num <= den modifies r { var t := 0; for i := 0 to n { - var b := r.BernoulliSample(5, 5); + var b := r.BernoulliSample(num, den); if b { t := t + 1; } } - - expect t == n; + TestBernoulliIsWithin3SigmaOfTrueMean(n, t as real, (num as real) / (den as real), "p(true)"); } method TestBernoulliExpNegLe1(n: nat, r: DafnyVMC.Random) diff --git a/tests/TestsRandom.dfy b/tests/TestsRandom.dfy index eab4340b..8fe0505e 100644 --- a/tests/TestsRandom.dfy +++ b/tests/TestsRandom.dfy @@ -53,33 +53,68 @@ module TestsRandom { Tests.TestUniformMean(100_000, NatArith.Power(10, 100), r); } + method {:test} TestUniformInterval0() + decreases * + { + var r := new DafnyVMC.Random(); + Tests.TestUniformInterval(1_000_000, 0, 1, r); + } - method {:test} TestUniformInterval() + method {:test} TestUniformInterval1() decreases * { var r := new DafnyVMC.Random(); - Tests.TestUniformInterval(1_000_000, r); + Tests.TestUniformInterval(1_000_000, -5, 5, r); } - method {:test} TestBernoulli() + method {:test} TestUniformInterval2() decreases * { var r := new DafnyVMC.Random(); - Tests.TestBernoulli(1_000_000, r); + Tests.TestUniformInterval(1_000_000, -15, 15, r); + } + + method {:test} TestUniformInterval3() + decreases * + { + var r := new DafnyVMC.Random(); + Tests.TestUniformInterval(1_000_000, -30, -5, r); + } + + method {:test} TestUniformInterval4() + decreases * + { + var r := new DafnyVMC.Random(); + Tests.TestUniformInterval(1_000_000, -30, 30, r); + } + + method {:test} TestBernoulli0() + decreases * + { + var r := new DafnyVMC.Random(); + Tests.TestBernoulli(1_000_000, 1, 5, r); + } + + method {:test} TestBernoulli1() + decreases * + { + var r := new DafnyVMC.Random(); + Tests.TestBernoulli(1_000_000, 0, 5, r); } method {:test} TestBernoulli2() decreases * { var r := new DafnyVMC.Random(); - Tests.TestBernoulli2(1_000_000, r); + Tests.TestBernoulli(1_000_000, 5, 5, r); } + method {:test} TestBernoulli3() decreases * { var r := new DafnyVMC.Random(); - Tests.TestBernoulli3(1_000_000, r); + Tests.TestBernoulli(1_000_000, 1, 100, r); } method {:test} TestBernoulliExpNegLe1()