I have to say whether or not the following two separation logic statements are valid:
- $ x \mapsto 3 * y \mapsto 7 \Longrightarrow x \mapsto 3 * true $
- $ 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