pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-28 07:16:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

SeparationLogic_template

Browse source
This commit is contained in:
Adam Chlipala 2016-04-20 10:29:55 -04:00
parent 47fd9a8abf
commit 28bd2266bf
3 changed files with 1155 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
SeparationLogic.v
View file

@ -115,7 +115,7 @@ Module Import S <: SEP.
(* Separating conjunction, one of the two big ideas of separation logic. (* Separating conjunction, one of the two big ideas of separation logic.
* When does [star p q] apply to [h]? When [h] can be partitioned into two * When does [star p q] apply to [h]? When [h] can be partitioned into two
* subheaps [h1] and [h2], respectively compatible with [p] and [q]. See ook * subheaps [h1] and [h2], respectively compatible with [p] and [q]. See book
* module [Map] for definitions of [split] and [disjoint]. *) * module [Map] for definitions of [split] and [disjoint]. *)
Definition star (p q : hprop) : hprop := Definition star (p q : hprop) : hprop :=
fun h => exists h1 h2, split h h1 h2 /\ disjoint h1 h2 /\ p h1 /\ q h2. fun h => exists h1 h2, split h h1 h2 /\ disjoint h1 h2 /\ p h1 /\ q h2.

1153
SeparationLogic_template.v Normal file
View file

File diff suppressed because it is too large Load diff

1
_CoqProject
View file

@ -25,4 +25,5 @@ TypesAndMutation.v
DeepAndShallowEmbeddings_template.v DeepAndShallowEmbeddings_template.v
DeepAndShallowEmbeddings.v DeepAndShallowEmbeddings.v
SepCancel.v SepCancel.v
SeparationLogic_template.v
SeparationLogic.v SeparationLogic.v