Re: Appetite for Frama-C annotations?

Hi! Thanks for the quick reply. Are you doing any of this work in a
public repository? If so, could we have a link? There is a similar
idea in Java Modelling Language. It also uses its own annotations to
describe additional requirements. Are you considering to use it? Maybe
I could help...

On Wed, 8 Dec 2021 at 16:02, Chapman Flack <chap(at)anastigmatix(dot)net> wrote:
>
> 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