diff --git a/.vscode/settings.json b/.vscode/settings.json index c03803f..f746685 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -6,5 +6,11 @@ } ], "rewrap.autoWrap.enabled": true, - "rewrap.wrappingColumn": 80 + "rewrap.wrappingColumn": 80, + "cSpell.words": [ + "footgun", + "Gitter", + "irreflexivity", + "preorder" + ] } diff --git a/README.md b/README.md index 27e4924..86df1ce 100644 --- a/README.md +++ b/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 ``` diff --git a/better-code/README.md b/better-code/README.md index 1125d25..04e0659 100644 --- a/better-code/README.md +++ b/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: diff --git a/better-code/book.toml b/better-code/book.toml index 5bd576a..8b92e3c 100644 --- a/better-code/book.toml +++ b/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] + diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md index 381114f..e26d762 100644 --- a/better-code/src/chapter-2-contracts.md +++ b/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$. + + 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,13 +181,13 @@ 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 @@ -192,7 +195,7 @@ The following—more useful—triples will help illustrate the sequencing rule: // 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 +> *…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 – contracts.* > -> —Building bug-free O-O software: An Introduction to Design by Contract™ -> https://www.eiffel.com/values/design-by-contract/introduction/ +> — Building bug-free O-O software: An Introduction to Design by Contract™ +> 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) +> —Alexander Stepanov () 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. + + _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(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(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(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(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: