Chapter 1 edits #26
Draft
Chapter 1 edits #26
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- use a similar version for slices and arrays (could be confusing otherwise what kind of binary search we are talking about) - i omitted the ghost idx - unfortunately we then only have the found ==> ... case - updated overflow and termination section which refer to this example Another option would be to move the binary section after introducing ghost and pure, as a separate "case study". Then the loop section would need some other example that is explained more.
people might be already familiar with the BinarySearch function from the slice package in Go's standard library. Returning found and index also allows us to write postconditions for both cases (element contained / not contained) changed sections that refer to this example
- add note about triggers - added empty page for the advanced section - introduce implication together do not really have a meaningful `forall` example without arrays, and the need to contrains indices. Of course, one could show mathematical things like `forall i int :: - i * i >= 0` but then we would neglect overflow again - example for existential quantifier tried to explain why we should not use them can complete the example in the loop section
example with a linear search now showing both found/not found cases might have small overlap with binary search section show the errors not established / preserved with very trivial mistakes also important: invariants must not hold when exiting abnormally (e.g. break or return) and only after an iteration
better to reuse the already familiar example than to introduce a new example. `almostMax` anyways bad with only the postcondition res >= arr[i] Otherwise would also return an index (possibly ghost?)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.