parse error

Dec 3, 2013 at 2:02 PM
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?
Dec 3, 2013 at 5:59 PM
There should be no semi-colon after the method signature, which is why you're getting a parsing error at that source location. Also, equality is written with a double-equals sign (like in C).
class Queue<T> 
    var contents: seq<T>;

    method Init()
    modifies this;
    ensures |contents| == 0;
Good luck,
Dec 10, 2013 at 3:05 PM
Dec 10, 2013 at 4:51 PM
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>;
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
        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]);
Dec 10, 2013 at 5:15 PM
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 out-parameter "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 purposes--I don't imagine you want to actually return the permutation in a running program--just declare the out-parameter as "ghost".

Here's a cleaned up version of your code:

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.

Dec 10, 2013 at 5:49 PM
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.
Dec 18, 2013 at 3:43 PM
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;}
Dec 18, 2013 at 11:27 PM
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 non-nullness 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 non-nullness and framing).

Dec 19, 2013 at 1:55 PM
Edited Dec 19, 2013 at 1: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>>.
Dec 20, 2013 at 11:39 PM
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