Boogie Records

Jan 24, 2013 at 6:35 PM
Edited Jan 25, 2013 at 6:04 PM

I think the answer is "no", but in case I missed something: Does Boogie have any support for product types and/or tagged disjoint unions?

Throwing in a bit of Haskell notation, I'd like to do the following:

type RefT ;
type ArrayRefT _;
type FieldT _ ;
data LocT alpha = MEMBER(RefT, FieldT alpha) | ITEM( ArrayRefT alpha, int ) ;
type StoreT = <alpha> [LocT alpha] alpha ;


Feb 7, 2013 at 12:54 PM
To answer my own question: It is clear from Rustan's 2010 Dafny paper that Boogie does not natively support tagged unions, although Z3 does. The Dafny paper outlines how they can be built using axioms.

Alternatively, the types above can be emulated by using the following types
type RefT
type ArrayRefT _ ;
type FieldT _ ;
type FieldStoreT = <alpha> [RefT, Field alpha] alpha ;
type ArrayStoreT = <alpha> [ArrayRefT alpha, int] alpha ;
Then, for example, each variable of type StoreT (above) is emulated by a pair of variables of types FieldStoreT and ArrayStoreT.

Feb 8, 2013 at 12:05 AM
I don't fully understand your Haskell notation. But boogie now has support for algebraic data types. Take a look at Boogie\Test\datatypes*.bpl for samples.