Boogie Grammar

Apr 5, 2013 at 12:10 AM
Is there a grammar for Boogie readable by some parser generator? Didn't find it in the repository. I'm building a tool in Java which takes Boogie as input and I don't want to come up with yet another IVL, but writting the grammar by hand is somehow painful as well. So it would be cool to have that is "really" compatible.
Apr 5, 2013 at 12:13 AM
Yes, the Boogie grammar is recorded in the Coco parser-generator file Source/Core/BoogiePL.atg.

Apr 7, 2013 at 5:33 AM
Edited Apr 8, 2013 at 10:50 PM
Great, thanks. Doesn't work with Java right away. Seems to be due to the "out" keyword. How stable is the Grammar? Does it make sense to invest a few hours to modify it for Java, or will there be big changes in the near future?
Apr 24, 2013 at 12:20 AM
The grammar is pretty stable. But, if you want to change the .atg file so that it instead produces Java, I would have expected many more changes than just out-parameters. Moreover, what would be a good rewrite of the code in Java without out-parameters?
Apr 24, 2013 at 3:42 AM
Well, yes there would be a lot of work to make it work with Java. Anyway, we borrowed a JavaCC grammar from Freiburg, which is now in the Joogie repository in case you are interested.
May 7, 2013 at 11:01 PM
Edited May 7, 2013 at 11:33 PM
Now, I have a parser that follows But it disagrees with Boogie on the following line:

I generate:

const unique java.lang.SecurityManager : JavaType <: unique java.lang.Object complete;

Boogie wants it be

const unique java.lang.SecurityManager : JavaType extends unique java.lang.Object complete;

Can I safely assume that "<:" is now called "extends"?

PS: mod ("%") is not accepted either. What should I use instead?