Mora - Automatic Generation of Moment-Based Invariants
493
x=0
while true:
u = RV(uniform, 0, b)
g = RV(gauss, 0, 1)
x = x - u @ 1/2; x + u @ 1/2
y = y + x + g
Loop conditions are ignored, yielding
non-deterministic PPs. The value of
the random variable u is sampled by
a uniform distribution with support in
the real interval [0, b], whereas the
value of g is a random number from a
normal distribution with mean (first
moment) 0 and variance (second moment) 1. Updates to variable x are probabilistic: with
probability 1/2, the variable x is updated by x-u. Similarly, with probability 1/2, x is
updated by x+u. Further, updates to u and g do not depend on other variables; the update
to x depends only on itself and u.
Fig. 1. An illustrative example of a Prob-solvable loop.
Moreover, the invariants inferred by MORA are not restricted to expected values
but are quantitative invariants over the higher-order moments of program variables. We
refer to such invariants as moment-based invariants [2]. To the best of our knowledge,
no other approach can so far automatically compute higher-order moments of PPs, not
even for the restricted yet expressive enough class of Prob-solvable loop.
The purpose of this paper is to describe what MORA can do and how it can be used.
The paper is intended as a tool demonstration and guide for potential users of MORA.
We focus on the usage and implementation aspects of MORA. For details on theoretical
foundations and algorithmic aspects of MORA for computing moment-based invariants,
we refer to [2]. We note however that, when compared to the experimental setup of [2],
MORA comes with a completely new design, fully implemented in python and supporting an easy installation and use by even non-experts in PPs.
2 MORA– Programming Model
Input programs to MORA are PP loops that are Prob-solvable [2]. In Figure 1, we give
an example of a Prob-solvable loop and use this example as a running example to guide
the potential users of MORA in the rest of this paper.
In a nutshell, the probabilistic assignments of Prob-solvable loops involve (i) variable values drawn from random distributions, such as uniform or normal distributions,
and (ii) random variable updates. In the sequel, we write RV to refer to a random variable. Input programs to MORA thus satisfy the following two properties:
(1) Input programs to MORA are PPs generated from the grammar in Figure 2.
(2) In addition to the grammar of Figure 2, MORA requires its PP input to be Probsolvable, imposing further restrictions as follows:
– PP loop variables are different from each other and from parameters;
– probabilities used within a variable update sum up to 1;
– updated variables depend on themselves linearly and may depend polynomially
only on other variables that have been previously updated.
Note that Figure 1 satisfies all constraints above, and thus is Prob-solvable.
493
x=0
while true:
u = RV(uniform, 0, b)
g = RV(gauss, 0, 1)
x = x - u @ 1/2; x + u @ 1/2
y = y + x + g
Loop conditions are ignored, yielding
non-deterministic PPs. The value of
the random variable u is sampled by
a uniform distribution with support in
the real interval [0, b], whereas the
value of g is a random number from a
normal distribution with mean (first
moment) 0 and variance (second moment) 1. Updates to variable x are probabilistic: with
probability 1/2, the variable x is updated by x-u. Similarly, with probability 1/2, x is
updated by x+u. Further, updates to u and g do not depend on other variables; the update
to x depends only on itself and u.
Fig. 1. An illustrative example of a Prob-solvable loop.
Moreover, the invariants inferred by MORA are not restricted to expected values
but are quantitative invariants over the higher-order moments of program variables. We
refer to such invariants as moment-based invariants [2]. To the best of our knowledge,
no other approach can so far automatically compute higher-order moments of PPs, not
even for the restricted yet expressive enough class of Prob-solvable loop.
The purpose of this paper is to describe what MORA can do and how it can be used.
The paper is intended as a tool demonstration and guide for potential users of MORA.
We focus on the usage and implementation aspects of MORA. For details on theoretical
foundations and algorithmic aspects of MORA for computing moment-based invariants,
we refer to [2]. We note however that, when compared to the experimental setup of [2],
MORA comes with a completely new design, fully implemented in python and supporting an easy installation and use by even non-experts in PPs.
2 MORA– Programming Model
Input programs to MORA are PP loops that are Prob-solvable [2]. In Figure 1, we give
an example of a Prob-solvable loop and use this example as a running example to guide
the potential users of MORA in the rest of this paper.
In a nutshell, the probabilistic assignments of Prob-solvable loops involve (i) variable values drawn from random distributions, such as uniform or normal distributions,
and (ii) random variable updates. In the sequel, we write RV to refer to a random variable. Input programs to MORA thus satisfy the following two properties:
(1) Input programs to MORA are PPs generated from the grammar in Figure 2.
(2) In addition to the grammar of Figure 2, MORA requires its PP input to be Probsolvable, imposing further restrictions as follows:
– PP loop variables are different from each other and from parameters;
– probabilities used within a variable update sum up to 1;
– updated variables depend on themselves linearly and may depend polynomially
only on other variables that have been previously updated.
Note that Figure 1 satisfies all constraints above, and thus is Prob-solvable.