Boogie Grammar

Apr 5, 2013 at 1:10 AM
Hi,
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 s.th. that is "really" compatible.
-Martin
Apr 5, 2013 at 1:13 AM
Yes, the Boogie grammar is recorded in the Coco parser-generator file Source/Core/BoogiePL.atg.

Rustan
Apr 7, 2013 at 6:33 AM
Edited Apr 8, 2013 at 11: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 1: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 4: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 8, 2013 at 12:01 AM
Edited May 8, 2013 at 12:33 AM
Now, I have a parser that follows http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf. 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?