diff --git a/docs/algebra.tex b/docs/algebra.tex index dc8bdead2a4ecf03b35cda890b1889420fca2241..5c2222caa82eb72514ba1345153184a975cc83ab 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -1,4 +1,4 @@ -\section{Algebraic Structures} +\section{Algebraic structures} \subsection{OFE} diff --git a/docs/base-logic.tex b/docs/base-logic.tex index 2a45cae7cbd88a1fc94619caf86a6a06aadb95df..63e44070dd919baf13c3dd12ca3047524dc25bc7 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -1,4 +1,4 @@ -\section{Base Logic} +\section{Base logic} \label{sec:base-logic} The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit $\munit$. diff --git a/docs/constructions.tex b/docs/constructions.tex index 0a205d8450d472dd288c9f6e4f9ddde69b5c071a..1ec372c848fdea1b7c94d6fbab730365c2e4e5f4 100644 --- a/docs/constructions.tex +++ b/docs/constructions.tex @@ -17,7 +17,7 @@ Note that in the definition of the carrier $\latert\cofe$, $\latertinj$ is a con $\latert(-)$ is a locally \emph{contractive} functor from $\OFEs$ to $\OFEs$. -\subsection{Uniform Predicates} +\subsection{Uniform predicates} Given a CMRA $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows: \begin{align*} diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex index bd10d54efa60000c9290d79789776440300a521a..4dc9f16269e0d0a9da35ab162e74594de2b02a7b 100644 --- a/docs/ghost-state.tex +++ b/docs/ghost-state.tex @@ -1,4 +1,4 @@ -\section{Extensions of the Base Logic} +\section{Extensions of the base logic} In this section we discuss some additional constructions that we define within and on top of the base logic. These are not extensions'' in the sense that they change the proof power of the logic, they just form useful derived principles. diff --git a/docs/program-logic.tex b/docs/program-logic.tex index 06a9f74959f9bad0bc14ead5414f9418e9a1c152..079b811d3e336536ee6ac65d45d008f19a600da8 100644 --- a/docs/program-logic.tex +++ b/docs/program-logic.tex @@ -5,7 +5,7 @@ This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the base logic. So in the following, we assume that some language $\Lang$ was fixed. -\subsection{Dynamic Composeable Higher-Order Resources} +\subsection{Dynamic composeable higher-order resources} \label{sec:composeable-resources} The base logic described in \Sref{sec:base-logic} works over an arbitrary CMRA $\monoid$ defining the structure of the resources. @@ -101,7 +101,7 @@ We will typically leave the $M_i$ implicit when asserting ghost ownership, as th -\subsection{World Satisfaction, Invariants, Fancy Updates} +\subsection{World satisfaction, invariants, fancy updates} \label{sec:invariants} To introduce invariants into our logic, we will define weakest precondition to explicitly thread through the proof that all the invariants are maintained throughout program execution. @@ -137,7 +137,7 @@ The following assertion states that an invariant with name $\iname$ exists and m $\knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}} {\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}}$ -\paragraph{Fancy Updates and View Shifts.} +\paragraph{Fancy updates and view shifts.} Next, we define \emph{fancy updates}, which are essentially the same as the basic updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants: $\pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop)$ Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update. @@ -244,7 +244,7 @@ Still, just to give an idea of what view shifts are'', here are some proof rul {\FALSE \vs[\mask_1][\mask_2] \prop } \end{mathparpagebreakable} -\subsection{Weakest Precondition} +\subsection{Weakest preconditions} Finally, we can define the core piece of the program logic, the assertion that reasons about program behavior: Weakest precondition, from which Hoare triples will be derived. @@ -439,7 +439,7 @@ We only give some of the proof rules for Hoare triples here, since we usually do % {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]} \end{mathparpagebreakable} -\subsection{Invariant Namespaces} +\subsection{Invariant namespaces} \label{sec:namespaces} In \Sref{sec:invariants}, we defined an assertion $\knowInv\iname\prop$ expressing knowledge (\ie the assertion is persistent) that $\prop$ is maintained as invariant with name $\iname$.