pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Proofreading MessagesAndRefinement

Browse source
This commit is contained in:
Adam Chlipala 2018-05-12 13:29:13 -04:00
parent 0f73a3901c
commit b3705cc79e
2 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
MessagesAndRefinement.v
View file

@ -29,7 +29,7 @@ Notation channel := nat (only parsing).
(* Here are the basic syntactic constructions of processes. *) (* Here are the basic syntactic constructions of processes. *)
Inductive proc := Inductive proc :=
| NewChannel (notThese : list channel) (k : channel -> proc) | NewChannel (notThese : list channel) (k : channel -> proc)
(* Pick a new channel [ch] name not found in [notThese], and continue like (* Pick a new channel name [ch] not found in [notThese], and continue like
* [k ch]. *) * [k ch]. *)
| BlockChannel (ch : channel) (pr : proc) | BlockChannel (ch : channel) (pr : proc)
@ -101,8 +101,8 @@ Definition tester (metaInput input output metaOutput : channel) : proc :=
(* Let's explain how programs run. We'll give a flavor of operational semantics (* Let's explain how programs run. We'll give a flavor of operational semantics
* called a "labeled transition system," because each step will include a label * called a "labeled transition system," because each step will include a label
* that explains what happened. In this case, the only relevant happenings are * that explains what happened. In this case, the only relevant happenings are
* sends or receives on channels. Crucially, we supress send/receive labels for * sends or receives on channels. Crucially, we suppress send/receive labels
* operations blocked by [Block]s. *) * for operations blocked by [Block]s. *)
Record message := { Record message := {
Channel : channel; Channel : channel;

5
frap_book.tex
View file

@ -4177,7 +4177,7 @@ We only trust the simple printing process, not the compiler that got us from a m
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Deriving Programs from Specifications} \chapter{Deriving Programs from Specifications}\label{deriving}
We have generally focused so far on proving that programs meet specifications. We have generally focused so far on proving that programs meet specifications.
What if we could generate programs from their specifications, in ways that guarantee correctness? What if we could generate programs from their specifications, in ways that guarantee correctness?
@ -5067,10 +5067,11 @@ What sorts of correctness theorems should we prove about processes?
The classic choice is to show that a more complex \emph{implementation} process is a \emph{safe substitute} for a simpler \emph{specification} process. The classic choice is to show that a more complex \emph{implementation} process is a \emph{safe substitute} for a simpler \emph{specification} process.
We will say that the implementation $p$ \emph{refines}\index{refinement} the specification $p'$. We will say that the implementation $p$ \emph{refines}\index{refinement} the specification $p'$.
Intuitively, such a claim means that any trace of labels that $p$ could generate may also be generated by $p'$, so that $p$ has \emph{no more behaviors} than $p'$ has, though it may have fewer behaviors. Intuitively, such a claim means that any trace of labels that $p$ could generate may also be generated by $p'$, so that $p$ has \emph{no more behaviors} than $p'$ has, though it may have fewer behaviors.
(There is a formal connection lurking here to the notion of refinement from Chapter \ref{deriving}, where method calls there are analogous to channel operations here.)
Crucially, in building traces of process executions, we ignore silent labels, only collecting the send and receive labels. Crucially, in building traces of process executions, we ignore silent labels, only collecting the send and receive labels.
This condition is called \emph{trace inclusion}\index{trace inclusion}, and, though it is intuitive, it is not strong enough to support all of the composition properties that we will want. This condition is called \emph{trace inclusion}\index{trace inclusion}, and, though it is intuitive, it is not strong enough to support all of the composition properties that we will want.
Instead, we formalize refinement via \emph{simulation}, very similarly to how we formalized compiler correctness in Chapter \ref{compiler_correctness}. Instead, we formalize refinement via \emph{simulation}, very similarly to how we formalized compiler correctness in Chapter \ref{compiler_correctness} and data abstraction in Chapter \ref{deriving}.
\abstraction \abstraction
\begin{definition} \begin{definition}