Skip to content

Commit

Permalink
remove changes to uniform interface
Browse files Browse the repository at this point in the history
  • Loading branch information
stefan-aws committed Feb 21, 2024
1 parent 5280e7d commit 8fb80e3
Showing 1 changed file with 9 additions and 9 deletions.
18 changes: 9 additions & 9 deletions src/Distributions/Uniform/Interface.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -4,33 +4,33 @@
*******************************************************************************/

module Uniform.Interface {
import UniformPowerOfTwo
import Monad
import Coin
import Model
import UniformPowerOfTwo
import Pos

trait {:termination false} Trait extends UniformPowerOfTwo.Interface.Trait {

method UniformSample(n: Pos.pos) returns (o: nat)
method UniformSample(n: Pos.pos) returns (u: nat)
modifies `s
decreases *
requires n > 0
ensures o < n
ensures Model.Sample(n)(old(s)) == Monad.Result(o, s)
ensures u < n
ensures Model.Sample(n)(old(s)) == Monad.Result(u, s)

method UniformIntervalSample(a: int, b: int) returns (o: int)
method UniformIntervalSample(a: int, b: int) returns (u: int)
modifies `s
decreases *
requires a < b
ensures a <= o < b
ensures Model.IntervalSample(a, b)(old(s)) == Monad.Result(o, s)
ensures a <= u < b
ensures Model.IntervalSample(a, b)(old(s)) == Monad.Result(u, s)
{
var v := UniformSample(b - a);
assert Model.Sample(b-a)(old(s)) == Monad.Result(v, s);
assert Model.IntervalSample(a, b)(old(s)) == Monad.Result(a + v, s);
o := a + v;
u := a + v;
}

}
}
}

0 comments on commit 8fb80e3

Please sign in to comment.