Fix spec typos (#359)

spec/bounds_safety/README.md

@@ -27,7 +27,7 @@ resulting file will be called checkedc.pdf.
 
 ## Obtaining LaTex 
 There are many widely
-used free distributions of LaTex available.   One version is [MikTex](http://www.miktek.org),
+used free distributions of LaTex available.   One version is [MikTex](http://www.miktex.org),
 which is widely used on Windows.  Another version is [TexLive](http://tug.org/texlive/),
 which is often used on Linux system.
 

spec/bounds_safety/checking-variable-bounds.tex

@@ -17,7 +17,7 @@ \chapter{Bounds for expressions and bounds declaration checking}
 rules.  The inference rules are defined by induction over expressions, 
 the same way that typechecking rules work.  Given an expression
 and bounds expressions for its subexpressions, a bounds expression
-is constructed.  The induction base casses are variables (for which
+is constructed.  The induction base cases are variables (for which
 bounds expressions are declared by the programmer) and constants.
 The inference may require the compiler to introduce temporaries to
 hold the values of subexpressions.
@@ -53,9 +53,9 @@ \chapter{Bounds for expressions and bounds declaration checking}
 rules for expressions.  C does not have a precise order of evaluation
 for expressions.  The times at which assignments
 must happen within expressions are only partially constrained.
-C also allows allows control flow within 
+C also allows control flow within 
 expressions via comma expressions, conditional expressions, and
-logical boolean expressions (the \code{&&} and \code{||} expressions).
+logical boolean expressions (the \code{&&} and \code{\|\|} expressions).
 
 To handle this, the analysis tracks sets of variables where assignments
 to those variables may not have been completed yet.  We call these
@@ -886,7 +886,7 @@ \subsection{Checking overview}
 sets of variables with pending assignments.  Pending
 assignments may or may not have been completed yet, which means
 that the variables being assigned to have {\em indeterminate}
-values.  The sets are used to used to detect:
+values.  The sets are used to detect:
 \begin{enumerate}
 \item Uses of variables whose values are indeterminate.
 \item Accessing memory with pointers whose bounds expressions

spec/bounds_safety/core-extensions.tex

@@ -1235,7 +1235,7 @@ \section{Programmer-inserted dynamic checks}
 
 \begin{lstlisting}[escapechar=\@]
 void decode(array_ptr<char> output_buffer, array_ptr<char> input_buffer,
-            size_t input_len|\textit{, size\_t output\_len}|)
+            size_t input_len, size_t output_len)
 {
   ...
       case UNCOMPRESSED_BYTES: {
@@ -1375,7 +1375,7 @@ \section{Programmer-inserted dynamic checks}
 }
 \end{lstlisting}
 
-The compiler now knows that \lstinline+i < src_count<= dst\_count+,
+The compiler now knows that \lstinline+i < src_count<= dst_count+,
 so it can eliminate the check.
 
 A compiler would not introduce this dynamic\_check because it would
@@ -1557,7 +1557,7 @@ \section{Changes to undefined behavior}
 first item (avoiding out-of-bounds pointer accesses). A
 partial correctness guarantee has the form ``assuming X holds, then Y is
 true''. Informally, one might say ``assuming that memory allocation and
-type casts are correct and that unchecked code never reads or write though
+type casts are correct and that unchecked code never reads or writes through
 out-of-bounds pointers, then checked code never reads or writes through
 out-of-bounds pointers.'' These assumptions can be turned into formal
 statements about program behavior at runtime. Given those assumptions,

spec/bounds_safety/variable-bounds.tex

@@ -1562,7 +1562,7 @@ \subsection{Definition of extent}
   to it at the component, then all the bounds declarations applying to
   it at the component must be syntactically identical. This avoids
   ambiguity about which bounds declaration applies to an occurrence of a
-  variable. It an error for the bounds declarations to disagree.
+  variable. It is an error for the bounds declarations to disagree.
 \item
   \emph{No missing bounds declarations}: If a bounds declaration for a
   variable applies to a function component, then all paths from the