bench/check-ce/array_records_mono.mlw

   1 module ArrayRecords
   2
   3     use int.Int
   4     use map.Map
   5
   6     type value = int
   7     type index = int
   8
   9     function to_rep value: int
  10     meta "model_projection" function to_rep
  11
  12     type basic_record = {
  13         flag [@model_trace:flag] : bool;
  14         first_value [@model_trace:first_val] : value;
  15         second_value [@model_trace:sec_val] : value;
  16     }
  17
  18     type array_of_records = private {
  19         mutable ghost elts : int -> basic_record;
  20         length : int
  21     } invariant { 0 <= length }
  22
  23     function ([]) (a: array_of_records) (i: int) : basic_record = a.elts i
  24
  25     val ([]) (a: array_of_records) (i: int) : basic_record
  26         requires { [@expl:index in array bounds] 0 <= i < length a }
  27         ensures  { result = a[i] }
  28
  29     val ghost function ([<-]) (a: array_of_records) (i: int) (v: basic_record): array_of_records
  30         ensures { result.length = a.length }
  31         ensures { result.elts = Map.set a.elts i v }
  32
  33     val ([]<-) (a: array_of_records) (i: int) (v: basic_record) : unit writes {a}
  34         requires { [@expl:index in array bounds] 0 <= i < length a }
  35         ensures  { a.elts = Map.set (old a).elts i v }
  36         ensures  { a = (old a)[i <- v] }
  37
  38 end
  39
  40 module Test
  41
  42    use int.Int
  43    use ArrayRecords
  44
  45    let var_overwrite (a: array_of_records) (i: int) : unit
  46      requires { a[i] = {flag = true; first_value = 3; second_value = 5}}
  47      ensures { a[i].first_value = 42 }
  48    =
  49      a[i] <- {flag = a[i].flag; first_value= a[i].first_value; second_value = 69};
  50      a[i] <- {flag = a[i].flag; first_value= 42; second_value = a[i].second_value};
  51      a[i] <- {flag = a[i].flag; first_value= 23; second_value = a[i].second_value};
  52      a[i] <- {flag = false; first_value= a[i].first_value; second_value = a[i].second_value};
  53      assert {a[i].second_value = 69};
  54
  55 end