Proving a predicate assignment is correct

Question

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.

as well as

Answer 1

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!