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 <c...@anastigmatix.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
