On Friday, 17 October 2014 at 10:50:54 UTC, Ola Fosheim Grøstad
wrote:
On Friday, 17 October 2014 at 10:30:14 UTC, eles wrote:
On Friday, 17 October 2014 at 09:46:49 UTC, Ola Fosheim
Grøstad wrote:
Nice idea, but how to persuade libraries to play that game?
1. Provide a meta-language for writing propositions that
describes what libraries do if they are foreign (pre/post
conditions). Could be used for "asserts" too.
That's complicated, to provide another langage for describing the
behavior. And how? Embedded in the binary library?
Maybe a set of annotations that are exposed through the .di
files. But, then, we are back to headers...
Another idea would be to simply make the in and out contracts of
a function exposed in the corresponding .di file, or at least a
part of them (we could use "public" for those).
Anyway, as far as I ca imagine it, it would be like embedding
Polyspace inside the compiler and stub functions inside libraries.
2. Provide a C compiler that compiles to the same internal
representation as the new language, so you can run the same
analysis on C code.
For source code. But for cloused-source libraries?
3. Remove int so that you have to specify the range and make
typedefs local to the library
Pascal arrays?
Lots of opportunities for improving "state-of-the-art".
True. But a lot of problems too. And there is not much agreement
on what is the state of the art...
