Skip to content
Snippets Groups Projects
Commit e018e3b1 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make better use of \Val, \State, \Expr macros.

parent 2af75e62
No related branches found
No related tags found
No related merge requests found
......@@ -26,7 +26,7 @@ Elements of $\SigAx$ are ranged over by $\sigax$.
\subsection{Grammar}\label{sec:grammar}
\paragraph{Syntax.}
Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$).
Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\Var$ of variables (ranged over by metavariables $\var$, $\varB$, $\varC$).
Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
\begin{align*}
......
......@@ -141,7 +141,7 @@
% We write $x \fgmapsto v$ for $\exists q.\; x \fgmapsto[q] v$ and $x \gmapsto v$ for $x \fgmapsto[1] v$.
% Note that $x \fgmapsto v$ is duplicable but cannot be boxed (as it depends on resources); \ie we have $x \fgmapsto v \Lra x \fgmapsto v * x \fgmapsto v$ but not $x \fgmapsto v \Ra \always x \fgmapsto v$.
% To implement this interface, allocate an instance $\gname_G$ of $\FHeap(\textdom{Val})$ and define
% To implement this interface, allocate an instance $\gname_G$ of $\FHeap(\Val)$ and define
% \[
% x \fgmapsto[q] v \eqdef
% \begin{cases}
......
......@@ -136,6 +136,8 @@
\newcommand{\Val}{\textdom{Val}}
\newcommand{\Loc}{\textdom{Loc}}
\newcommand{\Expr}{\textdom{Expr}}
\newcommand{\Var}{\textdom{Var}}
\newcommand{\ThreadPool}{\textdom{ThreadPool}}
\newcommand{\cofe}{T}
\newcommand{\cofeB}{U}
......
......@@ -3,12 +3,14 @@
\section{Language}
\label{sec:language}
A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that
A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), and a set \State of \emph{states} (metavariable $\state$) such that
\begin{itemize}
\item There exist functions $\ofval : \textdom{Val} \to \textdom{Expr}$ and $\toval : \textdom{Expr} \pfn \textdom{val}$ (notice the latter is partial), such that
\begin{mathpar} {\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and {\All\val. \toval(\ofval(\val)) = \val}
\item There exist functions $\ofval : \Val \to \Expr$ and $\toval : \Expr \pfn \Val$ (notice the latter is partial), such that
\begin{mathpar}
{\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and
{\All\val. \toval(\ofval(\val)) = \val}
\end{mathpar}
\item There exists a \emph{primitive reduction relation} \[(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\cup_n \textdom{Expr}^n)\]
\item There exists a \emph{primitive reduction relation} \[(-,- \step -,-,-) \subseteq \Expr \times \State \times \Expr \times \State \times (\cup_n \Expr^n)\]
A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \overline\expr$ indicates that, when $\expr_1$ reduces to $\expr_2$, the new threads in the list $\overline\expr$ is forked off.
We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$, \ie when no threads are forked off. \\
\item All values are stuck:
......@@ -26,7 +28,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
\end{defn}
\begin{defn}[Context]
A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
A function $\lctx : \Expr \to \Expr$ is a \emph{context} if the following conditions are satisfied:
\begin{enumerate}[itemsep=0pt]
\item $\lctx$ does not turn non-values into values:\\
$\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot $
......@@ -43,7 +45,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\paragraph{Machine syntax}
\[
\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Expr}^n
\tpool \in \ThreadPool \eqdef \bigcup_n \Expr^n
\]
\judgment[Machine reduction]{\cfg{\tpool}{\state} \step
......
......@@ -14,7 +14,7 @@ To this end, we use tokens that manage which invariants are currently enabled.
We assume to have the following four CMRAs available:
\begin{align*}
\textmon{State} \eqdef{}& \authm(\exm(\textdom{State})) \\
\textmon{State} \eqdef{}& \authm(\exm(\State)) \\
\textmon{Inv} \eqdef{}& \authm(\mathbb N \fpfn \agm(\latert \iPreProp)) \\
\textmon{En} \eqdef{}& \pset{\mathbb N} \\
\textmon{Dis} \eqdef{}& \finpset{\mathbb N}
......@@ -249,10 +249,10 @@ The purpose of the adequacy statement is to show that our notion of weakest prec
There are two properties we are looking for: First of all, the postcondition should reflect actual properties of the values the program can terminate with.
Second, a proof of a weakest precondition with any postcondition should imply that the program is \emph{safe}, \ie that it does not get stuck.
To express the adequacy statement for functional correctness, we assume we are given some set $V \in \textdom{Val}$ of legal return values.
To express the adequacy statement for functional correctness, we assume we are given some set $V \subseteq \Val$ of legal return values.
Furthermore, we assume that the signature $\Sig$ adds a predicate $\pred$ to the logic which reflects $V$ into the logic:
\[\begin{array}{rMcMl}
\Sem\pred &:& \Sem{\textdom{Val}\,} \nfn \Sem\Prop \\
\Sem\pred &:& \Sem{\Val\,} \nfn \Sem\Prop \\
\Sem\pred &\eqdef& \Lam \val. \Lam \any. \setComp{n}{v \in V}
\end{array}\]
The signature can of course state arbitrary additional properties of $\pred$, as long as they are proven sound.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment