# Are these separation logic statements valid?

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 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.

-
This seems like a homework level computer science question, rather than a research level mathematics question. If so, it is off-topic for MathOverflow. – Pete L. Clark May 31 '10 at 17:15

$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$.
should be just a bit more careful: a formula $A$ describes a 'set' of heaps $[A]$, and an implication $A\supset B$ holds iff $h \in [A]$ implies $h\in [B]$. – Noam Zeilberger Jun 1 '10 at 17:32