494
E. Bartocci et al.
Grammar defining PP inputs to MORA
PROGRAM → INIT ASSIGNS ” w h i l e t r u e : ” RV ASSIGNS UPD ASSIGNS
INIT ASSIGNS → INIT ASSIGN | INIT ASSIGN INIT ASSIGNS
RV ASSIGNS → RV ASSIGN | RV ASSIGN RV ASSIGNS
UPD ASSIGNS → UPD ASSIGN | UPD ASSIGN UPD ASSIGNS
INIT ASSIGN → VAR ” = ” INIT EXPR
RV ASSIGN → VAR ” = ” RV EXPR
UPD ASSIGN → VAR ” = ” UPD BRANCHES
UPD BRANCHES → UPD BRANCH | UPD BRANCH UPD BRANCHES
UPD BRANCH → UPD EXPR ”@” UPD PROB
UPD PROB → SIMP EXPR
INIT EXPR → RV EXPR | SIMP EXPR
RV EXPR → ”RV( u n i f o r m , ” SIMP EXPR ” , ” SIMP EXPR ” ) ”
| ”RV( g a u s s , ” SIMP EXPR ” , ” SIMP EXPR ” ) ”
UPD EXPR → UPD EXPR OP UPD EXPR | VAR | ATOM
SIMP EXPR → SIMP EXPR OP SIMP EXPR | ATOM
ATOM → NUM | PARAMETER
OP → [∗+−]
VAR → [ a−zA−Z ] [ a−zA−Z0−9]∗
PARAMETER → [ a−zA−Z ] [ a−zA−Z0−9]∗
NUM → [ − ]?[0 − 9]+[.]?[0 − 9]∗ ([\ /][1 − 9][0 − 9]∗ )?
Fig. 2.
3 MORA– Usage
We describe the easiest way MORA can be used to generate moment-based invariants:
– Save a Prob-solvable loop to a file, for example save Figure 1 in the file running
– In the main MORA folder invoke python with python3.7 and execute:
from mora.mora import mora
– Run MORA using the command:
mora("running", goal=GOAL),
where GOAL can be (i) a specific natural number k ≥ 1, in which case MORA computes the kth moments of all variables from running; (ii) a specific moment of one
loop variable of running (e.g. "xˆ2" specifying the second moment of a variable x
of Figure 1); or (iii) a list containing the goals as just specified. One can specify finitely
many goals as inputs to MORA; yet, at least one goal is required. For example, by
running mora("running", [1, "xˆ2", "xˆ3"]), MORA computes the expected values (first moments, i.e. 1) of all variables from Figure 1, as well as the second
and third moments of variable x of Figure 1 (specified by xˆ2 and xˆ3, respectively).
MORA is completely automatic. That is, once an execution of MORA is started on
a given Prob-solvable loop and input goals, MORA outputs the higher-order moments,
and thus moment-based invariants, of its loop w.r.t. the specified input goals. To this end,
MORA computes the expected values of all monomials over loop variables, on which
one of the goals from Goal depends. In general, computing the kth moment requires
computing the expected values of all monomial expressions over loop variables, such
that the total degree of the monomials is less or equal than k – see [2] for more details.
E. Bartocci et al.
Grammar defining PP inputs to MORA
PROGRAM → INIT ASSIGNS ” w h i l e t r u e : ” RV ASSIGNS UPD ASSIGNS
INIT ASSIGNS → INIT ASSIGN | INIT ASSIGN INIT ASSIGNS
RV ASSIGNS → RV ASSIGN | RV ASSIGN RV ASSIGNS
UPD ASSIGNS → UPD ASSIGN | UPD ASSIGN UPD ASSIGNS
INIT ASSIGN → VAR ” = ” INIT EXPR
RV ASSIGN → VAR ” = ” RV EXPR
UPD ASSIGN → VAR ” = ” UPD BRANCHES
UPD BRANCHES → UPD BRANCH | UPD BRANCH UPD BRANCHES
UPD BRANCH → UPD EXPR ”@” UPD PROB
UPD PROB → SIMP EXPR
INIT EXPR → RV EXPR | SIMP EXPR
RV EXPR → ”RV( u n i f o r m , ” SIMP EXPR ” , ” SIMP EXPR ” ) ”
| ”RV( g a u s s , ” SIMP EXPR ” , ” SIMP EXPR ” ) ”
UPD EXPR → UPD EXPR OP UPD EXPR | VAR | ATOM
SIMP EXPR → SIMP EXPR OP SIMP EXPR | ATOM
ATOM → NUM | PARAMETER
OP → [∗+−]
VAR → [ a−zA−Z ] [ a−zA−Z0−9]∗
PARAMETER → [ a−zA−Z ] [ a−zA−Z0−9]∗
NUM → [ − ]?[0 − 9]+[.]?[0 − 9]∗ ([\ /][1 − 9][0 − 9]∗ )?
Fig. 2.
3 MORA– Usage
We describe the easiest way MORA can be used to generate moment-based invariants:
– Save a Prob-solvable loop to a file, for example save Figure 1 in the file running
– In the main MORA folder invoke python with python3.7 and execute:
from mora.mora import mora
– Run MORA using the command:
mora("running", goal=GOAL),
where GOAL can be (i) a specific natural number k ≥ 1, in which case MORA computes the kth moments of all variables from running; (ii) a specific moment of one
loop variable of running (e.g. "xˆ2" specifying the second moment of a variable x
of Figure 1); or (iii) a list containing the goals as just specified. One can specify finitely
many goals as inputs to MORA; yet, at least one goal is required. For example, by
running mora("running", [1, "xˆ2", "xˆ3"]), MORA computes the expected values (first moments, i.e. 1) of all variables from Figure 1, as well as the second
and third moments of variable x of Figure 1 (specified by xˆ2 and xˆ3, respectively).
MORA is completely automatic. That is, once an execution of MORA is started on
a given Prob-solvable loop and input goals, MORA outputs the higher-order moments,
and thus moment-based invariants, of its loop w.r.t. the specified input goals. To this end,
MORA computes the expected values of all monomials over loop variables, on which
one of the goals from Goal depends. In general, computing the kth moment requires
computing the expected values of all monomial expressions over loop variables, such
that the total degree of the monomials is less or equal than k – see [2] for more details.