test-pgm-jcf.mlw 327 Bytes
Newer Older
1

2 3 4
theory A
  type t
end
5

6 7
module P

8
  use import module A
9
  use import int.Int
10
  use import module stdlib.Array
11

12 13
  logic c : int

14
  let foo (t : array int) = 
15
    { length t >= 1 && t[0] = 1 }
16 17 18
    t[0 <- 1];
    t[0] + 3
    { result = 3 }
19

20
end
21

22

23 24
(*
Local Variables: 
25
compile-command: "unset LANG; make -C .. testl-ide"
26 27
End: 
*)