From 8c757fcd4063601279332806a52d13fcfbf6f04c Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Tue, 28 Jun 2011 17:47:49 -0700 Subject: [PATCH] Clarify docs about claim --- doc/rust.texi | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/doc/rust.texi b/doc/rust.texi index 6274528c863..cc8848088f4 100644 --- a/doc/rust.texi +++ b/doc/rust.texi @@ -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