heap_lang.ref 738 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
1 subgoal
  
  Σ : gFunctors
  H : heapG Σ
  E : coPset
  ============================
  --------------------------------------∗
  WP let: "x" := ref #1 in "x" <- ! "x" + #1;; ! "x" @ E {{ v, ⌜v = #2⌝ }}
  
1 subgoal
  
  Σ : gFunctors
  H : heapG Σ
  E : coPset
  l : loc
  ============================
  _ : l ↦ #1
  --------------------------------------∗
  WP #l <- #1 + #1;; ! #l @ E {{ v, ⌜v = #2⌝ }}
  
21
22
23
24
25
26
27
28
29
30
31
32
1 subgoal
  
  Σ : gFunctors
  H : heapG Σ
  fun1, fun2, fun3 : expr
  ============================
  --------------------------------------∗
  WP let: "val1" := fun1 #() in
     let: "val2" := fun2 "val1" in
     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
  {{ _, True }}