From d96f252ebf4f0ce69329cb36e5cad039cf5fc75f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 10 Dec 2017 14:31:48 +0100
Subject: [PATCH] Revert "Docs: fix capitals of section."
This reverts commit 7a6d36c68948ac179f0519f73c7f857b0ebd1eea.
---
docs/algebra.tex | 2 +-
docs/base-logic.tex | 2 +-
docs/constructions.tex | 2 +-
docs/ghost-state.tex | 2 +-
docs/program-logic.tex | 10 +++++-----
5 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 5c2222caa..dc8bdead2 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 63e44070d..2a45cae7c 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 1ec372c84..0a205d845 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 4dc9f1626..bd10d54ef 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 079b811d3..06a9f7495 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 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.
@@ -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$.
--
GitLab