Contracts Cleanup

.vscode/settings.json

@@ -6,5 +6,11 @@
         }
     ],
     "rewrap.autoWrap.enabled": true,
-    "rewrap.wrappingColumn": 80
+    "rewrap.wrappingColumn": 80,
+    "cSpell.words": [
+        "footgun",
+        "Gitter",
+        "irreflexivity",
+        "preorder"
+    ]
 }

README.md

@@ -24,15 +24,29 @@ On Windows, you can download the installer from
 
 Once you have Rust and Cargo installed, you can install or upgrade mdBook by running:
 
-```
+```bash
 cargo install mdbook
 ```
 
+**Install mdbook-katex (for LaTeX math rendering):**
+
+Linux and macOS:
+```bash
+cargo install mdbook-katex --version 0.10.0-alpha
+```
+
+Windows:
+```bash
+cargo install mdbook-katex --version 0.10.0-alpha --no-default-features --features duktape
+```
+
+Note: On Windows, we use the `duktape` feature instead of the default `quick-js` backend because quick-js doesn't compile on Windows.
+
 ## Building the book
 
 To build the book, run:
 
-```
+```bash
 mdbook serve ./better-code
 ```
 

better-code/README.md

@@ -22,6 +22,20 @@ Download the installer from [here](https://win.rustup.rs/).
 cargo install mdbook
 ```
 
+**Install mdbook-katex (for LaTeX math rendering):**
+
+Linux and macOS:
+```bash
+cargo install mdbook-katex --version 0.10.0-alpha
+```
+
+Windows:
+```bash
+cargo install mdbook-katex --version 0.10.0-alpha --no-default-features --features duktape
+```
+
+Note: On Windows, we use the `duktape` feature instead of the default `quick-js` backend because quick-js doesn't compile on Windows.
+
 ### Building and Serving the Book
 
 To build and serve the book locally:

better-code/book.toml

@@ -1,7 +1,6 @@
 [book]
 authors = ["Sean Parent"]
 language = "en"
-multilingual = false
 src = "src"
 title = "Better Code"
 description = "A principled and rigorous approach to software development"
@@ -20,3 +19,6 @@ enable = true
 
 [output.html.print]
 enable = true
+
+[preprocessor.katex]
+

better-code/src/chapter-2-contracts.md

@@ -137,26 +137,29 @@ terminology.
 
 Hoare used this notation, called a “Hoare triple,”
 
-> {P}S{Q}
+> $\lbrace P \rbrace S \lbrace Q \rbrace$
 
-which is an assertion that if **precondition** *P* is met, operation
-*S* establishes **postcondition** *Q*.
+which is an assertion that if **precondition** $P$ is met, operation
+$S$ establishes **postcondition** $Q$.
+
+<!-- This had been using math for pre and post conditions, but I find mixing math and code makes it look like we are talking about different `x` and $x$ variables and equality vs. assignment gets confusing. I think if the operation is expressed in code, the conditions should be expressed in code. -->
 
 For example:
 
 - if we start with `x == 2` (precondition), after `x += 1`, `x == 3` (postcondition):
 
-  > {x == 2}x+=1{x == 3}
+  > $\lbrace$ `x == 2` $\rbrace$ `x += 1` $\lbrace$ `x == 3` $\rbrace$
+
 
 - if `x` is less than the maximum integer (precondition), after `x
   += 1`, `x` is greater than the minimum integer (postcondition):
 
-  > {x < Int.max}x+=1{x > Int.min}
+  > $\lbrace$ `x < Int.max` $\rbrace$ `x += 1` $\lbrace$ `x > Int.min` $\rbrace$
 
 What makes preconditions and postconditions useful for formal proofs
 is this *sequencing rule*:
 
-> {P}S{Q} ∧ {Q}T{R} ⇒ {P}S;T{R}
+> $\lbrace P \rbrace S \lbrace Q \rbrace \wedge \lbrace Q \rbrace T \lbrace R \rbrace \Rightarrow \lbrace P \rbrace S;T \lbrace R \rbrace$
 
 Given two valid Hoare triples, if the postconditions of the first are
 the preconditions of the second, we can form a new valid triple describing
@@ -178,21 +181,21 @@ h = l + m
 ```
 
 There are many valid Hoare triples for each of them.  For instance,
-**{*l*+*m*=0}**`h = l + m`**{*h*≤0}**.  This one isn't particularly
+$\lbrace$ `l + m == 0` $\rbrace$ `h = l + m` $\lbrace$ `h <= 0` $\rbrace$. This one isn't particularly
 useful, but it is valid because if `l + m == 0` is true before we
 execute it, `h <= 0` will be true afterwards.
 
 The following—more useful—triples will help illustrate the sequencing rule:
 
-- **{*l*≤*h*}**`let m = (h - l )/2`**{*m*≥ 0}**, i.e.
+- $\lbrace$ `l <= h` $\rbrace$ `let m = (h - l )/2` $\lbrace$ `m >= 0` $\rbrace$, i.e.,
 
   ```swift
   // precondition: l <= h
   let m = (h - l) / 2
   // postcondition: m >= 0
   ```
 
-- **{*m*≥0}**`h = l + m`**{*l*≤*h*}**, i.e.
+- $\lbrace$ `m >= 0` $\rbrace$ `h = l + m` $\lbrace$ `l <= h` $\rbrace$, i.e.,
 
   ```swift
   // precondition: m >= 0
@@ -205,16 +208,16 @@ precondition means that the operations can be executed in
 sequence, with the sequence having the first precondition and the
 second postcondition. Thus there's a new valid triple:
 
-**{*l*≤*h*}**`let m = (h -l )/2; h = l + m`**{*l*≤*h*}**, i.e.
+$\lbrace$ `l <= h` $\rbrace$ `let m = (h - l) / 2; h = l + m` $\lbrace$ `l <= h` $\rbrace$, i.e.,
 
 ```swift
-  // precondition: l <= h
-  let m = (h - l) / 2
-  h = l + m
-  // postcondition: l <= h
+// precondition: l <= h
+let m = (h - l) / 2
+h = l + m
+// postcondition: l <= h
 ```
 
-which says that if *l*≤*h* is true on entry to the sequence, it is
+which says that if `l <= h` is true on entry to the sequence, it is
 also true on exit.
 
 ### Invariants
@@ -253,12 +256,12 @@ step in understanding what it does.
 
 ## Design By Contract
 
-> *…a software system is viewed as a set of communicating components
+> *&hellip;a software system is viewed as a set of communicating components
 > whose interaction is based on precisely defined specifications of
-> the mutual obligations — contracts.*
+> the mutual obligations &ndash; contracts.*
 >
->   —Building bug-free O-O software: An Introduction to Design by Contract™
->    https://www.eiffel.com/values/design-by-contract/introduction/
+>   &mdash; Building bug-free O-O software: An Introduction to Design by Contract&trade;
+>    <https://www.eiffel.com/values/design-by-contract/introduction/>
 
 In the mid 1980s, The French computer scientist Bertrand Meyer took
 Hoare Logic, and shaped it into a practical discipline for software
@@ -327,7 +330,7 @@ When we talk about an instance being “in a good state,” we
 mean that its type's invariants are satisfied.
 
 For example, this type's public interface is like an
-array of pairs, but it stores elements of those pairs separate
+array of pairs, but it stores elements of those pairs in separate
 arrays.[^array-pairs]
 
 [^array-pairs]: You might want to use a type like this one to store
@@ -482,7 +485,7 @@ neither correct nor incorrect; it does something, but does it do the
 
 > All undocumented software is waste. It's a liability for a company.
 >
-> —Alexander Stepanov (https://youtu.be/COuHLky7E2Q?t=1773)
+> &mdash;Alexander Stepanov (<https://youtu.be/COuHLky7E2Q?t=1773>)
 
 
 Documentation is also essential for local reasoning.  We build atop
@@ -715,7 +718,7 @@ Now, not every contract is as simple as the ones we've shown so far,
 but simplicity is a goal.  In fact, if you can't write a terse,
 simple, but _complete_ contract for a component, there's a good chance
 it's badly designed.  A classic example is the C library `realloc`
-function, which does at least three different things—allocate, deallocate, and resize 
+function, which does at least three different things—allocate, deallocate, and resize
 dynamic memory—all of which
 need to be described. A better design would have separated these
 functions.  So simple contracts are both easy to digest and easy to
@@ -825,7 +828,7 @@ part of the method*.
   /// - Precondition: `self` is non-empty.
   /// - Postcondition: The length is one less than before
   ///   the call. Returns the original last element.
- public mutating func popLast() -> T { ... }
+  public mutating func popLast() -> T { ... }
 ```
 
 The invariant of this function is the rest of the elements, which are
@@ -838,7 +841,7 @@ unchanged:
   /// - Postcondition: The length is one less than before
   ///   the call. Returns the original last element.
   /// - Invariant: the values of the remaining elements.
- public mutating func popLast() -> T { ... }
+  public mutating func popLast() -> T { ... }
 ```
 
 Now, if the postcondition seems a bit glaringly redundant with the
@@ -868,7 +871,7 @@ omitted.
   /// Removes and returns the last element.
   ///
   /// - Precondition: `self` is non-empty.
- public mutating func popLast() -> T { ... }
+  public mutating func popLast() -> T { ... }
 ```
 
 In fact, the precondition is implied by the summary too.  You
@@ -887,7 +890,7 @@ should be sufficient:
 
 ```swift
   /// Removes and returns the last element.
- public mutating func popLast() -> T { ... }
+  public mutating func popLast() -> T { ... }
 ```
 
 In practice, once you are comfortable with this discipline, the
@@ -929,14 +932,16 @@ the elements arranged from least to greatest. The contract gives an
 explicit precondition that isn't implied by the summary: it requires
 that the predicate be a strict weak ordering.
 
+<!-- SRP: this section bothers me. "among others" instead of fully spelling out the requirements, using (i, j + 1) which may not exist, and the n^2 comparisons without calling out the O(n^3) complexity or which properties could be practically checked. Also is "stable" the term we want to use? Regular and deterministic are also candidates. I've tried to rewrite this a couple of times, but it just gets too complex and the main point is lost. -->
+
 _Some_ precondition on the predicate is needed just to make the result
 a meaningful sort with respect to the predicate.  For example, a
 totally unconstrained predicate could return random boolean values,
 and there's no reasonable sense in which the function could be said to
 leave the elements sorted with respect to that.  Therefore the
-predicate at least has to be stable. To leave elements meaningfully
+predicate at least has to be deterministic. To leave elements meaningfully
 sorted, the predicate has to be *transitive*: if it is `true` for
-elements (*i*, *j*), it must also be true for elements (*i*, *j*+1).
+elements $(i, j)$, it must also be true for elements $(i, j + 1)$.
 A strict weak ordering has both of these properties, among others.
 
 Note that the performance of this method is documented.  Time and
@@ -947,8 +952,9 @@ function as part of its postconditions, which brings all the
 function's guarantees under one name: its postconditions.
 
 The strict weak ordering requirement is a great example of a
-precondition that can't be efficiently checked.  To do so would
-require at least *N*² comparisons, where *N* is the number of
+precondition that can't be checked: there's no way to verify that a function
+is deterministic. Even if we could assume determinism, a complete check
+requires at least $n^3$ comparisons, where $n$ is the number of
 elements, which would violate the complexity bound of the algorithm.
 
 The summary gives the postcondition that no two adjacent elements are
@@ -970,9 +976,9 @@ understood, is another source of complexity. In fact we should
 probably put a link in the documentation to a definition.
 
 ```swift
-/// - Precondition: `areInIncreasingOrder` is [a strict weak
-///   ordering](https://simple.wikipedia.org/wiki/Strict_weak_ordering)
-///   over the elements of `self`.
+  /// - Precondition: `areInIncreasingOrder` is [a strict weak
+  ///   ordering](https://simple.wikipedia.org/wiki/Strict_weak_ordering)
+  ///   over the elements of `self`.
 ```
 
 We don't normally add examples to our documentation—it makes
@@ -1005,8 +1011,8 @@ the summary could have avoided swapping elements in the comparison and
 negating the result:
 
 ```swift
-/// Sorts the elements so that `areInOrder(self[i],
-/// self[i+1])` is true for each `i` in `0 ..< length - 2`.
+  /// Sorts the elements so that `areInOrder(self[i],
+  /// self[i+1])` is true for each `i` in `0 ..< length - 2`.
 ```
 
 If we view a strict weak ordering as a generalization of what `<` does, the
@@ -1031,29 +1037,28 @@ Therefore, if we have a sorting implementation that works with any
 strict weak order, we can easily convert it to work with any total
 preorder by passing the predicate through `converseOfComplement`.
 
-
 Note that the name of the predicate became simpler: it no longer tests
 that its arguments represent an _increase_.  Instead, it tells us
 whether the order is correct.  Because the summary is no longer
 tricky, we can drop the example, and we're left with this:
 
 ```swift
-/// Sorts the elements so that `areInOrder(self[i],
-/// self[i+1])` is true for each `i` in `0 ..< length - 2`.
-///
-/// - Precondition: `areInOrder` is a [total
-///   preorder](https://en.wikipedia.org/wiki/Weak_ordering#Total_preorders)
-///   over the elements of `self`.
-/// - Complexity: at most N log N comparisons, where N is the number
-///   of elements.
-mutating func sort<T>(areInOrder: (T, T)->Bool) { ... }
+  /// Sorts the elements so that `areInOrder(self[i],
+  /// self[i+1])` is true for each `i` in `0 ..< length - 2`.
+  ///
+  /// - Precondition: `areInOrder` is a [total
+  ///   preorder](https://en.wikipedia.org/wiki/Weak_ordering#Total_preorders)
+  ///   over the elements of `self`.
+  /// - Complexity: at most N log N comparisons, where N is the number
+  ///   of elements.
+  mutating func sort<T>(areInOrder: (T, T)->Bool) { ... }
 ```
 
 But we can go further and use a much simpler and more natural summary:
 
 ```swift
-/// Sorts the elements so that all adjacent pairs satisfy
-/// `areInOrder`.
+  /// Sorts the elements so that all adjacent pairs satisfy
+  /// `areInOrder`.
 ```
 
 Usually, the less our documentation looks like code (without
@@ -1084,13 +1089,13 @@ precondition there without overly complicating it, making the final
 declaration:
 
 ```swift
-/// Sorts the elements so that all adjacent pairs satisfy the [total
-/// preorder](https://en.wikipedia.org/wiki/Weak_ordering#Total_preorders)
-/// `areInOrder`.
-///
-/// - Complexity: at most N log N comparisons, where N is the number
-///   of elements.
-mutating func sort<T>(areInOrder: (T, T)->Bool) { ... }
+  /// Sorts the elements so that all adjacent pairs satisfy the [total
+  /// preorder](https://en.wikipedia.org/wiki/Weak_ordering#Total_preorders)
+  /// `areInOrder`.
+  ///
+  /// - Complexity: at most N log N comparisons, where N is the number
+  ///   of elements.
+  mutating func sort<T>(areInOrder: (T, T)->Bool) { ... }
 ```
 
 There is one factor we haven't considered in making these changes:
@@ -1106,10 +1111,10 @@ contract is an engineering decision you will have to make. To reduce
 the risk you could add this assertion[^checks], which will stop the program if
 the ordering is strict-weak:
 
-```
-precondition(
-  self.isEmpty || areInOrder(first!, first!),
-  "Total preorder required; did you pass a strict-weak ordering?")
+```swift
+  precondition(
+    self.isEmpty || areInOrder(first!, first!),
+    "Total preorder required; did you pass a strict-weak ordering?")
 ```
 
 [^checks]: See the next chapter for more on checking contracts at
@@ -1158,7 +1163,6 @@ For example,
 > - Document the performance of every operation that doesn't execute in
 >   constant time and space.
 
-
 It is reasonable to put information in the policies without which the
 project's other documentation would be incomplete or confusing, but
 you should be aware that it implies policies *must be read*. We
@@ -1288,7 +1292,7 @@ to promise more efficiency, but never weakened.
 
 ## Polymorphism and Higher-Order Functions
 
-Similar rules apply to the contracts for protocol conformances: a
+Similar rules apply to the contracts for protocol conformance: a
 method satisfying a protocol requirement can have weaker preconditions
 and/or stronger postconditions than required by the protocol: