mv-model 0.3.2

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

module 0x42::M {

  struct S {
    x: u64,
  }

  spec module {
    fun exists_in_vector(v: vector<S>): bool {
      exists s in v: s.x > 0
    }

    fun some_in_vector(v: vector<S>): S {
        choose s in v where s.x == 0
    }
  }
}