Contracts Cleanup #25
Conversation
Made a pass fixing spelling, math expressions (added ketex - see README), made indentation more consistent, removed non-ascii characters in favor of entities, and changed links to markdown format so they can be clicked in the generated docs.
| Hoare used this notation, called a “Hoare triple,” | ||
|
|
||
| > {P}S{Q} | ||
| > $\{P\}S\{Q\}$ |
There was a problem hiding this comment.
This is objectively harder to read, but as I said I'm OK with changes like this because the math will be formatted better. That said, the use of > was a “I'm doing my best with plain Markdown”-ism. Is there a more appropriate way to set this equation off? I guess “it's a quotation” still applies here…
There was a problem hiding this comment.
Note also the curlies are missing from the GitHub preview of this file in all the places surrounded by $…$. I don't know if they show up when rendered by mdbook…
| 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. --> |
There was a problem hiding this comment.
I agree in principle, and I even tried to do that, but when I looked at the preview the many transitions between gray and white backgrounds wasn't great. I realize that can be fixed with a stylesheet… but also, I think the Markdown processor forced me to add space next to the backticks that made the thing read differently from Hoare's notation. And that certainly is the case with your version. If the argument for math notation is that it's going to be easier to read, I don't think we're winning (yet).
It possibly might be better to get the book written and then take a holistic approach to math. It might be that we want to convert the entire thing to LaTeX, for example. Just a thought. More generally, let's make sure we account for the engineering tradeoffs in our approach.
| is this *sequencing rule*: | ||
|
|
||
| > {P}S{Q} ∧ {Q}T{R} ⇒ {P}S;T{R} | ||
| > $\{P\}S\{Q\} \wedge \{Q\}T\{R\} \Rightarrow \{P\}S;T\{R\}$ |
There was a problem hiding this comment.
We definitely want good math output for final production, but for the purposes of just reading and reviewing the text and changes, I really don't like the engineering cost I can't easily verify that it means what I originally wrote (and as noted elsewhere GitHub doesn't render the curlies so can't verify that way).
| > All undocumented software is waste. It's a liability for a company. | ||
| > | ||
| > —Alexander Stepanov (https://youtu.be/COuHLky7E2Q?t=1773) | ||
| > — Alexander Stepanov (<https://youtu.be/COuHLky7E2Q?t=1773>) |
There was a problem hiding this comment.
You added a space after the dash. I don't think that's how this is done (non-authoritative citation).
| > — Alexander Stepanov (<https://youtu.be/COuHLky7E2Q?t=1773>) | |
| > —Alexander Stepanov (<https://youtu.be/COuHLky7E2Q?t=1773>) |
| 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. --> |
There was a problem hiding this comment.
I think you may have some valid points here but too many complaints and a little to diffuse to deal with here; let's chat in person.
There was a problem hiding this comment.
I do think "deterministic" is a better word than "stable".
| precondition that can't be efficiently checked. Even if we could assume the | ||
| comparison is stable, to do so would | ||
| require at least $n^2$ comparisons, where $n$ is the number of |
There was a problem hiding this comment.
| precondition that can't be efficiently checked. Even if we could assume the | |
| comparison is stable, to do so would | |
| require at least $n^2$ 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 |
| 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 |
There was a problem hiding this comment.
| predicate at least has to be stable. To leave elements meaningfully | |
| predicate at least has to be deterministic. To leave elements meaningfully |
| /// - 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 |
There was a problem hiding this comment.
What's the rationale for these spaces? I don't see how they're helpful. Personally I think they look quite awkward in the rendered output.
|
@sean-parent ping. |
2 participants
Fixed spelling, math expressions (added ketex - see README), made indentation more consistent, removed non-ascii characters in favor of entities, and changed links to markdown format so they can be clicked in the generated docs.