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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

module 0x42::M {

  struct S has drop {
    x: u64,
    y: bool,
    z: vector<u64>,
  }

  struct R has drop {
    s: S
  }

  struct G<T> {
    x: T,
    y: bool,
  }

  struct T has key {
    x: u64
  }

  spec module {

    // Field undeclared
    fun field_undeclared(s: S): u64 {
      s.xx
    }

    // Field wrongly typed
    fun field_wrongly_typed(s: S): bool {
      s.x
    }

    // Pack wrongly typed
    fun pack_wrongly_typed(x: u64, y: u64, z: vector<u64>): S {
      S{x: x, y: y, z: z}
    }

    fun pack_misses_fields(x: u64): S {
      S{x: x}
    }

    // Generic pack wrongly typed
    fun generic_pack_wrongly_typed(x: u64, y: bool): G<bool> {
      G{x: x, y: y}
    }

    // Wrong number of generics
    fun wrong_number_generics(x: u64, y: bool): G<u64> {
      G<u64, bool>{x: x, y: y}
    }
  }
}