1
$\begingroup$

I am trying to show that the following interference is unsound in terms of Separation Logic:

$$ (p_0 \implies p_1) \implies ((p_0 * q) \implies (p_1 * q)) $$

I came up with the following values for a counter example: $p_0 = true$, $p_1 = x \mapsto 1$, $q = true$. The heap contains just one mapping of $x \mapsto 1$.

The idea is that $(p_1 * q)$ cannot be true because $p_1$ already describes the whole heap and there is nothing left for $q$.

I am not sure, however, why $true * true$ would hold if there is only one element in the heap. Shouldn’t it be false as those two $true$s cannot claim that single heap element at the same time?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.