Skip to content

Commit

Permalink
Fix URLs to generate correct HTML (#19)
Browse files Browse the repository at this point in the history
  • Loading branch information
atomb authored Dec 6, 2023
1 parent 4d09097 commit 5a099be
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion _includes/brittleness.html
Original file line number Diff line number Diff line change
Expand Up @@ -517,7 +517,7 @@ <h2 id="sec-what-is-brittleness" class="h1" data-line="18" data-heading-depth="1
<li class="li ul-li list-star-li compact-li" data-line="264"><span data-line="264"></span>Isolate each step so that the proof of it doesn’t need to (and, further, isn’t able to) take into account irrelevant information. This limits the number of choices that the prover has to evaluate when making each reasoning step.
</li></ul>

<p class="p noindent" data-line="266"><span data-line="266"></span>A nice coincidence is that programs written according to these principles tend to be easier to read, as well. Reducing the work a prover needs to do when reasoning about a program has the effect of reducing the amount of thinking a human has to do to understand what a program does, and why it’s correct. Constructing small, relatively isolated components relates strongly to the concepts of<span data-line="266"></span>&nbsp;<a href="https://en.wikipedia.org/wiki/Cohesion_(computer_science">cohesion</a><span data-line="266"></span>) and<span data-line="266"></span>&nbsp;<a href="https://en.wikipedia.org/wiki/Coupling_(computer_programming">coupling</a><span data-line="266"></span>) used in software engineering.
<p class="p noindent" data-line="266"><span data-line="266"></span>A nice coincidence is that programs written according to these principles tend to be easier to read, as well. Reducing the work a prover needs to do when reasoning about a program has the effect of reducing the amount of thinking a human has to do to understand what a program does, and why it’s correct. Constructing small, relatively isolated components relates strongly to the concepts of<span data-line="266"></span>&nbsp;<a href="https://en.wikipedia.org/wiki/Cohesion_%28computer_science%29">cohesion</a><span data-line="266"></span> and<span data-line="266"></span>&nbsp;<a href="https://en.wikipedia.org/wiki/Coupling_%28computer_programming%29">coupling</a><span data-line="266"></span> used in software engineering.
</p>
<p class="p indent" data-line="268"><span data-line="268"></span>Those principles are rather general, however, and there are several more specific guidelines for how to apply them in practice in Dafny.
</p>
Expand Down
2 changes: 1 addition & 1 deletion assets/mdk/brittleness.mdk
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ The examples covered so far illustrate two key principles for maintainable verif
* Break long leaps of reasoning down into smaller steps. This limits the number of reasoning steps that the prover needs to construct on its own.
* Isolate each step so that the proof of it doesn’t need to (and, further, isn’t able to) take into account irrelevant information. This limits the number of choices that the prover has to evaluate when making each reasoning step.

A nice coincidence is that programs written according to these principles tend to be easier to read, as well. Reducing the work a prover needs to do when reasoning about a program has the effect of reducing the amount of thinking a human has to do to understand what a program does, and why it’s correct. Constructing small, relatively isolated components relates strongly to the concepts of [cohesion](https://en.wikipedia.org/wiki/Cohesion_(computer_science)) and [coupling](https://en.wikipedia.org/wiki/Coupling_(computer_programming)) used in software engineering.
A nice coincidence is that programs written according to these principles tend to be easier to read, as well. Reducing the work a prover needs to do when reasoning about a program has the effect of reducing the amount of thinking a human has to do to understand what a program does, and why it’s correct. Constructing small, relatively isolated components relates strongly to the concepts of [cohesion](https://en.wikipedia.org/wiki/Cohesion_%28computer_science%29) and [coupling](https://en.wikipedia.org/wiki/Coupling_%28computer_programming%29) used in software engineering.

Those principles are rather general, however, and there are several more specific guidelines for how to apply them in practice in Dafny.

Expand Down

0 comments on commit 5a099be

Please sign in to comment.