[Dafny] set<object> comprehensions

Nov 21, 2012 at 3:18 PM

Let's say this has type C and this.a is an array (or, for that matter, anything other than C or object). I expected {this, this.a} to denote a value of type set<object>, but I get a typing error instead. Is this to be expected?

I wanted to use this to describe a dynamic frame (well, not really very "dynamic")  in the class invariant of a Vector class,  (e.g. http://rise4fun.com/Dafny/lwVs). The only workaround I found is to use a weaker invariant.... (for the actual initialization of the ghost var I can use two assignments).

Coordinator
Nov 22, 2012 at 5:40 PM

The type inference is broken in this regard, because it insists that all references between the curly braces be of the same type.  For dynamic frames, it is sufficient to specify a lower bound on the objects in "rep", so you can write:

this in rep && a in rep

When in the constructor you assign to "rep", you'll find the same issue for the assignment RHS, which you can work around using multiple assignment statements.

See http://rise4fun.com/Dafny/036, where I have also included the common condition "null !in rep".

  Rustan