tests/array_eq.mlw

   1
   2
   3 module ArrayUpdate
   4
   5   use int.Int
   6   use array.Array
   7
   8   let test (a:array int)
   9     requires { a.length >= 1 }
  10    =
  11     label L in
  12     a[0] <- 42;
  13     assert { a = (a at L)[0 <- 42] }
  14
  15
  16 end
  17
  18
  19 module ImpMapUpdate
  20
  21   clone impmap.ImpmapNoDom with type key = int
  22
  23   let test (m:t int) =
  24     label L in
  25     m[0] <- 42;
  26     assert { m = (m at L)[0 <- 42] }
  27
  28
  29
  30 end
  31
  32 module ArrayFunctionalUpdate
  33
  34   use int.Int
  35   use array.Array
  36
  37   predicate p (array int)
  38
  39   let test (a:array int) (i:int)
  40     requires { 0 <= i < a.length }
  41     requires { p (a[i<-42]) }
  42   = a[i] <- 42;
  43     assert { p a }
  44
  45 end