Chalice/tests/refinements/Pick.chalice


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

class Pick0 {
  method pick(s: seq<int>) returns (x)
    requires |s| > 0;
  {
    var x [x in s]
  }
}

class Pick1 refines Pick0 {
  transforms pick(s: seq<int>) returns (x)
  {
    replaces x by {x := s[0]}
  }
}

class Pick2 refines Pick0 {
  transforms pick(s: seq<int>) returns (x)
  {
    replaces * by {x := s[|s|-1]}
  }
}

class Pick3 refines Pick0 {
  transforms pick(s: seq<int>) returns (x)
  {
    replaces x by {x := s[1]}
  }
}