From 5efab50c8aef79e03be2f7d2929b42b6ca0c8f49 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Fri, 13 Oct 2023 14:52:02 -0400 Subject: [PATCH] Use camelCase instead of snake_case for locals --- src/Distributions/Uniform/Implementation.dfy | 8 ++--- .../UniformPowerOfTwo/Correctness.dfy | 34 +++++++++---------- src/Math/Analysis/Limits.dfy | 22 ++++++------ src/Math/Measures.dfy | 10 +++--- src/Math/Rationals.dfy | 8 ++--- 5 files changed, 41 insertions(+), 41 deletions(-) diff --git a/src/Distributions/Uniform/Implementation.dfy b/src/Distributions/Uniform/Implementation.dfy index 5ea2f59b..e73cd627 100644 --- a/src/Distributions/Uniform/Implementation.dfy +++ b/src/Distributions/Uniform/Implementation.dfy @@ -16,14 +16,14 @@ module Uniform.Implementation { ensures u < n ensures Model.Sample(n)(old(s)) == (u, s) { - ghost var prev_s := s; + ghost var prevS := s; u := UniformPowerOfTwoSample(2 * n); while u >= n decreases * - invariant Model.Sample(n)(old(s)) == Model.Sample(n)(prev_s) - invariant (u, s) == Model.Proposal(n)(prev_s) + invariant Model.Sample(n)(old(s)) == Model.Sample(n)(prevS) + invariant (u, s) == Model.Proposal(n)(prevS) { - prev_s := s; + prevS := s; u := UniformPowerOfTwoSample(2 * n); } } diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy index 8a51a428..58905dc1 100644 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy @@ -271,13 +271,13 @@ module UniformPowerOfTwo.Correctness { lemma SampleSetEquality(n: nat, m: nat) requires n >= 2 ensures - var b_of := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0; - var a_of := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0; - (iset s | Model.Sample(n)(s).0 == m) == (iset s | 2*a_of(s) + Helper.boolToNat(b_of(s)) == m) + var bOf := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0; + var aOf := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0; + (iset s | Model.Sample(n)(s).0 == m) == (iset s | 2*aOf(s) + Helper.boolToNat(bOf(s)) == m) { - var b_of := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0; - var a_of := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0; - forall s ensures Model.Sample(n)(s).0 == m <==> (2 * a_of(s) + Helper.boolToNat(b_of(s)) == m) { + var bOf := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0; + var aOf := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0; + forall s ensures Model.Sample(n)(s).0 == m <==> (2 * aOf(s) + Helper.boolToNat(bOf(s)) == m) { var (a, s') := Model.Sample(n / 2)(s); var (b, s'') := Monad.Coin(s'); calc { @@ -300,20 +300,20 @@ module UniformPowerOfTwo.Correctness { requires n >= 2 ensures Random.Prob(iset s | Model.Sample(n)(s).0 == m) == Random.Prob(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0 { - var a_of: Random.Bitstream -> nat := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0; - var b_of: Random.Bitstream -> bool := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0; + var aOf: Random.Bitstream -> nat := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0; + var bOf: Random.Bitstream -> bool := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0; var A: iset := (iset x: nat | x == m / 2); var E: iset := (iset s | m % 2 as nat == Helper.boolToNat(Monad.Coin(s).0)); var f := (s: Random.Bitstream) => Model.Sample(n / 2)(s).1; var e1 := (iset s | Model.Sample(n / 2)(s).1 in E); var e2 := (iset s | Model.Sample(n / 2)(s).0 in A); - var e3 := (iset s | 2*a_of(s) + Helper.boolToNat(b_of(s)) == m); + var e3 := (iset s | 2*aOf(s) + Helper.boolToNat(bOf(s)) == m); assert SplitEvent: e3 == e1 * e2 by { forall s ensures s in e3 <==> s in e1 && s in e2 { - var a: nat := a_of(s); - var b: nat := Helper.boolToNat(b_of(s)); + var a: nat := aOf(s); + var b: nat := Helper.boolToNat(bOf(s)); assert b < 2; calc { s in e3; @@ -325,14 +325,14 @@ module UniformPowerOfTwo.Correctness { } } - assert Eq2: (iset s | a_of(s) == m / 2) == e2 by { - forall s ensures a_of(s) == m / 2 <==> Model.Sample(n / 2)(s).0 in A { + assert Eq2: (iset s | aOf(s) == m / 2) == e2 by { + forall s ensures aOf(s) == m / 2 <==> Model.Sample(n / 2)(s).0 in A { } } - assert Eq3: (iset s | a_of(s) == m / 2) == (iset s | Model.Sample(n / 2)(s).0 == m / 2) by { - forall s ensures a_of(s) == m / 2 <==> Model.Sample(n / 2)(s).0 == m / 2 { - assert a_of(s) == Model.Sample(n / 2)(s).0; + assert Eq3: (iset s | aOf(s) == m / 2) == (iset s | Model.Sample(n / 2)(s).0 == m / 2) by { + forall s ensures aOf(s) == m / 2 <==> Model.Sample(n / 2)(s).0 == m / 2 { + assert aOf(s) == Model.Sample(n / 2)(s).0; } } @@ -385,7 +385,7 @@ module UniformPowerOfTwo.Correctness { == Random.Prob(e2) / 2.0; == { reveal Eq2; } - Random.Prob(iset s | a_of(s) == m / 2) / 2.0; + Random.Prob(iset s | aOf(s) == m / 2) / 2.0; == { reveal Eq3; } Random.Prob(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0; } diff --git a/src/Math/Analysis/Limits.dfy b/src/Math/Analysis/Limits.dfy index 8c542619..8a2fe15d 100644 --- a/src/Math/Analysis/Limits.dfy +++ b/src/Math/Analysis/Limits.dfy @@ -228,20 +228,20 @@ module Limits { } } - lemma LimitOfMultiplicationWithZeroSequence(sequence: nat -> real, bound: real, zero_seq: nat -> real) + lemma LimitOfMultiplicationWithZeroSequence(sequence: nat -> real, bound: real, zeroSeq: nat -> real) requires Sequences.IsBounded(sequence, bound) - requires ConvergesTo(zero_seq, 0.0) - ensures ConvergesTo(Sequences.Mul(sequence, zero_seq), 0.0) + requires ConvergesTo(zeroSeq, 0.0) + ensures ConvergesTo(Sequences.Mul(sequence, zeroSeq), 0.0) { - var productSequence := Sequences.Mul(sequence, zero_seq); + var productSequence := Sequences.Mul(sequence, zeroSeq); forall epsilon: real | epsilon > 0.0 ensures ExistsCloseSuffix(productSequence, 0.0, epsilon) { var epsilon' := epsilon / Reals.Max(bound, 1.0); - assert ExistsCloseSuffix(zero_seq, 0.0, epsilon'); - var N :| SuffixIsClose(zero_seq, 0.0, epsilon', N); + assert ExistsCloseSuffix(zeroSeq, 0.0, epsilon'); + var N :| SuffixIsClose(zeroSeq, 0.0, epsilon', N); assert SuffixIsClose(productSequence, 0.0, epsilon, N) by { forall n: nat | n >= N ensures Reals.Dist(productSequence(n), 0.0) < epsilon { var s := sequence(n); - var z := zero_seq(n); + var z := zeroSeq(n); calc { Reals.Dist(productSequence(n), 0.0); == @@ -364,8 +364,8 @@ module Limits { ensures ConvergesTo(Sequences.OneOverNPlus1, 0.0) { forall epsilon: real | epsilon > 0.0 ensures ExistsCloseSuffix(Sequences.OneOverNPlus1, 0.0, epsilon) { - var epsilon_inv := 1.0 / epsilon; - var N := epsilon_inv.Floor; + var epsilonInv := 1.0 / epsilon; + var N := epsilonInv.Floor; assert SuffixIsClose(Sequences.OneOverNPlus1, 0.0, epsilon, N) by { forall n: nat ensures n >= N ==> Reals.Dist(Sequences.OneOverNPlus1(n), 0.0) < epsilon { assert Sequences.OneOverNPlus1(n) > 0.0; @@ -377,8 +377,8 @@ module Limits { Sequences.OneOverNPlus1(N); == 1.0 / (N + 1) as real; - < { Reals.DivisionIsAntiMonotonicStrict(1.0, (N + 1) as real, epsilon_inv); } - 1.0 / epsilon_inv; + < { Reals.DivisionIsAntiMonotonicStrict(1.0, (N + 1) as real, epsilonInv); } + 1.0 / epsilonInv; == epsilon; } diff --git a/src/Math/Measures.dfy b/src/Math/Measures.dfy index c9b213bc..de0a0133 100644 --- a/src/Math/Measures.dfy +++ b/src/Math/Measures.dfy @@ -63,14 +63,14 @@ module Measures { } // Definition 9 - ghost predicate IsMeasurable(event_space_s: iset>, event_space_t: iset>, f: S -> T) { - forall e | e in event_space_t :: PreImage(f, e) in event_space_s + ghost predicate IsMeasurable(eventSpaceS: iset>, eventSpaceT: iset>, f: S -> T) { + forall e | e in eventSpaceT :: PreImage(f, e) in eventSpaceS } // Definition 10 - ghost predicate IsMeasurePreserving(event_space_s: iset>, mu_s: iset -> real, event_space_t: iset>, mu_t: iset -> real, f: S -> T) { - && IsMeasurable(event_space_s, event_space_t, f) - && forall e | e in event_space_t :: mu_s(PreImage(f, e)) == mu_t(e) + ghost predicate IsMeasurePreserving(eventSpaceS: iset>, measureS: iset -> real, eventSpaceT: iset>, measureT: iset -> real, f: S -> T) { + && IsMeasurable(eventSpaceS, eventSpaceT, f) + && forall e | e in eventSpaceT :: measureS(PreImage(f, e)) == measureT(e) } // Definition 12 diff --git a/src/Math/Rationals.dfy b/src/Math/Rationals.dfy index eeed13e6..a1ef2669 100644 --- a/src/Math/Rationals.dfy +++ b/src/Math/Rationals.dfy @@ -121,16 +121,16 @@ module Rationals { var floor := r.numer / r.denom; var multiple := floor * r.denom; assert r.numer == multiple + r.numer % r.denom; - var next_multiple := multiple + r.denom; + var nextMultiple := multiple + r.denom; assert Floor(r) as real <= ToReal(r); assert ToReal(r) < Floor(r) as real + 1.0 by { - assert r.numer < next_multiple; + assert r.numer < nextMultiple; calc { ToReal(r); == r.numer as real / r.denom as real; - < { DivStrictlyMonotonic(r.denom as real, r.numer as real, next_multiple as real); } - next_multiple as real / r.denom as real; + < { DivStrictlyMonotonic(r.denom as real, r.numer as real, nextMultiple as real); } + nextMultiple as real / r.denom as real; == (floor + 1) as real; ==