Mutation, references, and borrowing documentation #1706
Conversation
…requires and ensures with mutable references AND asserts containing mutable references
| {{#include ../../../../examples/guide/references.rs:immut}} | ||
| ``` | ||
|
|
||
| Verus only support the use of mutable references as arguments to a function, such as in the following example. |
There was a problem hiding this comment.
"only support" -> "only supports" and perhaps "Verus only" -> "Currently Verus only"
| {{#include ../../../../examples/guide/references.rs:mut}} | ||
| ``` | ||
|
|
||
| Given that the pieces of memory to which mutable references point can be modified during function calls, we need a particular way to talk about their old and updated in Verus spec code, particularly in the `requires` and `ensures` of functions and in `assert`. |
There was a problem hiding this comment.
I might phrase this as:
about their old and updated values in Verus spec code, particularly in function
requiresandensuresclauses, and inassertstatements.
| // ANCHOR_END: immut | ||
| } | ||
|
|
||
| // ANCHOR: mut |
There was a problem hiding this comment.
Stylistically, we generally sort functions such that callees precede callers, so in this case, that would mean putting modify_y before mutable_example.
| *a = *a + 1; | ||
| assert(*a == 1); | ||
| *a = *a + 1; | ||
| assert(*a == 2); |
There was a problem hiding this comment.
Maybe we could add another copy of assert(*old(a) == 0); in here to emphasize that old refers to the value at the very beginning of the function, not to the value right before the last update.
|
Implemented suggestions :) |
In the main document, I succinctly describe ownership, references, and borrowing in Rust, while also linking the official Rust documentation that contains more examples. Then, I shortly explain how to use mutable references in requires, ensures, and assert, while providing simple and more complex examples.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.