Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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

share|improve this question
4  
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

1 Answer 1

up vote 0 down vote accepted

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.

share|improve this answer
1  
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

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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