Re: Appetite for Frama-C annotations?

On 12/07/21 13:32, Colin Gilbert wrote:
> I've been becoming more and more interested in learning formal methods
> and wanted to find a good project to which I could contribute. Would
> the development team appreciate someone adding ACSL annotations to the
> codebase?

My ears perked up ... I have some Frama-C-related notes-to-self from
a couple years ago that I've not yet pursued, with an interest in how
useful they could be in the hairy mess of the PL/Java extension.

Right at the moment, I am more invested in a somewhat massive
refactoring of the extension. In one sense, tackling the refactoring
without formal tools feels like the wrong order (or working without a net).
It's just that there are only so many hours in the day, and the
refactoring really can't wait, given the backlog of modern capabilities
(like polyglot programming) held back by the current structure. And the
code base should be less hairy afterward, and maybe more amenable to
spec annotations.

According to OpenHub, PL/Java's implementation is currently 74% Java,
19% C. A goal of the current refactoring is to skew that ratio more
heavily Java, with as little C glue remaining as can be achieved.
Meaning, ultimately, a C-specific framework like Frama-C isn't where
most of the fun would be in PL/Java. Still, I'd be interested to see it
in action.

Regards,
-Chap