# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Programs
#### 3.3.7 Semantics of Assertions  
Let us now define the semantic meaning of assertions. The semantics of assertions is defined in terms of a satisfaction relation \(ph,pm,s,\mathcal{P}\) stating that the assertion \(\mathcal{P}\) is satisfied by the model \((ph,pm,s,g)\). Its definition depends on an operation \(\llbracket\cdot\rrbracket:\mathit{AbstrBinder}\rightarrow\mathit{Store} \rightarrow\mathit{Binder}\) for evaluating abstraction binders \(\Pi=\{x_{0}\mapsto E_{0},\ldots,x_{n}\mapsto E_{n}\}\), that is defined as follows.  
**Definition 27** (Abstraction binder evaluation).: \[\llbracket\{x_{0}\mapsto E_{0},\ldots,x_{n}\mapsto E_{n}\}\rrbracket s\ \triangleq\ \lambda x\cdot\begin{cases}\llbracket E_{i}\rrbracket s&\text{if }\ x=x_{i}\ \text{ for some }0\leq i\leq n\\ \text{undefined}&\text{otherwise}\end{cases}\]  
Moreover, recall that hybrid processes may contain both program variables and process-algebraic variables. The semantics of assertions relies on a closure operation for \"closing\" processes with respect to any program variable occurring in it. More specifically, given any hybrid process \(\widetilde{P}\) and store \(s\), the \(s\)_-closure of \(\widetilde{P}\)_, written \(\widetilde{P}[s]\), is defined to be \(\widetilde{P}[X/s(X)]_{X\in\operatorname{FV}(\widetilde{P})}\), i.e., replacing every free program variable \(X\) in \(\widetilde{P}\) by \(s(X)\). This operation is \"closing\" \(\widetilde{P}\) in the sense that \(\operatorname{FV}(\widetilde{P}[s])=\emptyset\) and \(\widetilde{P}[s]\in\mathit{Proc}\).  
**Definition 28** (Semantics of assertions).: _The modelling relation \(ph,pm,s,g\models\mathcal{P}\) is defined by structural recursion on \(\mathcal{P}\) as follows._  
\[\begin{array}{rl}ph,pm,s,g\models B&\text{iff}\quad\llbracket B\rrbracket s \\ ph,pm,s,g\models\forall X.\mathcal{P}&\text{iff}\quad\forall v\cdot(ph,pm,s[X \mapsto v],g[X\mapsto v])\models\mathcal{P}\\ ph,pm,s,g\models\exists X.\mathcal{P}&\text{iff}\quad\exists v\cdot(ph,pm,s[X \mapsto v],g[X\mapsto v])\models\mathcal{P}\\ ph,pm,s,g\models\mathcal{P}_{1}\lor P_{1}&\text{iff}\quad ph,pm,s,g\models \mathcal{P}_{1}\lor ph,pm,s,g\models\mathcal{P}_{2}\\ ph,pm,s,g\models\mathcal{P}_{1}*\mathcal{P}_{2}&\text{iff}\quad\exists ph_{1},ph_{2}\cdot ph_{1}\perp_{\text{ph}}ph_{2}  
variables (namely \(X\)), one can not immediately deduce that it is bisimilar to \(\widetilde{P}\) according to Definition 7. However, we do have that \(0<X:\widetilde{P}\approx\widetilde{P}*X=2\), since for every model \((ph,pm,s,g)\) satisfying this assertion it holds that \(s(X)=2\). We shall later give entailment rules that allow such _context-dependent bisimulation equivalences_ to be used to simplify processes inside \(\mathsf{Proc}_{\pi}\) ownership predicates.  
The \(\models\) modelling relation satisfies the following properties:  
1. \(ph,pm,s,g\models\mathcal{P}\) and \(pm\cong_{\mathsf{pm}}pm\) implies \(ph,pm^{\prime},s,g\models\mathcal{P}\).
2. If \(ph,pm,s,g\models\mathcal{P}\), then for any \(ph^{\prime}\) and \(pm^{\prime}\) such that \(ph\perp_{\mathsf{ph}}ph^{\prime}\) and \(pm\perp_{\mathsf{pm}}pm\)\(pm^{\prime}\) it holds that \(ph\uplus_{\mathsf{ph}}ph^{\prime},pm\uplus_{\mathsf{pm}}pm^{\prime},s,g\models \mathcal{P}\).  
Lemma 7 is essential for allowing replacing process-algebraic abstractions by bisimilar ones inside the program logic. Lemma 7 expresses monotonicity, and states that adding resources does not invalidate the satisfiability of any assertion (i.e., adding more resources makes the assertion \"more true\"). This is a key property of _intuitionistic_ separation logic and is necessary for proving soundness of the weakening rule, which we introduce later in Section 3.4.1.