Skip to content

Commit

Permalink
Add link to invariants in Kani
Browse files Browse the repository at this point in the history
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
  • Loading branch information
feliperodri committed Aug 27, 2024
1 parent f5f426f commit 7d0b5bd
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/src/challenges/0009-duration.md
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ pub const fn new(secs: u64, nanos: u32) -> Duration {

### Success Criteria

Write a type invariant for the struct `Duration`. Write function contracts for the following public functions.
Write a [type invariant](https://model-checking.github.io/kani/crates/doc/kani/derive.Invariant.html) for the struct `Duration`. Write function contracts for the following public functions.

1. `Duration::new(secs: u64, nanos: u32) -> Duration`
2. `Duration::from_secs(secs: u64) -> Duration`
Expand Down

0 comments on commit 7d0b5bd

Please sign in to comment.