2
$\begingroup$

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.

Thanks in advance

$\endgroup$
1
  • 4
    $\begingroup$ This seems like a homework level computer science question, rather than a research level mathematics question. If so, it is off-topic for MathOverflow. $\endgroup$ May 31, 2010 at 17:15

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ 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]$. $\endgroup$ Jun 1, 2010 at 17:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.