Forwarded from coyotos-dev.
-------- Forwarded Message --------
From: Constantine Plotnikov <[EMAIL PROTECTED]>
Reply-To: Coyotos development discussions <[email protected]>
To: Coyotos development discussions <[email protected]>
Subject: [coyotos-dev] BitC: annotation framework
Date: Thu, 27 Jan 2005 19:54:21 +0600
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
_______________________________________________
coyotos-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/coyotos-dev
_______________________________________________
bitc-dev mailing list
[EMAIL PROTECTED]
http://www.coyotos.org/mailman/listinfo/bitc-dev
