
Hi all,
I'm very susprised because for
class Queue<T>
{
var contents: seq<T>;
method Init();
modifies this;
ensures contents = 0;
}
Dafny says: "rbrace expected" in the ";" after Init.
Please, some help?
Paqui



There should be no semicolon after the method signature, which is why you're getting a parsing error at that source location. Also, equality is written with a doubleequals sign (like in C).
class Queue<T>
{
var contents: seq<T>;
method Init()
modifies this;
ensures contents == 0;
}
Good luck,
Rustan



Thanks,
Paqui



Hi again,
I'm trying to use your example of "sorting a queue" (see below the code).
The problem is in the line
since p is a ghost variable that can only be used in specification context.
Is there any refactoring solution?
method Sort(q: Queue<int>) returns (r: Queue<int>, perm: seq<int>)
requires q != null;
modifies q;
ensures r != null && fresh(r) && r.contents == old(q.contents);
ensures (forall i, j :: 0 <= i && i < j && j < r.contents ==> r.Get(i) <= r.Get(j));
ensures perm == r.contents; // ==pperm
ensures (forall i: int :: 0 <= i && i < perm ==> 0 <= perm[i] && perm[i] < perm);
ensures (forall i, j: int :: 0 <= i && i < j && j < perm ==> perm[i] != perm[j]);
ensures (forall i: int :: 0 <= i && i < perm ==> r.contents[i] == old(q.contents)[perm[i]]);
{
r := new Queue<int>;
r.Init();
ghost var p := [];
var n := 0;
while (n < q.contents)
invariant n == p && n <= q.contents;
invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);
{
p := p + [n]; n := n + 1;
}
perm:= [];
ghost var pperm := p + perm;
while (q.contents != 0)
invariant r.contents == old(q.contents)  q.contents;
invariant (forall i, j :: 0 <= i && i < j && j < r.contents ==> r.contents[i] <= r.contents[j]);
invariant (forall i, j :: 0 <= i && i < r.contents && 0 <= j && j < q.contents ==> r.contents[i] <= q.contents[j]);
invariant pperm==p + perm && p==q.contents&& perm==r.contents;
invariant (forall i: int :: 0 <= i && i < perm ==> 0 <= perm[i] && perm[i] < pperm);
invariant (forall i:int::0<=i && i<p==> 0<=p[i] && p[i]<pperm);
invariant (forall i, j: int :: 0 <= i && i < j && j < pperm ==> pperm[i] != pperm[j]);
invariant (forall i: int :: 0 <= i && i < perm ==> r.contents[i] == old(q.contents)[perm[i]]);
invariant (forall i: int :: 0 <= i && i < p ==> q.contents[i] == old(q.contents)[p[i]]);
decreases q.contents;
{
var m,k := RemoveMin(q);
perm := perm + [p[k]]; //adds index of min to perm
p := p[k+1..]+ p[..k]; //remove index of min from p
r.Enqueue(m);
pperm := pperm[k+1..p+1]+pperm[..k]+pperm[p+1..]+[pperm[k]];
}
//lemma needed to trigger axiom
assert (forall i:int :: 0<=i && i < perm ==> perm[i] == pperm[i]);
}



I'm afraid I can't see what line you were referring to? But perhaps you're asking about the permutation and wanting to make it a ghost? That makes sense. In your version of the code above, the fact that Sort produces a permutation of the input is ensured
by actually returning that permutation as outparameter "perm". A different way to do it would be to existentially quantify over some "perm" in the postcondition, but since "perm" is computed anyway, then you might as well return
it. Since "perm" is used only for specification purposesI don't imagine you want to actually return the permutation in a running programjust declare the outparameter as "ghost".
Here's a cleaned up version of your code:
http://rise4fun.com/Dafny/HplwT
Btw, it seems you have built this code from some really old Dafny program. You can solve the problem more elegantly by using a multiset to specify the fact that you want Sort to produce a permutation. See the Dafny test suite.
Rustan



Thank you again. Now, it works. I agree that it is more elegant to use multisets. It allows us to abstract the permutation. I think that it would be also useful to show the two versions to the students and compare them.
Paqui



I'm very happy using multisets for specifiying a sorting algorithm for seq<int> and Queue<int>.
Now, I have two questions. The first one is if does Dafny support polimorphism to extend my solution to seq<T> (or Queue<T>)
where T is any "ordered" type? I mean, similar to Haskell.
The second with the objects of the type "Queue<Queue<T>>". Could you tell how to modify the head of the head of q:Queue<Queue<T>>.
For example, the following method M is not correct:
class Queue<T>
{
var contents: seq<T>;
function method Head(): T
requires 0 < contents;
reads this;
{ contents[0] }
// Here the remaining methods of the class
}
method M(q: Queue<Queue<int>>)
{
if q.Head().Head() != 0 { }
else {(q.contents[0])).contents[0] := 0;}
}



Hi Paqui,
For your first question, I'm not sure if you want to (0) write a program using seq<T> and then refine it into using Queue<T> instead, or (1) let the type parameter T indicate that any "ordered" type is acceptable. For (0), there is no
direct way to saying "replace every seq<T> with a Queue<T> in my program", although Dafny's refinement features are intended to help in that direction. For (1), Dafny has no type classes like Haskell does. It also does not currently allow
you to pass such a comparison function as a parameter. However, you can use modules and refinement in Dafny to achieve this. See Test/test3/GenericSort.dfy in the Dafny test suite, which I just checked in.
For the second question, first obtain (a pointer to) the inner Queue object (the one of type Queue<int>):
var inner := q.contents[0];
Then, set inner.contents to a new sequence. The new sequence will be like the previous one, except that it will map index 0 to the value 0:
inner.contents := inner.contents[0 := 0];
To get the code to verify, you will need to think about the nonnullness of inner as well as issues of framing (that is, what you're allowed to modify). Also, I imagine there's some reason you want to manipulate the .contents directly, but otherwise you may
consider changing contents by invoking methods on the two Queue's (you would still have to thinking about nonnullness and framing).
Rustan


Dec 19, 2013 at 2:55 PM
Edited Dec 19, 2013 at 2:59 PM

Hi Rustan,
Thank you again for your clear and quick answers.
I'm doing many different Dafny implementations of a sorting algorithm, in order to learn Dafny.
I already know that Dafny polimorphism is not as powerful as Haskell polimorphism.
However, I hope that functions over generic datatypes can be used over instances of these datatypes.
For example, if I define
`type T
datatype Seq<T> = Empty  Cons(head:T, tail:Seq<T>)
function length(s: Seq<T>):int
{
match s
case Empty => 0
case Cons(hd,tl) => 1+ length(tl)
}
then, it seem that I cannot apply the function length to a value of type Seq<int>, for example
a typing error is reported for using "length" in the following predicate definition
predicate sorted(s: Seq<int>)
{
length(s)>1 ==> s.head <= s.tail.head && sorted(s.tail)
}
Is there some way to declare <T> to be generic, in order to enable the application of the functions, defined over
Seq<T>, to values of instance types like Seq<int> or Seq<Seq<int>>.
Best,
Paqui



In your example, there are two different T's. One of them is declared as an uninterpreted type (using "type T"). The other is a bound type variable in the declaration of "Seq". Note that the "T" you refer to in the "length"
function is the former, so your "length" function applies only to sequences of that particular type "T". That's why you get a type error when you try to call "length" with a Seq<int>.
To fix the problem, get rid of the "type T" declaration. Instead, declare "length" to take a type parameter:
function length<T>(s: Seq<T>): int
Rustan

