[coyotos-dev] BitC: annotation framework
cap at isg.axmor.com
Thu Jan 27 08:54:21 EST 2005
I suggest to introduce a code annotation framework for BitC (like one
used in C# and Java 1.5). I see the following benefits:
1. Source code might be annotated with verifiable or externally
referenced assertions. For example pointer variable might be annotated
with assertion that referenced location is not referenced anywhere else.
This might be very useful for generating proofs as tools are usually
no-so-good at discovering assertions that are obvious to the programmer.
2. Source code analysis tools may look for specific annotations in the
code and gather statistic.
3. These annotations might be used to generate additional code (for
example CapIDL) by other tools basing on the source code.
4. These annotations might be used to give platform dependent hints to
compiler (for example to disable or enable some specific optimization or
to use one of call conventions). Or they maybe used control layout of
5. These annotations might be used to create references to related
standards and specifications.
6. Annotations might give hints to type inference engine. BTW the
current syntax for type annotations is a bit out of the line from the
rest as it does not use (S-expressions).
I do not know what annotation syntax would look best for BitC. My
current idea is to use allow (@ <annotation list> ) at start of the any
construct. I think that annotations should be declared explicitly by
some constructs. For example of proposed annotation usage:
(define ((@ (finite-recursion-by 1)) odd x)
(if (< x 0)
(odd (- x))
(not (even (- x 1)))))
(define ((@ (finite-recursion-by 1)) even x)
(cond ((= x 0) #t)
((< x 0) (even (- x)))
(#t (not (odd (- x 1)))))))
More information about the coyotos-dev