From b3705cc79eb246ecdbdb93012ede2a8621f8dda2 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 12 May 2018 13:29:13 -0400
Subject: [PATCH] Proofreading MessagesAndRefinement

---
 MessagesAndRefinement.v | 6 +++---
 frap_book.tex           | 5 +++--
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/MessagesAndRefinement.v b/MessagesAndRefinement.v
index 04ef22f..adc5ecf 100644
--- a/MessagesAndRefinement.v
+++ b/MessagesAndRefinement.v
@@ -29,7 +29,7 @@ Notation channel := nat (only parsing).
 (* Here are the basic syntactic constructions of processes. *)
 Inductive 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]. *)
 
 | 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
  * called a "labeled transition system," because each step will include a label
  * that explains what happened.  In this case, the only relevant happenings are
- * sends or receives on channels.  Crucially, we supress send/receive labels for
- * operations blocked by [Block]s. *)
+ * sends or receives on channels.  Crucially, we suppress send/receive labels
+ * for operations blocked by [Block]s. *)
 
 Record message := {
   Channel : channel;
diff --git a/frap_book.tex b/frap_book.tex
index 16b8390..66530d9 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -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.
 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.
 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.
+(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.
 
 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
 \begin{definition}