How usable is BCT?

Jun 23, 2010 at 3:33 PM
Hi, How usable is the BCT tool currently? Regards, Matthijs ter Woord
Coordinator
Jun 23, 2010 at 8:05 PM

The new bytecode translator, BCT, is currently not usable.  However, we have recently started an effort to flesh out the MSIL-to-Boogie translation it does.  If you're interested in contributing, let me know.

  Rustan

Jun 24, 2010 at 9:31 AM

I looked into Boogie before, and especially the Boogie language is quite complicated, and not really well documented. I only found 1 PDF file, but that file didn't have a correct PDF TOC in it, so navigating was really hard.

If there's any good information, I would consider contributing to this project.

 

Coordinator
Jun 29, 2010 at 2:30 AM

The Boogie language is documented in the Boogie language reference manual, "This is Boogie 2", http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf.  It is slightly out of date (for example, the "finite" modifier for types has been removed).  That may be the PDF file to which you're referring.  For some more motivation, you may want to consult the paper "A Polymorphic Intermediate Verification Language: Design and Logical Encoding" by Leino and Rümmer [TACAS 2010].  For further example uses, see, for example, my Marktoberdorf 2008 lecture notes on Dafny, called "Specification and verification of object-oriented software", or there may be some useful slide decks on http://research.microsoft.com/en-us/um/people/leino/talks.html.

The basic functionality of the Boogie language is straightforward--it's got procedures and assignments and if-statements and loops and gotos.  The polymorphic type system is more complicated, and there are some subtle features like "where" clauses and matching triggers, but the difficulties there don't have to be understood to get started using the language.

Feel free to post specific questions at this Discussion forum.

  Rustan

Jun 29, 2010 at 11:50 AM
That first pdf is the one i referred to. Problem i have with that one, is that there's no clickable reference in the pdf. You still have the sources, so you can re-save it, with the right form of TOC?



On Tue, Jun 29, 2010 at 3:30 AM, rustanleino <notifications@codeplex.com> wrote:

From: rustanleino

The Boogie language is documented in the Boogie language reference manual, "This is Boogie 2", http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf.  It is slightly out of date (for example, the "finite" modifier for types has been removed).  That may be the PDF file to which you're referring.  For some more motivation, you may want to consult the paper "A Polymorphic Intermediate Verification Language: Design and Logical Encoding" by Leino and Rümmer [TACAS 2010].  For further example uses, see, for example, my Marktoberdorf 2008 lecture notes on Dafny, called "Specification and verification of object-oriented software", or there may be some useful slide decks on http://research.microsoft.com/en-us/um/people/leino/talks.html.

The basic functionality of the Boogie language is straightforward--it's got procedures and assignments and if-statements and loops and gotos.  The polymorphic type system is more complicated, and there are some subtle features like "where" clauses and matching triggers, but the difficulties there don't have to be understood to get started using the language.

Feel free to post specific questions at this Discussion forum.

  Rustan

Read the full discussion online.

To add a post to this discussion, reply to this email (boogie@discussions.codeplex.com)

To start a new discussion for this project, email boogie@discussions.codeplex.com

You are receiving this email because you subscribed to this discussion on CodePlex. You can unsubscribe on CodePlex.com.

Please note: Images and attachments will be removed from emails. Any posts to this discussion will also be available online at CodePlex.com


Jun 29, 2010 at 2:31 PM
OK. So I downloaded the sources of BCT, and the binaries of boogie. The initial version I had crashed with a simple test program. I made some changes, and I'm not at the point where the Microsoft.Boogie.Program class is filled correctly (I think, cannot test that:), but the file-emitting logic of the boogie model seems broken.



On Tue, Jun 29, 2010 at 12:49 PM, Matthijs ter Woord <matthijsterwoord@gmail.com> wrote:
That first pdf is the one i referred to. Problem i have with that one, is that there's no clickable reference in the pdf. You still have the sources, so you can re-save it, with the right form of TOC?




On Tue, Jun 29, 2010 at 3:30 AM, rustanleino <notifications@codeplex.com> wrote:

From: rustanleino

The Boogie language is documented in the Boogie language reference manual, "This is Boogie 2", http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf.  It is slightly out of date (for example, the "finite" modifier for types has been removed).  That may be the PDF file to which you're referring.  For some more motivation, you may want to consult the paper "A Polymorphic Intermediate Verification Language: Design and Logical Encoding" by Leino and Rümmer [TACAS 2010].  For further example uses, see, for example, my Marktoberdorf 2008 lecture notes on Dafny, called "Specification and verification of object-oriented software", or there may be some useful slide decks on http://research.microsoft.com/en-us/um/people/leino/talks.html.

The basic functionality of the Boogie language is straightforward--it's got procedures and assignments and if-statements and loops and gotos.  The polymorphic type system is more complicated, and there are some subtle features like "where" clauses and matching triggers, but the difficulties there don't have to be understood to get started using the language.

Feel free to post specific questions at this Discussion forum.

  Rustan

Read the full discussion online.

To add a post to this discussion, reply to this email (boogie@discussions.codeplex.com)

To start a new discussion for this project, email boogie@discussions.codeplex.com

You are receiving this email because you subscribed to this discussion on CodePlex. You can unsubscribe on CodePlex.com.

Please note: Images and attachments will be removed from emails. Any posts to this discussion will also be available online at CodePlex.com



Coordinator
Jun 30, 2010 at 6:44 AM

Thanks for the suggestion.  I don't know how to add a PDF TOC, but I added bookmarks to the PDF file, which should aid in navigation.

Jun 30, 2010 at 8:18 AM
Are you interested in me trying to help out with BCT ?

i made some fixes locally.
also, current binary release of boogie language model seems to be buggy

On 6/30/10, rustanleino <notifications@codeplex.com> wrote:
> From: rustanleino
>
> Thanks for the suggestion. I don't know how to add a PDF TOC, but I added
> bookmarks to the PDF file, which should aid in navigation.
>
>
Coordinator
Jun 30, 2010 at 3:45 PM

If you would like to work on the BCT project, that would be fantastic! Does its architecture make sense to you? Is there anything about the existing code that I should explain?

I've started a regression test set in the directory BCT/RegressionTests/RegressionTestInput. I guess the best way to start would be to add a new test case there --- hopefully one as small as possible. Then we can look into why it doesn't work and figure out which part would be best for you to work on.

Thanks!

Jun 30, 2010 at 3:49 PM
I'm very interested in working on the BCT project. I looked around, and the architecture makes sense, it basically parses the assembly, and generates .bpl stuff for it. I made some changes, so that generating works for my small sample project, however this revealed a bug in the Microsoft.Boogie namespace: the Procedure class gets Pre and Postconditions, but those arent' written to file..

I tried to build boogie itself, but it gives me a huge amount of build errors...


On Wed, Jun 30, 2010 at 4:45 PM, mikebarnett <notifications@codeplex.com> wrote:

From: mikebarnett

If you would like to work on the BCT project, that would be fantastic! Does its architecture make sense to you? Is there anything about the existing code that I should explain?

I've started a regression test set in the directory BCT/RegressionTests/RegressionTestInput. I guess the best way to start would be to add a new test case there --- hopefully one as small as possible. Then we can look into why it doesn't work and figure out which part would be best for you to work on.

Thanks!

Read the full discussion online.

To add a post to this discussion, reply to this email (boogie@discussions.codeplex.com)

To start a new discussion for this project, email boogie@discussions.codeplex.com

You are receiving this email because you subscribed to this discussion on CodePlex. You can unsubscribe on CodePlex.com.

Please note: Images and attachments will be removed from emails. Any posts to this discussion will also be available online at CodePlex.com


Jun 30, 2010 at 6:31 PM
Great!!!

This is (almost) what I meant with pdf toc. at least the links are on the left.. :)

On Wed, Jun 30, 2010 at 7:44 AM, rustanleino <notifications@codeplex.com> wrote:

From: rustanleino

Thanks for the suggestion.  I don't know how to add a PDF TOC, but I added bookmarks to the PDF file, which should aid in navigation.

Read the full discussion online.

To add a post to this discussion, reply to this email (boogie@discussions.codeplex.com)

To start a new discussion for this project, email boogie@discussions.codeplex.com

You are receiving this email because you subscribed to this discussion on CodePlex. You can unsubscribe on CodePlex.com.

Please note: Images and attachments will be removed from emails. Any posts to this discussion will also be available online at CodePlex.com