Add a Random module to the dafny library

[markrtuttle]

Overview

The Dafny.Random module provides a uniform interface to random values across target languages.

    // Return an arbitrary boolean value
    predicate nextBool()

    // Return an arbitrary integer value in the range [0, bound)
    function nextInt(bound: int := 0): (value: int)
        ensures 0 <= value
        ensures bound > 0 ==> value < bound

    // Return an arbitrary real value in the range [0,1)
     function nextReal(): (value: real)
        ensures 0.0 <= value < 1.0

To see the need for a uniform interface to probability, C# provides random integer values and Java and JavaScript provide random real values, and Dafny actually models real numbers as rationals with integral numerators and denominators of arbitrary size. This module gives one interface to these various sources of randomness. This is a simple interface to probability. For a more sophisticated treatment of probability, see the Verified Monte Carlo (VMC) library.

The Dafny.Random module also provides a uniform interface to nondeterminism and probability. For example, nextInt(10) returns an arbitrary integer from [0,10), but

• in a proof context, the integer is chosen nondeterministcally, and
• in a compiled code context, the integer is chose probabilistically according to the uniform probability distribution.

Compare this with the Dafny construct var value: int := *; where value is arbitrary in a proof context and constant (typically 0) in compiled code.

Usage

The Random module, like FileIO will not compile or run correctly without a language-specific implementation file. Implementations are currently provided for C#, Java, and JavaScript. To use Random in your code, you must:

• include and import the Random module as you would any other library module
• incorporate the corresponding language-specific implementation file (e.g. Random.cs) when building or running your program

The example random.dfy in the examples directory shows how to use the module. From the examples directory, compile and run the file random.dfy with

# C#
$ dafny run random.dfy --target cs --input ../../src/Random/Random.cs -- --verbose

# Java
$ dafny run random.dfy --target java --input ../../src/Random/Random.java -- --verbose

# JavaScript
$ dafny run random.dfy --target js --input ../../src/Random/Random.js -- --verbose

[fzaiser]

General comment on using floating point random numbers: One has to be very careful if using random floating point numbers because FP numbers have a higher resolution closer to zero, which could potentially skew the distribution. Ideally one would use library functions that directly return a random integer without going through floating point. There's a lot of subtleties that are easy to get wrong here, see the last paragraph of https://en.wikipedia.org/wiki/Fisher%E2%80%93Yates_shuffle#Modulo_bias as an example. The whole article contains a nice list of things that can go wrong if one is not very careful around randomness.

[codyroux]

I'd feel remiss not to add: https://xkcd.com/221/