# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Proof System
#### Program Judgments  
We now define _program judgments_ and give the Hoare rules of the program logic. Judgments of programs are sequents (quintuples) of the form \(\Gamma;\mathcal{R}\vdash\{\mathcal{P}\}\,C\,\{\mathcal{Q}\}\). The right-hand side is a traditional Hoare triple, whereas \(\mathcal{R}\) is a _resource invariant_ that captures resources available only to atomically executing programs (i.e., in executions that are free of thread interference), and \(\Gamma\) an environment in the style of interface specifications of [38]. These _process environments_ have the following definition.  
**Definition 29** (Process environments).: \[\Gamma\in\mathit{ProcEnv} ::= \mathcal{O}\mid\Gamma,\{\widetilde{B}\}\,P(x)\]  
That is, process environments are comma-separated sequences of pairs \(\{\widetilde{B}\}\,P(x)\) of processes \(P\) and their precondition \(\widetilde{B}\), with \(x\) a placeholder variable for an input parameter that may occur freely in both \(P\) and \(\widetilde{B}\). Note that processes do not have postconditions here; if desired one could encode process Hoare triples op top of these pairs as \(\{\widetilde{B_{\mathit{pre}}}\}\,P(x)\,\{\widetilde{B_{\mathit{post}}}\}\triangleq \{\widetilde{B_{\mathit{pre}}}\}\,(P(x)\cdot\gamma(\widetilde{B_{\mathit{post}}}))\)--by adding a trailing assertion. Moreover, even though process environments are given as sequences, they are used as if they were (finite) sets, as is customary, in the sense that the order of their pairs is unimportant.  
Process environments contain the contracts of the process-algebraic models defined for the program under verification. In particular, they allow for assume-guarantee style reasoning: the proof system may _assume_ validity of these contracts when dealing with process-algebraic models, since they must be _guaranteed_ externally, for example via interactive theorem proving or model checking, e.g., using mCRL2 [25]. Validity of process contracts and process environments is defined as follows.  
**Definition 30** (Validity of process environments).: _Any pair \(\{\widetilde{B}\}\,P(x)\) of a process \(P\) and its precondition \(\widetilde{B}\) is defined to be valid, denoted \(\models\{\widetilde{B}\}\,P(x)\), if \(\forall s,\sigma\cdot\,[\widetilde{B}[\widetilde{s}]]\sigma\implies\sigma \cdot\,(P,\sigma)\)._  
_Any process environment \(\Gamma\) is defined to be valid if \(\models_{\mathsf{env}}\Gamma\), which is a judgment inductively defined by the following two rules._  
\[\begin{array}{c}\infer{\models_{\mathsf{env}}\Gamma}{\models_{\mathsf{env}} \emptyset}\\ \infer{\models_{\mathsf{env}}\Gamma,\{\widetilde{B}\}\,P(x)}\end{array}\]Figures 4 and 5 give the Hoare rules of the logic. The standard structural rules are essentially the same as the ones of classical CSL [34]. One minor difference is that HT-atomic leaves true instead of \"emp\" after obtaining a resource invariant, since our logic is intuitionistic. (The assertion language of classical CSL contains an extra emp construct, for explicitly denoting that the heap is empty. In our intuitionistic version of the logic, resources are allowed to be thrown away using \(*\)-weak. As a consequence, assertions cannot express \"precise\" properties about the content of the heap, including emptiness of heaps.) Moreover, our assertion language does not contain the logical conjunction \(\wedge\) connective, but has separating conjunction instead.