alt-ergo-models.mlw 855 Bytes
Newer Older
1

2
3
4
5
6
7
(*

DONE alt-ergo devrait tenir que de certains labels, i.e.
pour les termes et les propositions, un label qui matche "model:.*", et
pour les variables "model:[0-9]+" 

MARCHE Claude's avatar
MARCHE Claude committed
8
DONE: modele donné apres timeout
9
10
11

*)

12
13
14
15
module M1

  use import int.Int

16
17
18
19
20
21
22
  let f (x "model:0":int) : int =
    { }
    if ("model:cond" x >= 42) then x + 3 else 0
    { "model:post" result <= 50 }

  let f_no_lab (x:int) : int =
    { }
23
24
25
    if x >= 42 then x + 3 else 0
    { result <= 50 }

26
27
  use import module ref.Ref

28
29
  let g (x "model:0": ref int) : int =
    { }
30
    x := !x + 1;
31
32
33
34
35
36
37
    if ("model:cond" !x >= 42) then !x + 3 else 0
    { "model:post" result <= 50 }

  let g_no_label (x : ref int) : int =
    { }
    x := !x + 1;
    if (!x >= 42) then !x + 3 else 0
38
39
    { result <= 50 }

40
end
41
42
43
44
45
46
47


(*
Local Variables: 
compile-command: "../../bin/why3ide alt-ergo-models.mlw"
End: 
*)