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/better-code/book.toml b/better-code/book.toml index f626b05..8b92e3c 100644 --- a/better-code/book.toml +++ b/better-code/book.toml @@ -19,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..7bc3e94 100644 --- a/better-code/src/chapter-2-contracts.md +++ b/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*. + + 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 @@ -715,7 +717,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 @@ -804,10 +806,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 @@ -820,25 +822,25 @@ 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 @@ -865,10 +867,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 @@ -886,8 +888,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 @@ -929,12 +931,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. + + _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. @@ -981,19 +985,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: (T, T)->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(areInIncreasingOrder: (T, T)->Bool) { ... } ``` #### Letting Simplicity Drive Design @@ -1031,7 +1035,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 @@ -1106,7 +1109,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?") @@ -1158,7 +1161,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