Skip to content
Snippets Groups Projects
Commit ee8bef79 authored by Ralf Jung's avatar Ralf Jung
Browse files

make logatom printing consistent with new WP/Texan Triple printing

parent 163e26ee
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/bi/lib/atomic.v
+ 12
− 12
View file @ ee8bef79
......@@ -113,7 +113,7 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'C
) .. )
)
(at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
format "'[ ' 'AU' '<<' ∀ x1 .. xn , α '>>' '/' '[' @ Eo , Ei ']' '/' '[ ' '<<' ∃ y1 .. yn , β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
format "'[hv ' 'AU' '<<' '[' ∀ x1 .. xn , '/' α ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' ∃ y1 .. yn , '/' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
(atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
......@@ -127,7 +127,7 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :
λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
)
(at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
format "'[ ' 'AU' '<<' ∀ x1 .. xn , α '>>' '/' '[' @ Eo , Ei ']' '/' '[ ' '<<' β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
format "'[hv ' 'AU' '<<' '[' ∀ x1 .. xn , '/' α ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
(atomic_update (TA:=TeleO)
......@@ -142,7 +142,7 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :
(λ y1, .. (λ yn, Φ%I) ..))
)
(at level 20, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
format "'[ ' 'AU' '<<' α '>>' '/' '[' @ Eo , Ei ']' '/' '[ ' '<<' ∃ y1 .. yn , β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
format "'[hv ' 'AU' '<<' '[' α ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' ∃ y1 .. yn , '/' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
(atomic_update (TA:=TeleO) (TB:=TeleO) Eo Ei
......@@ -151,10 +151,10 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
(tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
)
(at level 20, Eo, Ei, α, β, Φ at level 200,
format "'[ ' 'AU' '<<' α '>>' '/' '[' @ Eo , Ei ']' '/' '[ ' '<<' β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
format "'[hv ' 'AU' '<<' '[' α ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
(** Notation: Atomic accessors *)
Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
(atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
Eo Ei
......@@ -173,9 +173,9 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 ..
) .. )
)
(at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
format "'[ ' 'AACC' '[ ' '<<' ∀ x1 .. xn , α '/' ABORT P '>>' ']' '/' '[' @ Eo , Ei ']' '/' '[ ' '<<' ∃ y1 .. yn , β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
format "'[hv ' 'AACC' '<<' '[' ∀ x1 .. xn , '/' α , '/' ABORT P ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' ∃ y1 .. yn , '/' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
(atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
(TB:=TeleO)
Eo Ei
......@@ -188,9 +188,9 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM
λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
)
(at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder,
format "'[ ' 'AACC' '[ ' '<<' ∀ x1 .. xn , α '/' ABORT P '>>' ']' '/' '[' @ Eo , Ei ']' '/' '[ ' '<<' β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
format "'[hv ' 'AACC' '<<' '[' ∀ x1 .. xn , '/' α , '/' ABORT P ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
(atomic_acc (TA:=TeleO)
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
Eo Ei
......@@ -204,9 +204,9 @@ Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM
(λ y1, .. (λ yn, Φ%I) ..))
)
(at level 20, Eo, Ei, α, P, β, Φ at level 200, y1 binder, yn binder,
format "'[ ' 'AACC' '[ ' '<<' α '/' ABORT P '>>' ']' '/' '[' @ Eo , Ei ']' '/' '[ ' '<<' ∃ y1 .. yn , β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
format "'[hv ' 'AACC' '<<' '[' α , '/' ABORT P ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' ∃ y1 .. yn , '/' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
(atomic_acc (TA:=TeleO)
(TB:=TeleO)
Eo Ei
......@@ -216,7 +216,7 @@ Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
(tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
)
(at level 20, Eo, Ei, α, P, β, Φ at level 200,
format "'[ ' 'AACC' '[ ' '<<' α '/' ABORT P '>>' ']' '/' '[' @ Eo , Ei ']' '/' '[ ' '<<' β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
format "'[hv ' 'AACC' '<<' '[' α , '/' ABORT P ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
(** Lemmas about AU *)
Section lemmas.
......
iris/program_logic/atomic.v
+ 4
− 4
View file @ ee8bef79
......@@ -42,7 +42,7 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v
) .. )
)
(at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
format "'[hv' '[ ' '<<<' ∀ x1 .. xn , α '>>>' ']' '/ ' e @ E '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v '>>>' ']' ']'")
format "'[hv' '<<<' '[' ∀ x1 .. xn , '/' α ']' '>>>' '/ ' e @ E '/' '<<<' '[' ∃ y1 .. yn , '/' β , '/' 'RET' v ']' '>>>' ']'")
: bi_scope.
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
......@@ -62,7 +62,7 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
) .. )
)
(at level 20, E, α, β, v at level 200, x1 binder, xn binder,
format "'[hv' '[ ' '<<<' ∀ x1 .. xn , α '>>>' ']' '/ ' e @ E '/' '[ ' '<<<' β , '/' 'RET' v '>>>' ']' ']'")
format "'[hv' '<<<' '[' ∀ x1 .. xn , '/' α ']' '>>>' '/ ' e @ E '/' '<<<' '[' β , '/' 'RET' v ']' '>>>' ']'")
: bi_scope.
Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
......@@ -79,7 +79,7 @@ Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
(λ y1, .. (λ yn, v%V) .. ))
)
(at level 20, E, α, β, v at level 200, y1 binder, yn binder,
format "'[hv' '[ ' '<<<' α '>>>' ']' '/ ' e @ E '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v '>>>' ']' ']'")
format "'[hv' '<<<' '[' α ']' '>>>' '/ ' e @ E '/' '<<<' '[' ∃ y1 .. yn , '/' β , '/' 'RET' v ']' '>>>' ']'")
: bi_scope.
Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
......@@ -92,7 +92,7 @@ Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
(tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) v%V)
)
(at level 20, E, α, β, v at level 200,
format "'[hv' '[ ' '<<<' α '>>>' ']' '/ ' e @ E '/' '[ ' '<<<' β , '/' 'RET' v '>>>' ']' ']'")
format "'[hv' '<<<' '[' α ']' '>>>' '/ ' e @ E '/' '<<<' '[' β , '/' 'RET' v ']' '>>>' ']'")
: bi_scope.
(** Theory *)
......
tests/atomic.ref
+ 60
− 42
View file @ ee8bef79
......@@ -9,8 +9,9 @@
============================
"Hl" : l ↦ v
--------------------------------------∗
AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0 ABORT l ↦ v >>
@ ⊤ ∖ ∅, ∅ << l ↦{q} v0, COMM Q -∗ Q >>
AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT l ↦ v >>
@ ⊤ ∖ ∅, ∅
<< l ↦{q} v0, COMM Q -∗ Q >>
"non_laterable"
: string
......@@ -24,8 +25,9 @@
============================
"HP" : ▷ P
--------------------------------------∗
AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >>
@ ⊤ ∖ ∅, ∅ << l ↦{q} v, COMM True >>
AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
@ ⊤ ∖ ∅, ∅
<< l ↦{q} v, COMM True >>
1 goal
......@@ -37,8 +39,9 @@
============================
"HP" : ▷ P
--------------------------------------∗
AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >>
@ ⊤ ∖ ∅, ∅ << l ↦{q} v, COMM True >>
AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
@ ⊤ ∖ ∅, ∅
<< l ↦{q} v, COMM True >>
"printing"
: string
......@@ -67,10 +70,12 @@
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤ ∖ ∅, ∅
<< ∃ y : val, P y, COMM Φ #() >> >>
@ ⊤ ∖ ∅, ∅ << ∃ y : val, P y, COMM Φ #() >>
_ : AACC << ∀ x : val, P x,
ABORT AU << ∀ x : val, P x >>
@ ⊤ ∖ ∅, ∅
<< ∃ y : val, P y, COMM Φ #() >> >>
@ ⊤ ∖ ∅, ∅
<< ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -99,10 +104,12 @@
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤ ∖ ∅, ∅
<< l ↦ x, COMM Φ #() >> >>
@ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
_ : AACC << ∀ x : val, l ↦ x,
ABORT AU << ∀ x : val, l ↦ x >>
@ ⊤ ∖ ∅, ∅
<< l ↦ x, COMM Φ #() >> >>
@ ⊤ ∖ ∅, ∅
<< l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -131,10 +138,12 @@
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >> >>
@ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
_ : AACC << l ↦ #(),
ABORT AU << l ↦ #() >>
@ ⊤ ∖ ∅, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >> >>
@ ⊤ ∖ ∅, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -163,9 +172,10 @@
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >> >>
@ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
_ : AACC << l ↦ #(),
ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >> >>
@ ⊤ ∖ ∅, ∅
<< l ↦ #(), COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -177,7 +187,7 @@
heapGS0 : heapGS Σ
l : loc
============================
⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
code @ ∅
<<< ∃ y : val, l ↦ y, RET #() >>>
1 goal
......@@ -187,7 +197,8 @@
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤ ∖ ∅, ∅
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >>
@ ⊤ ∖ ∅, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -198,7 +209,7 @@
heapGS0 : heapGS Σ
l : loc
============================
⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ∅
<<< ∃ y : val, l ↦ y, RET #() >>>
1 goal
......@@ -209,7 +220,8 @@
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
@ ⊤ ∖ ∅, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -219,7 +231,7 @@
heapGS0 : heapGS Σ
l : loc
============================
⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ∅
<<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
......@@ -230,7 +242,7 @@
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
_ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
@ ⊤ ∖ ∅, ∅
<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
l ↦ xx, COMM Φ #() >>
......@@ -243,7 +255,7 @@
heapGS0 : heapGS Σ
l : loc
============================
⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ∅
<<< l ↦ x, RET #() >>>
1 goal
......@@ -253,8 +265,9 @@
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤ ∖ ∅, ∅
<< l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -265,7 +278,7 @@
l : loc
x : val
============================
⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ∅
<<< ∃ y : val, l ↦ y, RET #() >>>
1 goal
......@@ -276,8 +289,9 @@
x : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤ ∖ ∅, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -288,7 +302,7 @@
l : loc
x : val
============================
⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ∅
<<< l ↦ #(), RET #() >>>
1 goal
......@@ -299,8 +313,9 @@
x : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤ ∖ ∅, ∅
<< l ↦ #(), COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -311,7 +326,7 @@
l : loc
xx, yyyy : val
============================
⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ∅
<<< l ↦ yyyy, RET #() >>>
1 goal
......@@ -322,8 +337,9 @@
xx, yyyy : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
l ↦ xx >> @ ⊤ ∖ ∅, ∅ << l ↦ yyyy, COMM Φ #() >>
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
@ ⊤ ∖ ∅, ∅
<< l ↦ yyyy, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -334,7 +350,7 @@
l : loc
xx, yyyy : val
============================
⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ∅
<<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
......@@ -346,7 +362,8 @@
xx, yyyy : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤ ∖ ∅, ∅
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
@ ⊤ ∖ ∅, ∅
<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
l ↦ xx, COMM Φ #() >>
--------------------------------------∗
......@@ -363,7 +380,8 @@
============================
"AU" : ∃ x : val, P x ∗
(P x ={∅,⊤}=∗
AU << ∀ x0 : val, P x0 >> @ ⊤ ∖ ∅, ∅
AU << ∀ x0 : val, P x0 >>
@ ⊤ ∖ ∅, ∅
<< ∃ y : val, P y, COMM Φ #() >>)
∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
--------------------------------------∗
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment