From 9fe20e5de05378f3d570df17a80ad0cbe32e5e54 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Wed, 1 Sep 2010 02:18:50 +0000 Subject: Dafny: Added Dafny solutions to the VSComp 2010 problems --- Test/VSComp2010/Answer | 25 +++ Test/VSComp2010/Problem1-SumMax.dfy | 43 +++++ Test/VSComp2010/Problem2-Invert.dfy | 79 ++++++++++ Test/VSComp2010/Problem3-FindZero.dfy | 92 +++++++++++ Test/VSComp2010/Problem4-Queens.dfy | 219 ++++++++++++++++++++++++++ Test/VSComp2010/Problem5-DoubleEndedQueue.dfy | 174 ++++++++++++++++++++ Test/VSComp2010/runtest.bat | 15 ++ 7 files changed, 647 insertions(+) create mode 100644 Test/VSComp2010/Answer create mode 100644 Test/VSComp2010/Problem1-SumMax.dfy create mode 100644 Test/VSComp2010/Problem2-Invert.dfy create mode 100644 Test/VSComp2010/Problem3-FindZero.dfy create mode 100644 Test/VSComp2010/Problem4-Queens.dfy create mode 100644 Test/VSComp2010/Problem5-DoubleEndedQueue.dfy create mode 100644 Test/VSComp2010/runtest.bat (limited to 'Test/VSComp2010') diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer new file mode 100644 index 00000000..74aaae2b --- /dev/null +++ b/Test/VSComp2010/Answer @@ -0,0 +1,25 @@ + +-------------------- Problem1-SumMax.dfy -------------------- + +Dafny program verifier finished with 4 verified, 0 errors +Compiled program written to out.cs + +-------------------- Problem2-Invert.dfy -------------------- + +Dafny program verifier finished with 7 verified, 0 errors +Compiled program written to out.cs + +-------------------- Problem3-FindZero.dfy -------------------- + +Dafny program verifier finished with 7 verified, 0 errors +Compiled program written to out.cs + +-------------------- Problem4-Queens.dfy -------------------- + +Dafny program verifier finished with 15 verified, 0 errors +Compiled program written to out.cs + +-------------------- Problem5-DoubleEndedQueue.dfy -------------------- + +Dafny program verifier finished with 21 verified, 0 errors +Compiled program written to out.cs diff --git a/Test/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy new file mode 100644 index 00000000..be7cc2c8 --- /dev/null +++ b/Test/VSComp2010/Problem1-SumMax.dfy @@ -0,0 +1,43 @@ +// VSComp 2010, problem 1, compute the sum and max of the elements of an array and prove +// that 'sum <= N * max'. +// Rustan Leino, 18 August 2010. +// +// The problem statement gave the pseudo-code for the method, but did not ask to prove +// that 'sum' or 'max' return as the sum and max, respectively, of the array. The +// given assumption that the array's elements are non-negative is not needed to establish +// the requested postcondition. + +method M(N: int, a: array) returns (sum: int, max: int) + requires 0 <= N && a != null && |a| == N && (forall k :: 0 <= k && k < N ==> 0 <= a[k]); + ensures sum <= N * max; +{ + sum := 0; + max := 0; + var i := 0; + while (i < N) + invariant i <= N && sum <= i * max; + { + if (max < a[i]) { + max := a[i]; + } + sum := sum + a[i]; + i := i + 1; + } +} + +method Main() +{ + var a := new int[10]; + a[0] := 9; + a[1] := 5; + a[2] := 0; + a[3] := 2; + a[4] := 7; + a[5] := 3; + a[6] := 2; + a[7] := 1; + a[8] := 10; + a[9] := 6; + call s, m := M(10, a); + print "N = ", |a|, " sum = ", s, " max = ", m, "\n"; +} diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy new file mode 100644 index 00000000..63da4cb5 --- /dev/null +++ b/Test/VSComp2010/Problem2-Invert.dfy @@ -0,0 +1,79 @@ +// VSComp 2010, problem 2, compute the inverse 'B' of a permutation 'A' and prove that 'B' is +// indeed an inverse of 'A' (or at least prove that 'B' is injective). +// Rustan Leino, 31 August 2010. +// +// In the version of this program that I wrote during the week of VSTTE 2010, I had +// used a lemma (stated as a ghost method) that I proved inductively (using a loop and +// a loop invariant). Here, I have simplified that version by just including an +// assertion of the crucial property, which follows from the surjectivity of 'A'. +// +// The difficulty in proving this program with an SMT solver stems from the fact that +// the quantifier that states the surjectivity property has no good matching trigger +// (because there are no function symbols mentioned in the antecedent of that quantifier, +// only built-in predicates). Therefore, I introduced a dummy function 'inImage' and +// defined it always to equal 'true'. I can then mention this function in the crucial +// assertion, which causes the appropriate triggering to take place. +// +// A slight annoyance is that the loop's modifications of the heap, which is checked +// to include only the elements of 'B'. Since 'A' and 'B' are arrays stored at different +// locations in the heap, it then follows that the elements of 'A' are not modified. +// However, the fact that the heap has changed at all makes the symbolic expressions +// denoting the elements of 'A' look different before and after the heap. The +// assertion after the loop (which, like all assertions, is proved) is needed to +// connect the two. + +method M(N: int, A: array, B: array) + requires 0 <= N && A != null && B != null && N == |A| && N == |B| && A != B; + requires (forall k :: 0 <= k && k < N ==> 0 <= A[k] && A[k] < N); + requires (forall j,k :: 0 <= j && j < k && k < N ==> A[j] != A[k]); // A is injective + requires (forall m :: 0 <= m && m < N && inImage(m) ==> (exists k :: 0 <= k && k < N && A[k] == m)); // A is surjective + modifies B; + ensures (forall k :: 0 <= k && k < N ==> 0 <= B[k] && B[k] < N); + ensures (forall k :: 0 <= k && k < N ==> B[A[k]] == k && A[B[k]] == k); // A and B are each other's inverses + ensures (forall j,k :: 0 <= j && j < k && k < N ==> B[j] != B[k]); // (which means that) B is injective +{ + var n := 0; + while (n < N) + invariant n <= N; + invariant (forall k :: 0 <= k && k < n ==> B[A[k]] == k); + { + B[A[n]] := n; + n := n + 1; + } + assert (forall i :: 0 <= i && i < N ==> A[i] == old(A[i])); // the elements of A were not changed by the loop + // it now follows from the surjectivity of A that A is the inverse of B: + assert (forall j :: 0 <= j && j < N && inImage(j) ==> 0 <= B[j] && B[j] < N && A[B[j]] == j); +} + +static function inImage(i: int): bool { true } // this function is used to trigger the surjective quantification + +method Main() +{ + var a := new int[10]; + a[0] := 9; + a[1] := 3; + a[2] := 8; + a[3] := 2; + a[4] := 7; + a[5] := 4; + a[6] := 0; + a[7] := 1; + a[8] := 5; + a[9] := 6; + var b := new int[10]; + call M(10, a, b); + print "a:\n"; + call PrintArray(a); + print "b:\n"; + call PrintArray(b); +} + +method PrintArray(a: array) + requires a != null; +{ + var i := 0; + while (i < |a|) { + print a[i], "\n"; + i := i + 1; + } +} diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy new file mode 100644 index 00000000..03e6bdfe --- /dev/null +++ b/Test/VSComp2010/Problem3-FindZero.dfy @@ -0,0 +1,92 @@ +// VSComp 2010, problem 3, find a 0 in a linked list and return how many nodes were skipped +// until the first 0 (or end-of-list) was found. +// Rustan Leino, 18 August 2010. +// +// The difficulty in this problem lies in specifying what the return value 'r' denotes and in +// proving that the program terminates. Both of these are addressed by declaring a ghost +// field 'List' in each linked-list node, abstractly representing the linked-list elements +// from the node to the end of the linked list. The specification can now talk about that +// sequence of elements and can use 'r' as an index into the sequence, and termination can +// be proved from the fact that all sequences in Dafny are finite. +// +// We only want to deal with linked lists whose 'List' field is properly filled in (which +// can only happen in an acyclic list, for example). To that avail, the standard idiom in +// Dafny is to declare a predicate 'Valid()' that is true of an object when the data structure +// representing object's abstract value is properly formed. The definition of 'Valid()' +// is what one intuitively would think of as the ''object invariant'', and it is mentioned +// explicitly in method pre- and postconditions. As part of this standard idiom, one also +// declared a ghost variable 'Repr' that is maintained as the set of objects that make up +// the representation of the aggregate object--in this case, the Node itself and all its +// successors. + +class Node { + ghost var List: seq; + ghost var Repr: set; + var head: int; + var next: Node; + + function Valid(): bool + reads this, Repr; + { + this in Repr && + 1 <= |List| && List[0] == head && + (next == null ==> |List| == 1) && + (next != null ==> + next in Repr && next.Repr <= Repr && this !in next.Repr && next.Valid() && next.List == List[1..]) + } + + static method Cons(x: int, tail: Node) returns (n: Node) + requires tail == null || tail.Valid(); + ensures n != null && n.Valid(); + ensures if tail == null then n.List == [x] else n.List == [x] + tail.List; + { + n := new Node; + n.head := x; + n.next := tail; + if (tail == null) { + n.List := [x]; + n.Repr := {n}; + } else { + n.List := [x] + tail.List; + n.Repr := {n} + tail.Repr; + } + } +} + +static method Search(ll: Node) returns (r: int) + requires ll == null || ll.Valid(); + ensures ll == null ==> r == 0; + ensures ll != null ==> + 0 <= r && r <= |ll.List| && + (r < |ll.List| ==> ll.List[r] == 0 && 0 !in ll.List[..r]) && + (r == |ll.List| ==> 0 !in ll.List); +{ + if (ll == null) { + r := 0; + } else { + var jj := ll; + var i := 0; + while (jj != null && jj.head != 0) + invariant jj != null ==> jj.Valid() && i + |jj.List| == |ll.List| && ll.List[i..] == jj.List; + invariant jj == null ==> i == |ll.List|; + invariant 0 !in ll.List[..i]; + decreases |ll.List| - i; + { + jj := jj.next; + i := i + 1; + } + r := i; + } +} + +method Main() +{ + var list: Node := null; + call list := list.Cons(0, list); + call list := list.Cons(5, list); + call list := list.Cons(0, list); + call list := list.Cons(8, list); + call r := Search(list); + print "Search returns ", r, "\n"; + assert r == 1; +} diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy new file mode 100644 index 00000000..a07a2a5e --- /dev/null +++ b/Test/VSComp2010/Problem4-Queens.dfy @@ -0,0 +1,219 @@ +// VSComp 2010, problem 4, N queens +// Rustan Leino, 31 August 2010. +// +// In the version of this program that I wrote during the week of VSTTE 2010, I had +// an unproved assumption. In this version, I simply changed the existential quantifier +// in that assumption to specify a particular witness, which is enough of a hint for +// Dafny to fully prove the correctness of the program. +// +// Oh, I also added some comments in this version of the program. +// +// The correctness of this program relies on some properties of Queens boards. These +// are stated and proved as lemmas, which can be declared in Dafny as ghost methods. +// +// There are two annoyances in this program: +// +// One has to do with Dafny's split between ''ghost'' variables/code and ''physical'' +// variables/code. The ''ghost'' things are used by the verifier, but are ignored by +// the compiler. This is generally good, since any additional specifications are ghost +// state that are needed to convince the verifier that a program is correct (let alone +// express what it means for the program to be correct) are not required at run time. +// However, Dafny currently considers *all* quantifiers to be ghost-only, which +// necessitates some duplication of the 'IsConsistent' condition. +// +// The other annoyance is that Dafny's proof-term representation of the function +// 'IsConsistent' implicitly takes the heap as an argument, despite the fact that +// 'IsConsistent' does not depend on any part of the heap. Dafny ought to be able +// to figure that out from the fact that 'IsConsistent' has no 'reads' clause. +// Maybe a future version of Dafny will do just that. But until then, some methods +// below are specified with an (easy-to-prove) postcondition that 'IsConsistent(B,p)' +// does not change for any 'B' and 'p', even if the method may change the heap in +// some way. + + +// The Search method returns whether or not there exists an N-queens solution for the +// given N. If 'success' returns as 'true', 'board' indicates a solution. If 'success' +// returns as 'false', no solution exists, as stated in the second postcondition. +method Search(N: int) returns (success: bool, board: seq) + requires 0 <= N; + ensures success ==> + |board| == N && + (forall p :: 0 <= p && p < N ==> IsConsistent(board, p)); + ensures !success ==> + (forall B :: + |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) + ==> + (exists p :: 0 <= p && p < N && !IsConsistent(B, p))); +{ + call success, board := SearchAux(N, []); +} + +// Given a board, this function says whether or not the queen placed in column 'pos' +// is consistent with the queens placed in columns to its left. +static function IsConsistent(board: seq, pos: int): bool +{ + 0 <= pos && pos < |board| && + (forall q :: 0 <= q && q < pos ==> + board[q] != board[pos] && + board[q] - board[pos] != pos - q && + board[pos] - board[q] != pos - q) +} + +// The following lemma says that 'IsConsistent' is monotonic in its first argument. +// More precisely, if 'short' is a board with a queen consistently placed in column +// 'pos', then that queen is also consistently placed in any extension 'long' of the +// board 'short' (that is, the sequence of queen positions 'short' is a prefix of the +// sequence of queen positions 'long'). In other words, consistency of a queen in +// column 'pos' does not depend on columns to the right of 'pos'. +ghost method Lemma0(short: seq, long: seq, pos: int) + requires short <= long; + ensures IsConsistent(short, pos) ==> IsConsistent(long, pos); +{ + if (IsConsistent(short, pos)) { + assert IsConsistent(long, pos); + } +} + +// Lemma1 states Lemma0 for every column in the board 'short'. +ghost method Lemma1(short: seq, long: seq) + requires short <= long; + ensures (forall k :: 0 <= k && k < |short| && IsConsistent(short, k) ==> IsConsistent(long, k)); + ensures (forall B, p :: IsConsistent(B, p) <==> old(IsConsistent(B, p))); +{ + var j := 0; + while (j < |short|) + invariant j <= |short|; + invariant (forall k :: 0 <= k && k < j && IsConsistent(short, k) ==> IsConsistent(long, k)); + { + call Lemma0(short, long, j); + j := j + 1; + } +} + +method CheckConsistent(board: seq, pos: int) returns (b: bool) + ensures b <==> IsConsistent(board, pos); + ensures (forall B, p :: IsConsistent(B, p) <==> old(IsConsistent(B, p))); +{ + // The Dafny compiler won't compile a function with a 'forall' inside. (This seems reasonable + // in general, since quantifiers could range over all the integers. Here, however, where the + // range of the quantifier is bounded, it just seems stupid.) Therefore, we + // have to provide a method that computes the same thing as the function defines. + if (0 <= pos && pos < |board|) { + var p := 0; + while (p < pos) + invariant p <= pos; + invariant (forall q :: 0 <= q && q < p ==> + board[q] != board[pos] && + board[q] - board[pos] != pos - q && + board[pos] - board[q] != pos - q); + { + if (!(board[p] != board[pos] && + board[p] - board[pos] != pos - p && + board[pos] - board[p] != pos - p)) { + b := false; + return; + } + p := p + 1; + } + b := true; + return; + } + b := false; +} + +// Here comes the method where the real work is being done. With an ultimate board size of 'N' +// in mind and given the consistent placement 'boardSoFar' of '|boardSoFar|' columns, this method +// will search for a solution for the remaining columns. If 'success' returns as 'true', +// then 'newBoard' is a consistent placement of 'N' queens. If 'success' returns as 'false', +// then there is no way to extend 'boardSoFar' to get a solution for 'N' queens. +method SearchAux(N: int, boardSoFar: seq) returns (success: bool, newBoard: seq) + requires 0 <= N && |boardSoFar| <= N; + // consistent so far: + requires (forall k :: 0 <= k && k < |boardSoFar| ==> IsConsistent(boardSoFar, k)); + ensures success ==> + |newBoard| == N && + (forall p :: 0 <= p && p < N ==> IsConsistent(newBoard, p)); + ensures !success ==> + (forall B :: + |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) && + boardSoFar <= B + ==> + (exists p :: 0 <= p && p < N && !IsConsistent(B, p))); + ensures (forall B, p :: IsConsistent(B, p) <==> old(IsConsistent(B, p))); + decreases N - |boardSoFar|; +{ + var pos := |boardSoFar|; + if (pos == N) { + // The given board already has the desired size. + newBoard := boardSoFar; + success := true; + } else { + // Exhaustively try all possibilities for the new column, 'pos'. + var n := 0; + while (n < N) + invariant n <= N; + invariant (forall B :: + // For any board 'B' with 'N' queens, each placed in an existing row + |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) && + // ... where 'B' is an extension of 'boardSoFar' + boardSoFar <= B && + // ... and the first column to extend 'boardSoFar' has a queen in one of + // the first 'n' rows + 0 <= B[pos] && B[pos] < n + ==> + // ... the board 'B' is not entirely consistent + (exists p :: 0 <= p && p < N && !IsConsistent(B, p))); + { + // Let's try to extend the board-so-far with a queen in column 'n': + var candidateBoard := boardSoFar + [n]; + call consistent := CheckConsistent(candidateBoard, pos); + if (consistent) { + // The new queen is consistent. Thus, 'candidateBoard' is consistent in column 'pos'. + // The consistency of the queens in columns left of 'pos' follows from the + // consistency of those queens in 'boardSoFar' and the fact that 'candidateBoard' is + // an extension of 'boardSoFar', as Lemma1 tells us: + call Lemma1(boardSoFar, candidateBoard); + // Thus, we meet the precondition of 'SearchAux' on 'candidateBoard', so let's search + // for a solution that extends 'candidateBoard'. + call s, b := SearchAux(N, candidateBoard); + if (s) { + // The recursive call to 'SearchAux' found consistent positions for all remaining columns + newBoard := b; + success := true; + return; + } + // The recursive call to 'SearchAux' determined that no consistent extensions to 'candidateBoard' + // exist. + } else { + // Since 'n' is not a consistent placement for a queen in column 'pos', there is also + // no extension of 'candidateBoard' that would make the entire board consistent. + assert (forall B :: + |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) && + candidateBoard <= B + ==> + !IsConsistent(B, pos)); + } + n := n + 1; + } + + success := false; + } +} + +method Main() +{ + call s, b := Search(2); + print "N=2 returns ", s, "\n"; + call s, b := Search(4); + print "N=4 returns ", s, "\n"; + call PrintSeq(b); +} + +method PrintSeq(b: seq) +{ + var i := 0; + while (i < |b|) { + print " ", b[i], "\n"; + i := i + 1; + } +} diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy new file mode 100644 index 00000000..70b38a5d --- /dev/null +++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy @@ -0,0 +1,174 @@ +// VSComp 2010, problem 5, double-ended queue. +// Rustan Leino, 18 August 2010. +// +// This program employs the standard Valid()/Repr idiom used in the dynamic-frames +// style of specifications, see for example the comment in Problem3-FindZero.dfy. +// Within that idiom, the specification is straightforward (if verbose), and there +// are no particular wrinkles or annoyances in getting the verifier to prove the +// correctness. + +class AmortizedQueue { + // The front of the queue. + var front: LinkedList; + // The rear of the queue (stored in reversed order). + var rear: LinkedList; + + ghost var Repr: set; + ghost var List: seq; + + function Valid(): bool + reads this, Repr; + { + this in Repr && + front != null && front in Repr && front.Repr <= Repr && front.Valid() && + rear != null && rear in Repr && rear.Repr <= Repr && rear.Valid() && + |rear.List| <= |front.List| && + List == front.List + rear.ReverseSeq(rear.List) + } + + method Init() + modifies this; + ensures Valid() && List == []; + { + var tmp := new LinkedList; + front := tmp; + call front.Init(); + tmp := new LinkedList; + rear := tmp; + call rear.Init(); + Repr := {this}; + Repr := Repr + front.Repr + rear.Repr; + List := []; + } + + method InitFromPieces(f: LinkedList, r: LinkedList) + requires f != null && f.Valid() && r != null && r.Valid(); + modifies this; + ensures Valid() && List == f.List + r.ReverseSeq(r.List); + { + if (r.length <= f.length) { + front := f; + rear := r; + } else { + call rr := r.Reverse(); + call ff := f.Concat(rr); + front := ff; + + var tmp := new LinkedList; + call tmp.Init(); + rear := tmp; + } + Repr := {this}; + Repr := Repr + front.Repr + rear.Repr; + List := front.List + rear.ReverseSeq(rear.List); + } + + method Front() returns (t: T) + requires Valid() && List != []; + ensures t == List[0]; + { + t := front.head; + } + + method Tail() returns (r: AmortizedQueue) + requires Valid() && List != []; + ensures r != null && r.Valid() && r.List == List[1..]; + { + r := new AmortizedQueue; + call r.InitFromPieces(front.tail, rear); + } + + method Enqueue(item: T) returns (r: AmortizedQueue) + requires Valid(); + ensures r != null && r.Valid() && r.List == List + [item]; + { + call rr := rear.Cons(item); + var tmp := new AmortizedQueue; + call tmp.InitFromPieces(front, rr); + r := tmp; + } +} + + +class LinkedList { + var head: T; + var tail: LinkedList; + var length: int; + + ghost var List: seq; + ghost var Repr: set>; + + function Valid(): bool + reads this, Repr; + { + this in Repr && + 0 <= length && length == |List| && + (length == 0 ==> List == [] && tail == null) && + (length != 0 ==> + tail != null && tail in Repr && + tail.Repr <= Repr && this !in tail.Repr && + tail.Valid() && + List == [head] + tail.List && + length == tail.length + 1) + } + + method Init() + modifies this; + ensures Valid() && List == []; + { + tail := null; + length := 0; + List := []; + Repr := {this}; + } + + method Cons(d: T) returns (r: LinkedList) + requires Valid(); + ensures r != null && r.Valid() && r.List == [d] + List; + { + r := new LinkedList; + r.head := d; + r.tail := this; + r.length := length + 1; + r.List := [d] + List; + r.Repr := {r} + Repr; + } + + method Concat(end: LinkedList) returns (r: LinkedList) + requires Valid() && end != null && end.Valid(); + ensures r != null && r.Valid() && r.List == List + end.List; + decreases Repr; + { + if (length == 0) { + r := end; + } else { + call c := tail.Concat(end); + call r := c.Cons(head); + } + } + + method Reverse() returns (r: LinkedList) + requires Valid(); + ensures r != null && r.Valid() && |List| == |r.List|; + ensures (forall k :: 0 <= k && k < |List| ==> List[k] == r.List[|List|-1-k]); + ensures r.List == ReverseSeq(List); + decreases Repr; + { + if (length == 0) { + r := this; + } else { + call r := tail.Reverse(); + var e := new LinkedList; + call e.Init(); + call e := e.Cons(head); + call r := r.Concat(e); + } + } + + static function method ReverseSeq(s: seq): seq + decreases s; + { + if s == [] then [] else + ReverseSeq(s[1..]) + [s[0]] + } +} diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat new file mode 100644 index 00000000..e39abe7d --- /dev/null +++ b/Test/VSComp2010/runtest.bat @@ -0,0 +1,15 @@ +@echo off +setlocal + +set BOOGIEDIR=..\..\Binaries +set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe +set BPLEXE=%BOOGIEDIR%\Boogie.exe + + +for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy + Problem3-FindZero.dfy Problem4-Queens.dfy + Problem5-DoubleEndedQueue.dfy) do ( + echo. + echo -------------------- %%f -------------------- + %DAFNY_EXE% %* %%f +) -- cgit v1.2.3