mv-model 0.3.2

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

module 0x42::M {

  struct S has copy, drop {
    x: u64,
  }

  spec S {
    global sum: num;
    invariant pack sum = sum + x;
    invariant unpack sum = sum - x;
  }
}