I have to say whether or not the following two separation logic statements are valid:


1. $ x \mapsto 3 \* y \mapsto 7 \Longrightarrow x \mapsto 3 \* true $
2. $ true \* x \mapsto 3 \Longrightarrow x \mapsto 3 $


Where $ x \mapsto 3 $ means x (in the stack) points to an abitrary memory location in the heap containing the value 3.


Now as far as I understand the $ true $ in the first statement means that... in fact I'm not sure what it means. I have notes saying:


$ x \mapsto 1 $ == $ h = h1 $   

$ y \mapsto 2 $ == $ h = h2 $   

$ x \mapsto 1 \* y \mapsto 2 $ == $ h = h1 \* h2 $   

$ x \mapsto 1 \* true $ == h1 contained in h 


So back to the first statement: is it simply saying that x is pointing to a value 3 *somewhere in the heap* and therefore it is a valid satement because the value 3 is somewhere in the heap and it makes no assertions about y... Does that make any sense?


And the second statement is not valid because... I've never seen the true on the left hand side ?? 


I've started trying to read this [separation logic overview](http://www.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/www15818As2007/cs818A3-07.html) as it seems better than our lectures but any other links/pointers would be greatly appreciated.


I'm well aware that I'm rather out of my depth here and could be completely wrong with my assumption/answers above so any feedback would be great.


Thanks in advance



Are these separation logic statements valid?
The trick with separation logic is that the formulas describe resources (heaps) and if a logical implication holds, then both sides of the implication are descriptions of the same heap.


True can correspond to any heap.


$h \* x\mapsto 3$ is almost always a larger heap than $x\mapsto 3$, which consists of just one element. So it is not the case that every heap satisfying $\mathit{True} \* x\mapsto 3$ is also a heap satisfying $x\mapsto 3$.


Thus the first is valid, the second isn't. 


It's worth unravelling the semantics of separation logic formula to see this.


