Update Kani Book #3474

carolynzech · 2024-08-30T20:25:44Z

Add the following to the book:

Reference section on contracts. The point of this section is not to be an exhaustive explanation--we have good documentation on contracts already, and we don't want to maintain it in two places. The goal of the section is to give readers an intuition for the main idea and then direct them to more detailed resources.
Add a reference to the blog--it's a good resource to learn about Kani and it would be nice to have an easier way to find it. Inspired by this post.
Move the crates documentation earlier. This partly addresses #3029 by at least making our crates documentation more visible in the book. (I don't have this PR as resolving that issue, since we would need to actually publish the docs on crates.io to do that.)

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

docs/src/getting-started.md

docs/src/reference/experimental/contracts.md

zhassan-aws

Thank you!

carolynzech added 2 commits August 30, 2024 16:17

contracts section; move crates docs

0d849bd

add recursion attribute

96019c9

carolynzech marked this pull request as ready for review August 30, 2024 20:50

carolynzech requested a review from a team as a code owner August 30, 2024 20:50

celinval assigned zhassan-aws Sep 3, 2024

zhassan-aws reviewed Sep 3, 2024

View reviewed changes

address feedback

b99d368

carolynzech requested a review from zhassan-aws September 4, 2024 00:24

fix typo

5f45ab8

zhassan-aws approved these changes Sep 4, 2024

View reviewed changes

Merge branch 'main' into update-docs

b5d8532

carolynzech enabled auto-merge September 4, 2024 01:03

carolynzech added this pull request to the merge queue Sep 4, 2024

Merged via the queue into model-checking:main with commit edded56 Sep 4, 2024
27 checks passed

carolynzech deleted the update-docs branch September 4, 2024 02:46

Provide feedback