OpenE2K/rust
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Clarify docs about claim

Browse Source
This commit is contained in:
Tim Chevalier 2011-06-28 17:47:49 -07:00
parent 5059c5f8fd
commit 8c757fcd40
1 changed files with 6 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
doc/rust.texi
View File

@ -3641,14 +3641,12 @@ that is not actually checked at runtime. Thus, using a @code{claim} implies a
proof obligation to ensure---without compiler assistance---that an assertion
always holds.
With a command-line flag, the compiler can turn all @code{claim} expressions
into @code{check} expressions, but the default is to not check the assertion
contained in a @code{claim}.
The idea is to use @code{check} during development, with @code{claim}
providing the freedom to disable a few runtime checks in performance-critical
locations once code is debugged, while leaving the @code{claim} expressions in
the code as documentation.
Setting a runtime flag can turn all @code{claim} expressions
into @code{check} expressions in a compiled Rust program, but the default is to not check the assertion
contained in a @code{claim}. The idea behind @code{claim} is that performance profiling might identify a
few bottlenecks in the code where actually checking a given callee's predicate
is too expensive; @code{claim} allows the code to typecheck without removing
the predicate check at every other call site.
@node Ref.Expr.IfCheck
@subsection Ref.Expr.IfCheck