mv-model 0.3.2

Move model
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

error: undeclared `M::one`
  ┌─ tests/sources/lets_err.move:6:16
  │
6 │     let zero = one;
  │                ^^^

error: let bound `new_a` propagated via schema inclusion is referring to post state
   ┌─ tests/sources/lets_err.move:22:5
   │
21 │     let post new_a = old(a) / sum;
   │                      ------------ let defined here
22 │     include Ensures{actual: a, expected: new_a + sum - sum};
   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   ·
28 │     let a = expected;
   │     ----------------- not allowed to use post state

error: invalid reference to post state
   ┌─ tests/sources/lets_err.move:43:5
   │
43 │     include Requires{a: result};
   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │                         │
   │                         expression referring to post state
   ·
48 │     requires a != 0;
   │     ---------------- not allowed to refer to post state

error: invalid reference to post state
   ┌─ tests/sources/lets_err.move:44:5
   │
44 │     include Requires{a: old(x)};
   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │                         │
   │                         expression referring to post state
   ·
48 │     requires a != 0;
   │     ---------------- not allowed to refer to post state