1
$\begingroup$

I am currently reading Formal Methods - An Appetizer and am stuck in chapter 3 (Program Verification).

I am unfamiliar with logic and I do not think I understand the $\vDash$ notation correctly.


I tried to work through Definition 3.8 by giving myself a super-simple example:

Let there be an edge $(q_1, \texttt{y:=1}, q_2)$ and a predicate assignment that is given by $P(q_1)=(\texttt{x}=\underline{n})\land(\underline{n}>0)$.

How do I now prove in the sense of Definition 3.8 that the predicate assignment is correct given $\mathcal{S}[\![\texttt{y:=1}]\!](\sigma)=\sigma[\texttt{y}\mapsto 1]$ (which means the memory is updated so that $\texttt{y}$ now has value 1)?

I do not even know how to start.

What does it mean to have "suitable pairs of memory"?

Further, I already get stuck finding out whether $(\sigma,\underline{\sigma})\vDash P(q_1)$. I think what I am supposed to do is

$$\begin{align*}&(\sigma,\underline{\sigma})\vDash P(q_1)\\ =\quad &(\sigma,\underline{\sigma})\vDash (\texttt{x}=\underline{n})\land(\underline{n}>0)\\ =\quad &\left(\,(\sigma,\underline{\sigma})\vDash (\texttt{x}=\underline{n})\,\right)\land\left(\,(\sigma,\underline{\sigma})\vDash(\underline{n}>0\,\right)\\ \end{align*}$$

and then first do

$$\begin{align*}&(\sigma,\underline{\sigma})\vDash (\texttt{x}=\underline{n})\\ =\quad &[\![\texttt{x}]\!](\sigma,\underline{\sigma})=[\![\underline{n}]\!](\sigma,\underline{\sigma})\end{align*}$$

and this is where I am stuck... now, $[\![\texttt{x}]\!](\sigma,\underline{\sigma})$ is $\sigma(x)$ by definition, that is, the value of $\texttt{x}$ in the memory $\sigma$, and $[\![\underline{n}]\!](\sigma,\underline{\sigma})$ is $\underline{\sigma}(\underline{n})$, but I never specified which values are in $\sigma$ and $\underline{\sigma}$.

And rightfully so, I think, because I want to prove it for all "suitable" memories. How do I proceed here?

Any help would be greatly appreciated!


These are the relevant parts from the book in order to provide (hopefully) enough context.

enter image description here

as well as

enter image description here

$\endgroup$

1 Answer 1

1
+100
$\begingroup$

What does it mean to have "suitable pairs of memory"?

In the case of the Definition 3.8 it means exactly any pair that makes $(\sigma,\underline{\sigma})\vDash P(q_1)$ true. If it's not true then the whole premise of implication in the Definition 3.8 is false and from false anything goes thus the predicate $P$ is vacuously correct. That's a boring case so we're only interested in $(\sigma,\underline{\sigma})$ that indeed validates the predicate, which means we have some constrains regarding the sigmas.

In your examples constrains are straightforward, they are precisely where you stopped: $[\![\texttt{x}]\!](\sigma,\underline{\sigma})=[\![\underline{n}]\!](\sigma,\underline{\sigma})$ meaning $\sigma(\texttt{x}) = \underline{\sigma}(\underline{n})$.

The next step is to show $(\sigma',\underline{\sigma})\vDash P(q_2)$ given $\sigma' = \mathcal{S}[\![\texttt{y:=1}]\!](\sigma)$ and $\sigma(\texttt{x}) = \underline{\sigma}(\underline{n})$. Simplifying this gives us $\sigma' = \sigma[\texttt{x}\mapsto \underline{\sigma}(\underline{n})][\texttt{y}\mapsto 1]$ (yeah we can simply chain square brackets especially realizing they even commute in a case of different variables :)).

I guess the rest is rather obvious considering your predicate $P$ does not depend on $q_1$ or $q_2$ and the update to the $\sigma$ does not affect variable $\texttt{x}$. :)

I hope this helps!

$\endgroup$

Your Answer

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