Skip to content
Snippets Groups Projects
Verified Commit e83196f8 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

adapt docs

parent 2e378abb
No related branches found
No related tags found
1 merge request!65Introduce params for args automatically
Pipeline #116542 passed
......@@ -20,12 +20,25 @@ The `params` clause specifies a universally-quantified parameter of the specific
The `args` clause specifies the refinement and (optionally) a type for the single argument `x` of the function.
RefinedRust infers a "default" type for the argument from Rust's type, but this can also be overridden by providing an explicit type after a `@`.
For instance, the clause `#[rr::args("z" @ "int i32")]` would be equivalent to the one specified above.
In addition, for types (like structs) with invariants declared on them, the argument can be prefixed with `#raw` in order to not require the invariant on them to hold (e.g. `#[rr::args("z", #raw "-[#x]")]`).
In addition, for types (like structs) with invariants declared on them, the argument can be prefixed with `#raw` in order to not require the invariant on them to hold (e.g. `#[rr::args("z", #raw "-[x]")]`).
The `requires` clause specifies the requirement that the result of the addition fits into an `i32` (see [RefinedRust propositions](#refinedrust-propositions) for details on the syntax).
Finally, the `returns` clause specifies a refinement (and optionally, a type) for the return value of the function.
### Shortcut attributes
As an alternative to specifying the refinement for arguments explicitly, we can also let RefinedRust automatically introduce a parameter for them.
If the `rr::args` clause is missing, RefinedRust will automatically introduce one parameter for every argument, named after the Rust variable name, and assume that the arguments are refined accordingly.
For instance, we can equivalently specify the `add_42` as:
```rust
#[rr::requires("x + 42 ∈ i32")]
#[rr::returns("x + 42")]
fn add_42(x : i32) -> i32 {
x + 42
}
```
For mutable reference arguments `x`, you can use the notations `x.cur` and `x.ghost` to refer to the references current value and ghost variable, respectively.
| Keyword | Purpose | Properties | Example |
|-----------|------------------------------|------------|----------------------------------|
......@@ -43,7 +56,7 @@ Finally, the `returns` clause specifies a refinement (and optionally, a type) fo
There are further attributes that influence the proof-checking behaviour:
| Keyword | Purpose | Properties | Example |
|-----------|------------------------------|------------|----------------------------------|
| `verify` | Tell RefinedRust to verify this function with the default specification | none | `#[rr::verify]` |
| `verify` | Tell RefinedRust to verify this function with the default specification | none | `#[rr::verify]` |
| `trust_me` | generate and type-check the specification and code, but do not generate a proof | none | `#[rr::trust_me]` |
| `only_spec` | only generate and type-check the specification, but do not generate the code | none | `#[rr::only_spec]` |
| `skip` | ignore annotations on this function completely | none | `#[rr::skip]` |
......
......@@ -161,18 +161,18 @@ This is why we have marked `add` as unsafe.
For `add` we take the following specification:
```
#[rr::params("x", "γ")]
#[rr::args(#raw "(#(-[#x]), γ)")]
#[rr::args(#raw "((-[x]), γ)")]
#[rr::requires("(x + 1 ≤ MaxInt i32)%Z")]
#[rr::observe("γ": "(-[#(x+1)%Z] : plist place_rfn _)")]
```
The first noteworthy part is the `#raw` annotation on the first argument: it asserts that we do not require the invariant on `EvenInt` to currently hold.
That is why we also use `-[#x]` for the contents of the mutable reference, which is the "raw" refinement for the struct (where `x` is the refinement of the first field) without the annotated invariant.
That is why we also use `-[x]` for the contents of the mutable reference, which is the "raw" refinement for the struct (where `x` is the refinement of the first field) without the annotated invariant.
As we add 1, we require that `x + 1` fits into a `i32` integer.
For `add_two`, we add the following specification:
```
#[rr::params("x", "γ")]
#[rr::args("(#x, γ)")]
#[rr::args("(x, γ)")]
#[rr::requires("(x + 2 ≤ MaxInt i32)%Z")]
#[rr::observe("γ": "(x+2)")]
```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment