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?


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.