Merge pull request #37 from stlab/sean-parent/contracts-cleanup-2

Refine contracts chapter and update config files

Author: sean-parent

.vscode/settings.json

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

better-code/book.toml

@@ -19,3 +19,6 @@ enable = true
 
 [output.html.print]
 enable = true
+
+[preprocessor.katex]
+

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

@@ -142,6 +142,8 @@ Hoare used this notation, called a “Hoare triple,”
 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):
@@ -156,7 +158,7 @@ For example:
 What makes preconditions and postconditions useful for formal proofs
 is this *sequencing rule*:
 
-> {P}S{Q} ∧ {Q}T{R} ⇒ {P}S;T{R}
+> {P}S{Q} ^ {Q}T{R} => {P}S;T{R}
 
 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
@@ -327,7 +329,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
@@ -716,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
@@ -805,10 +807,10 @@ What are the preconditions for removing an element?  Obviously, there
 needs to be an element to remove.
 
 ```swift
-  /// Removes and returns the last element.
-  ///
-  /// - Precondition: `self` is non-empty.
-  public mutating func popLast() -> T { ... }
+/// Removes and returns the last element.
+///
+/// - Precondition: `self` is non-empty.
+public mutating func popLast() -> T { ... }
 ```
 
 A client of this method is considered to have a bug unless
@@ -821,25 +823,25 @@ has a bug.  The bug could be in the documentation of course, *which is
 a part of the method*.
 
 ```swift
-  /// Removes and returns the last element.
-  ///
-  /// - 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 { ... }
+/// Removes and returns the last element.
+///
+/// - 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 { ... }
 ```
 
 The invariant of this function is the rest of the elements, which are
 unchanged:
 
 ```swift
-  /// Removes and returns the last element.
-  ///
-  /// - Precondition: `self` is non-empty.
-  /// - 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 { ... }
+/// Removes and returns the last element.
+///
+/// - Precondition: `self` is non-empty.
+/// - 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 { ... }
 ```
 
 Now, if the postcondition seems a bit glaringly redundant with the
@@ -866,10 +868,10 @@ invariant is also trivially implied.  And that is also very commonly
 omitted.
 
 ```swift
-  /// Removes and returns the last element.
-  ///
-  /// - Precondition: `self` is non-empty.
- public mutating func popLast() -> T { ... }
+/// Removes and returns the last element.
+///
+/// - Precondition: `self` is non-empty.
+public mutating func popLast() -> T { ... }
 ```
 
 In fact, the precondition is implied by the summary too.  You
@@ -887,8 +889,8 @@ you are going to remove the last element, so the original declaration
 should be sufficient:
 
 ```swift
-  /// Removes and returns the last element.
- public mutating func popLast() -> T { ... }
+/// Removes and returns the last element.
+public mutating func popLast() -> T { ... }
 ```
 
 In practice, once you are comfortable with this discipline, the
@@ -931,12 +933,14 @@ 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).
 A strict weak ordering has both of these properties, among others.
@@ -983,19 +987,19 @@ essential information—but because the statement of effects is tricky,
 this is a case where an example might really help.
 
 ```swift
-  /// Sorts the elements so that `areInIncreasingOrder(self[i+1],
-  /// self[i])` is false for each `i` in `0 ..< length - 2`.
-  ///
-  ///     var a = [7, 9, 2, 7]
-  ///     a.sort(areInIncreasingOrder: <)
-  ///     print(a)     // prints [2, 7, 7, 9]
-  ///
-  /// - Precondition: `areInIncreasingOrder` is [a strict weak
-  ///   ordering](https://simple.wikipedia.org/wiki/Strict_weak_ordering)
-  ///   over the elements of `self`.
-  /// - Complexity: at most N log N comparisons, where N is the number
-  ///   of elements.
-  mutating func sort(areInIncreasingOrder: (Element, Element)->Bool) { ... }
+/// Sorts the elements so that `areInIncreasingOrder(self[i+1],
+/// self[i])` is false for each `i` in `0 ..< length - 2`.
+///
+///     var a = [7, 9, 2, 7]
+///     a.sort(areInIncreasingOrder: <)
+///     print(a)     // prints [2, 7, 7, 9]
+///
+/// - Precondition: `areInIncreasingOrder` is [a strict weak
+///   ordering](https://simple.wikipedia.org/wiki/Strict_weak_ordering)
+///   over the elements of `self`.
+/// - Complexity: at most N log N comparisons, where N is the number
+///   of elements.
+mutating func sort<T>(areInIncreasingOrder: (T, T)->Bool) { ... }
 ```
 
 #### Letting Simplicity Drive Design
@@ -1033,7 +1037,6 @@ 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
@@ -1108,7 +1111,7 @@ 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:
 
-```
+```swift
 precondition(
   self.isEmpty || areInOrder(first!, first!),
   "Total preorder required; did you pass a strict-weak ordering?")
@@ -1160,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