Commit d96f252e authored by Ralf Jung's avatar Ralf Jung

Revert "Docs: fix capitals of section."

This reverts commit 7a6d36c6.
parent 7a6d36c6
\section{Algebraic structures} \section{Algebraic Structures}
\subsection{OFE} \subsection{OFE}
......
\section{Base logic} \section{Base Logic}
\label{sec:base-logic} \label{sec:base-logic}
The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit $\munit$. The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit $\munit$.
......
...@@ -17,7 +17,7 @@ Note that in the definition of the carrier $\latert\cofe$, $\latertinj$ is a con ...@@ -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$. $\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: Given a CMRA $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
\begin{align*} \begin{align*}
......
\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. 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. These are not ``extensions'' in the sense that they change the proof power of the logic, they just form useful derived principles.
......
...@@ -5,7 +5,7 @@ ...@@ -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. 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. 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} \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. 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 ...@@ -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} \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. 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 ...@@ -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}}} \[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}
{\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}} \] {\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: 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) \] \[ \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. 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 ...@@ -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 } {\FALSE \vs[\mask_1][\mask_2] \prop }
\end{mathparpagebreakable} \end{mathparpagebreakable}
\subsection{Weakest preconditions} \subsection{Weakest Precondition}
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. 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 ...@@ -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]} % {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]}
\end{mathparpagebreakable} \end{mathparpagebreakable}
\subsection{Invariant namespaces} \subsection{Invariant Namespaces}
\label{sec: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$. 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$.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment