Boogie Documentation

[MartinKoelbl]

It's great to see the progress Boogie is still making.

We are working on some output to Boogie and trying to understand the memory model of Move, Dafny and other verifiers. These verifiers convert to Boogie, so it would be helpful to understand the Boogie language in detail. For example, the concept of accessing an attribute attr of a structure type {:datatype} $1_M1_Beta; through $attr#$1_M1_Beta.

The given documentation contains some gaps and the paper 'This is Boogie 2' has been published for some time.
Is there any recent documentation for Boogie?
Many thanks for your help.

[shazqadeer]

In general, attributes don't have standard semantics in Boogie. They are often used to (1) add client-specific semantics, or (2) quickly experiment with features.

The specific attribute you are referring to :datatype was added to experiment with exposing inductive datatypes, which are supported in SMT solvers, at the Boogie level. The experience with datatypes was positive so now we hav added native support for datatypes and this particular attribute has been eliminated. You can see many samples using datatypes in the Test\datatypes or Test\civl folders. datatype is now a Boogie keyword. You can also search for it in the Test to see all the samples that use it.