mv-model 0.3.2

Move model
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14

module 0x42::M {

  fun invalid_old_exp(x: &mut u64, y: u64) {
    let a = x;
    let b = &mut y;
    *a = *b;
    *b = 0;
    spec {
      assert old(a) == y;
      assert old(b) == 0;
      assert old(x != y);
    }
  }
}