How to define exponential and log function for real variables in Dafny?

Question

I have been trying to use Dafny for verification of some algorithms. In some parts, the calculation needs exponential and log functions, but Dafny does not offer any libaries or built-in math functions. I checked some other verification codes, for exponential function, they simulated it with multiply operations, like the following:

function power (n: nat) : nat
{
  if n == 0 then 1
            else 2 * power(n-1)
}

This works only for natural numbers, but I need something like this

function power (n: real, alpha: real) : real
  requires alpha > 0.0
{
    // something to implement this funciton and calculate alpha^{n}
}

and this

function log (n: real, alpha: real) : real
  requires alpha > 0.0 && n > 0.0
{
    // something here to calculate log_{alpha}(n)
}

also, this lemma needs to be ensured

lemma consistency (n: real, alpha: real)
  requires n > 0.0 && alpha > 0.0
  requires log(power(n,alpha),alpha) == n
  requires power(log(n,alpha),alpha) == n
{
}

any ideas?

well-defined dafny functions to implement exponential and log function for real variables

Answer 1

There is a library method available for integer powers and logarithms. However, for real numbers I suspect verifying these transcendental functions is quite difficult. Probably you would need to develop a theory of limits in Dafny, which is definitely non-trivial.

Actually calculating a logarithm in Dafny would be hard. However, if all you need is the functions and the properties of logrithms and power you can define them with ghost functions and axioms. This will allow you to verify lemmas about them.

ghost function power(n: real, alpha: real): real
    requires n > 0.0 && alpha > 0.0

ghost function log(n: real, alpha: real): real
    requires n > 0.0 && alpha > 0

lemma consistency(n: real, alpha: real)
    requires n > 0.0 && alpha > 0.0
    ensures log(power(n, alpha), alpha) == n
    ensures power(log(n, alpha), alpha) == n

lemma logarithmSum(n: real, alpha: real, x: real, y: real)
    requires n > 0.0 && alpha > 0.0
    requires x > 0.0
    requires n == x * y
    ensures log(n, alpha) == log(x, alpha) +  log(y, alpha)

lemma test() {
    var pow3 := power(3.0, 4.0);
    consistency(3.0,4.0);
    assert log(pow3, 3.0) == 4.0;

    var log6 := log(6.0, 8.0);
    logarithmSum(6.0, 8.0, 2.0, 3.0);
    assert log6 == log(2.0, 8.0)+log(3.0, 8.0);
}

When you leave off the body of a lemma, that is how you assert to dafny that something is an axiom and when you call the lemma with instantiated values it will verify the property.

Practically speaking, how you might be able to use this is when you define a certain method you would have some variables which calculated as power or logarithms and then you would write more lemmas or possibly other axioms that ensure that the algorithm/method loop invariants maintain the relationship of the power/logarithm.

lemma powerLemma(n: real, alpha: real)
    requires n > 0.0 && alpha > 0.0
    ensures power(n, alpha) * alpha == power(n+1.0, alpha)

lemma test2() {
    var pow3 := power(3.0, 4.0);
    var power4 := power(4.0, 4.0);
    powerLemma(3.0, 4.0);
    assert pow3 * 4.0 == power4;
}

However, you will probably run into an issue or two trying to use the ghost functions in a method since they aren't actually calculable. Again, you'll have to start with real values, and use axioms/lemmas to assert that they are equivalent to some power or logarithm.

lemma power1(alpha: real)
    requires alpha > 0.0
    ensures power(1.0, alpha) == alpha

method pow(n: nat, alpha: real) returns (product: real)
    requires n > 0
    requires alpha > 0.0
    ensures product == power(n as real, alpha)
{
    product := alpha;
    var i: nat := 1;
    power1(alpha);
    assert product == power(1.0, alpha);
    while i < n
        invariant i <= n
        invariant product == power(i as real, alpha)
    {
        powerLemma(i as real, alpha);
        product := product * alpha;
        i := i + 1;
    }
    assert i == n;
    assert product == power(n as real, alpha);
}