The specification currently provides a DECLARE form that lives inside a
procedure body:
(define (f x)
(declare ...declare-forms...)
... body ...)
This form is misnamed. Let me try to explain the intention so that
people will have a sense what it is for. Here are some examples of
DECLARE-FORMS:
inline -- procedure is to be inlined wherever possible
(measure fn) -- "fn" is a "measure function" that should be
used by the prover to show that this procedure
terminates
emit -- this procedure is referenced by the run time system
or by assembly code. It should be emitted even if
reachability analysis suggests that it is not actually
called.
no-emit -- this procedure is not referenced by the actual
program, and should not be emitted by the code
generator. This is useful when a procedure exists
to support proof rather than execution. For example,
measure functions are often annotated this way.
pure -- this procedure is deeply non-mutating and terminating.
This implies that the prover can safely assume that
any state created by this procedure is non-escaping,
and that the only modification to state resulting from
a call to this procedure is the return value.
The compiler is obligated to check these properties.
logic -- this procedure is purely functional, terminating,
and does not reference mutable variables or fields.
This implies that it can be evaluate by pure term
substitution, and that the execution has no effect
on the state of the program other than its return
value.
The compiler is obligated to check these properties.
entry -- this procedure is an entry point to the program.
This annotation is primarily useful in the kernel
where BitC procedures are called from assembly
language.
(guard expr) -- EXPR is an expression that should always
return true. From the "callee" perspective, a
guard is taken as an assertion that the expression's
validity can be assumed. From the "caller" perspective,
the guard is a proof obligation that must be
discharged at every call site.
A guard expression must reference only LOGIC procedures
and parameters.
?? This is borrowed from ACL2, and I am wondering if
it should be generalized to pre- and post-conditions ??
Note that the annotations PURE and LOGIC are both things that should be
discovered by the compiler automatically. The purpose of providing a
means of declaring them is to alert the compiler about programmer
intention so that the constraints can be checked.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
