[coyotos-dev] BitC: annotation framework

Constantine Plotnikov 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 
data structures.

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:

(mutual-recursion
 (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)))))))

Constantine




More information about the coyotos-dev mailing list