From 7cabbe6e10f11b90df4e4b5f5a3bb1c2253b87c5 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Wed, 13 Jun 2012 11:54:11 -0700 Subject: Dafny: liberalized equality to work when the types could possibly be the same (i.e. a != b is allowed when a: array and b: array) --- Test/vacid0/LazyInitArray.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Test/vacid0') diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy index e56a8317..3e5a95ef 100644 --- a/Test/vacid0/LazyInitArray.dfy +++ b/Test/vacid0/LazyInitArray.dfy @@ -11,10 +11,10 @@ class LazyInitArray { reads this, a, b, c; { a != null && b != null && c != null && - a.Length == |Contents| + 1 && // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c' + a.Length == |Contents| && b.Length == |Contents| && c.Length == |Contents| && - b != c && + b != c && a != b && a != c && 0 <= n && n <= c.Length && (forall i :: 0 <= i && i < |Contents| ==> Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) && @@ -41,7 +41,7 @@ class LazyInitArray { ensures |Contents| == N && Zero == zero; ensures (forall x :: x in Contents ==> x == zero); { - a := new T[N+1]; + a := new T[N]; b := new int[N]; c := new int[N]; n := 0; -- cgit v1.2.3 From 1f267ac0d7daf434ed4db31d23914428149297bc Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 14 Jun 2012 13:34:20 -0700 Subject: Dafny: cleaned up test scripts a little --- Test/VSComp2010/runtest.bat | 2 - Test/VSI-Benchmarks/runtest.bat | 2 - Test/dafny0/runtest.bat | 1 - Test/dafny1/Answer | 4 - Test/dafny1/BQueue.bpl | 430 ---------------------------------------- Test/dafny1/runtest.bat | 8 - Test/dafny2/Answer | 4 + Test/dafny2/TuringFactorial.dfy | 26 +++ Test/dafny2/runtest.bat | 3 +- Test/vacid0/runtest.bat | 2 - Test/vstte2012/runtest.bat | 1 - 11 files changed, 31 insertions(+), 452 deletions(-) delete mode 100644 Test/dafny1/BQueue.bpl create mode 100644 Test/dafny2/TuringFactorial.dfy (limited to 'Test/vacid0') diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat index 9535d677..63f5df23 100644 --- a/Test/VSComp2010/runtest.bat +++ b/Test/VSComp2010/runtest.bat @@ -3,8 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe -set BPLEXE=%BOOGIEDIR%\Boogie.exe -set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy Problem3-FindZero.dfy Problem4-Queens.dfy diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat index 611f9251..f5b9d1b9 100644 --- a/Test/VSI-Benchmarks/runtest.bat +++ b/Test/VSI-Benchmarks/runtest.bat @@ -3,8 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe -set BPLEXE=%BOOGIEDIR%\Boogie.exe -set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do ( echo. diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 0da7fe3e..ac7c8aed 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -3,7 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe -set BPLEXE=%BOOGIEDIR%\Boogie.exe for %%f in (Simple.dfy) do ( echo. diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 9ed6d75a..7c7719ee 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -1,8 +1,4 @@ --------------------- BQueue.bpl -------------------- - -Boogie program verifier finished with 8 verified, 0 errors - -------------------- Queue.dfy -------------------- Dafny program verifier finished with 22 verified, 0 errors diff --git a/Test/dafny1/BQueue.bpl b/Test/dafny1/BQueue.bpl deleted file mode 100644 index 77f1efb3..00000000 --- a/Test/dafny1/BQueue.bpl +++ /dev/null @@ -1,430 +0,0 @@ -// BQueue.bpl -// A queue program specified in the style of dynamic frames. -// Rustan Leino, Michal Moskal, and Wolfram Schulte, 2007. - -// --------------------------------------------------------------- - -type ref; -const null: ref; - -type Field x; - -// this variable represents the heap; read its type as \forall \alpha. ref * Field \alpha --> \alpha -type HeapType = [ref, Field x]x; -var H: HeapType; - -// every object has an 'alloc' field, which says whether or not the object has been allocated -const unique alloc: Field bool; - -// for simplicity, we say that every object has one field representing its abstract value and one -// field representing its footprint (aka frame aka data group). - -const unique abstractValue: Field Seq; -const unique footprint: Field [ref]bool; - -// --------------------------------------------------------------- - -type T; // the type of the elements of the queue -const NullT: T; // some value of type T - -// --------------------------------------------------------------- - -// Queue: -const unique head: Field ref; -const unique tail: Field ref; -const unique mynodes: Field [ref]bool; -// Node: -const unique data: Field T; -const unique next: Field ref; - -function ValidQueue(HeapType, ref) returns (bool); -axiom (forall h: HeapType, q: ref :: - { ValidQueue(h, q) } - q != null && h[q,alloc] ==> - (ValidQueue(h, q) <==> - h[q,head] != null && h[h[q,head],alloc] && - h[q,tail] != null && h[h[q,tail],alloc] && - h[h[q,tail], next] == null && - // The following line can be suppressed now that we have a ValidFootprint invariant - (forall o: ref :: { h[q,footprint][o] } o != null && h[q,footprint][o] ==> h[o,alloc]) && - h[q,footprint][q] && - h[q,mynodes][h[q,head]] && h[q,mynodes][h[q,tail]] && - (forall n: ref :: { h[q,mynodes][n] } - h[q,mynodes][n] ==> - n != null && h[n,alloc] && ValidNode(h, n) && - SubSet(h[n,footprint], h[q,footprint]) && - !h[n,footprint][q] && - (h[n,next] == null ==> n == h[q,tail]) - ) && - (forall n: ref :: { h[n,next] } - h[q,mynodes][n] ==> - (h[n,next] != null ==> h[q,mynodes][h[n,next]]) - ) && - h[q,abstractValue] == h[h[q,head],abstractValue] - )); - -// frame axiom for ValidQueue -axiom (forall h0: HeapType, h1: HeapType, n: ref :: - { ValidQueue(h0,n), ValidQueue(h1,n) } - (forall o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o] - ==> h0[o,f] == h1[o,f]) - && - (forall o: ref, f: Field alpha :: o != null && h1[o,alloc] && h1[n,footprint][o] - ==> h0[o,f] == h1[o,f]) - ==> - ValidQueue(h0,n) == ValidQueue(h1,n)); - -function ValidNode(HeapType, ref) returns (bool); -axiom (forall h: HeapType, n: ref :: - { ValidNode(h, n) } - n != null && h[n,alloc] ==> - (ValidNode(h, n) <==> - // The following line can be suppressed now that we have a ValidFootprint invariant - (forall o: ref :: { h[n,footprint][o] } o != null && h[n,footprint][o] ==> h[o,alloc]) && - h[n,footprint][n] && - (h[n,next] != null ==> - h[h[n,next],alloc] && - SubSet(h[h[n,next], footprint], h[n,footprint]) && - !h[h[n,next], footprint][n]) && - (h[n,next] == null ==> EqualSeq(h[n,abstractValue], EmptySeq)) && - (h[n,next] != null ==> EqualSeq(h[n,abstractValue], - Append(Singleton(h[h[n,next],data]), h[h[n,next],abstractValue]))) - )); - -// frame axiom for ValidNode -axiom (forall h0: HeapType, h1: HeapType, n: ref :: - { ValidNode(h0,n), ValidNode(h1,n) } - (forall o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o] - ==> h0[o,f] == h1[o,f]) - && - (forall o: ref, f: Field alpha :: o != null && h1[o,alloc] && h1[n,footprint][o] - ==> h0[o,f] == h1[o,f]) - ==> - ValidNode(h0,n) == ValidNode(h1,n)); - -// --------------------------------------------------------------- - -procedure MakeQueue() returns (q: ref) - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, EmptySet); - ensures q != null && H[q,alloc]; - ensures AllNewSet(old(H), H[q,footprint]); - ensures ValidQueue(H, q); - ensures Length(H[q,abstractValue]) == 0; -{ - var n: ref; - - assume Fresh(H,q); - H[q,alloc] := true; - - call n := MakeNode(NullT); - H[q,head] := n; - H[q,tail] := n; - H[q,mynodes] := SingletonSet(n); - H[q,footprint] := UnionSet(SingletonSet(q), H[n,footprint]); - H[q,abstractValue] := H[n,abstractValue]; -} - -procedure IsEmpty(q: ref) returns (isEmpty: bool) - requires ValidFootprints(H); - requires q != null && H[q,alloc] && ValidQueue(H, q); - ensures isEmpty <==> Length(H[q,abstractValue]) == 0; -{ - isEmpty := H[q,head] == H[q,tail]; -} - -procedure Enqueue(q: ref, t: T) - requires ValidFootprints(H); - requires q != null && H[q,alloc] && ValidQueue(H, q); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, old(H)[q,footprint]); - ensures DifferenceIsNew(old(H), old(H)[q,footprint], H[q,footprint]); - ensures ValidQueue(H, q); - ensures EqualSeq(H[q,abstractValue], Append(old(H)[q,abstractValue], Singleton(t))); -{ - var n: ref; - - call n := MakeNode(t); - - // foreach m in q.mynodes { m.footprint := m.footprint U n.footprint } - call BulkUpdateFootprint(H[q,mynodes], H[n,footprint]); - H[q,footprint] := UnionSet(H[q,footprint], H[n,footprint]); - - // foreach m in q.mynodes { m.abstractValue := Append(m.abstractValue, Singleton(t)) } - call BulkUpdateAbstractValue(H[q,mynodes], t); - H[q,abstractValue] := H[H[q,head],abstractValue]; - - H[q,mynodes] := UnionSet(H[q,mynodes], SingletonSet(n)); - - H[H[q,tail], next] := n; - H[q,tail] := n; -} - -procedure BulkUpdateFootprint(targetSet: [ref]bool, delta: [ref]bool); - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySetField(old(H), H, targetSet, footprint); - ensures (forall o: ref :: - o != null && old(H)[o,alloc] && targetSet[o] - ==> H[o,footprint] == UnionSet(old(H)[o,footprint], delta)); - -procedure BulkUpdateAbstractValue(targetSet: [ref]bool, t: T); - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySetField(old(H), H, targetSet, abstractValue); - ensures (forall o: ref :: - o != null && old(H)[o,alloc] && targetSet[o] - ==> EqualSeq(H[o,abstractValue], Append(old(H)[o,abstractValue], Singleton(t)))); - -procedure Front(q: ref) returns (t: T) - requires ValidFootprints(H); - requires q != null && H[q,alloc] && ValidQueue(H, q); - requires 0 < Length(H[q,abstractValue]); - ensures t == Index(H[q,abstractValue], 0); -{ - t := H[H[H[q,head], next], data]; -} - -procedure Dequeue(q: ref) - requires ValidFootprints(H); - requires q != null && H[q,alloc] && ValidQueue(H, q); - requires 0 < Length(H[q,abstractValue]); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, old(H)[q,footprint]); - ensures DifferenceIsNew(old(H), old(H)[q,footprint], H[q,footprint]); - ensures ValidQueue(H, q); - ensures EqualSeq(H[q,abstractValue], Drop(old(H)[q,abstractValue], 1)); -{ - var n: ref; - - n := H[H[q,head], next]; - H[q,head] := n; - // we could also remove old(H)[q,head] from H[q,mynodes], and similar for the footprints - H[q,abstractValue] := H[n,abstractValue]; -} - -// -------------------------------------------------------------------------------- - -procedure MakeNode(t: T) returns (n: ref) - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, EmptySet); - ensures n != null && H[n,alloc]; - ensures AllNewSet(old(H), H[n,footprint]); - ensures ValidNode(H, n); - ensures H[n,data] == t && H[n,next] == null; -{ - assume Fresh(H,n); - H[n,alloc] := true; - - H[n,next] := null; - H[n,data] := t; - H[n,footprint] := SingletonSet(n); - H[n,abstractValue] := EmptySeq; -} - -// -------------------------------------------------------------------------------- - -procedure Main(t: T, u: T, v: T) - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, EmptySet); -{ - var q0, q1: ref; - var w: T; - - call q0 := MakeQueue(); - call q1 := MakeQueue(); - - call Enqueue(q0, t); - call Enqueue(q0, u); - - call Enqueue(q1, v); - - assert Length(H[q0,abstractValue]) == 2; - - call w := Front(q0); - assert w == t; - call Dequeue(q0); - - call w := Front(q0); - assert w == u; - - assert Length(H[q0,abstractValue]) == 1; - assert Length(H[q1,abstractValue]) == 1; -} - -// -------------------------------------------------------------------------------- - -procedure Main2(t: T, u: T, v: T, q0: ref, q1: ref) - requires q0 != null && H[q0,alloc] && ValidQueue(H, q0); - requires q1 != null && H[q1,alloc] && ValidQueue(H, q1); - requires DisjointSet(H[q0,footprint], H[q1,footprint]); - requires Length(H[q0,abstractValue]) == 0; - - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, UnionSet(old(H)[q0,footprint], old(H)[q1,footprint])); -{ - var w: T; - - call Enqueue(q0, t); - call Enqueue(q0, u); - - call Enqueue(q1, v); - - assert Length(H[q0,abstractValue]) == 2; - - call w := Front(q0); - assert w == t; - call Dequeue(q0); - - call w := Front(q0); - assert w == u; - - assert Length(H[q0,abstractValue]) == 1; - assert Length(H[q1,abstractValue]) == old(Length(H[q1,abstractValue])) + 1; -} - -// --------------------------------------------------------------- - -// Helpful predicates used in specs - -function ModifiesOnlySet(oldHeap: HeapType, newHeap: HeapType, set: [ref]bool) returns (bool); -axiom (forall oldHeap: HeapType, newHeap: HeapType, set: [ref]bool :: - { ModifiesOnlySet(oldHeap, newHeap, set) } - ModifiesOnlySet(oldHeap, newHeap, set) <==> - NoDeallocs(oldHeap, newHeap) && - (forall o: ref, f: Field alpha :: { newHeap[o,f] } - o != null && oldHeap[o,alloc] ==> - oldHeap[o,f] == newHeap[o,f] || set[o])); - -function ModifiesOnlySetField(oldHeap: HeapType, newHeap: HeapType, - set: [ref]bool, field: Field alpha) returns (bool); -axiom (forall oldHeap: HeapType, newHeap: HeapType, set: [ref]bool, field: Field alpha :: - { ModifiesOnlySetField(oldHeap, newHeap, set, field) } - ModifiesOnlySetField(oldHeap, newHeap, set, field) <==> - NoDeallocs(oldHeap, newHeap) && - (forall o: ref, f: Field beta :: { newHeap[o,f] } - o != null && oldHeap[o,alloc] ==> - oldHeap[o,f] == newHeap[o,f] || (set[o] && f == field))); - -function NoDeallocs(oldHeap: HeapType, newHeap: HeapType) returns (bool); -axiom (forall oldHeap: HeapType, newHeap: HeapType :: - { NoDeallocs(oldHeap, newHeap) } - NoDeallocs(oldHeap, newHeap) <==> - (forall o: ref :: { newHeap[o,alloc] } - o != null && oldHeap[o,alloc] ==> newHeap[o,alloc])); - -function AllNewSet(oldHeap: HeapType, set: [ref]bool) returns (bool); -axiom (forall oldHeap: HeapType, set: [ref]bool :: - { AllNewSet(oldHeap, set) } - AllNewSet(oldHeap, set) <==> - (forall o: ref :: { oldHeap[o,alloc] } - o != null && set[o] ==> !oldHeap[o,alloc])); - -function DifferenceIsNew(oldHeap: HeapType, oldSet: [ref]bool, newSet: [ref]bool) returns (bool); -axiom (forall oldHeap: HeapType, oldSet: [ref]bool, newSet: [ref]bool :: - { DifferenceIsNew(oldHeap, oldSet, newSet) } - DifferenceIsNew(oldHeap, oldSet, newSet) <==> - (forall o: ref :: { oldHeap[o,alloc] } - o != null && !oldSet[o] && newSet[o] ==> !oldHeap[o,alloc])); - -function ValidFootprints(h: HeapType) returns (bool); -axiom (forall h: HeapType :: - { ValidFootprints(h) } - ValidFootprints(h) <==> - (forall o: ref, r: ref :: { h[o,footprint][r] } - o != null && h[o,alloc] && r != null && h[o,footprint][r] ==> h[r,alloc])); - -function Fresh(h: HeapType, o: ref) returns (bool); -axiom (forall h: HeapType, o: ref :: - { Fresh(h,o) } - Fresh(h,o) <==> - o != null && !h[o,alloc] && h[o,footprint] == SingletonSet(o)); - -// --------------------------------------------------------------- - -const EmptySet: [ref]bool; -axiom (forall o: ref :: { EmptySet[o] } !EmptySet[o]); - -function SingletonSet(ref) returns ([ref]bool); -axiom (forall r: ref :: { SingletonSet(r) } SingletonSet(r)[r]); -axiom (forall r: ref, o: ref :: { SingletonSet(r)[o] } SingletonSet(r)[o] <==> r == o); - -function UnionSet([ref]bool, [ref]bool) returns ([ref]bool); -axiom (forall a: [ref]bool, b: [ref]bool, o: ref :: { UnionSet(a,b)[o] } - UnionSet(a,b)[o] <==> a[o] || b[o]); - -function SubSet([ref]bool, [ref]bool) returns (bool); -axiom(forall a: [ref]bool, b: [ref]bool :: { SubSet(a,b) } - SubSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} a[o] ==> b[o])); - -function EqualSet([ref]bool, [ref]bool) returns (bool); -axiom(forall a: [ref]bool, b: [ref]bool :: { EqualSet(a,b) } - EqualSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} a[o] <==> b[o])); - -function DisjointSet([ref]bool, [ref]bool) returns (bool); -axiom (forall a: [ref]bool, b: [ref]bool :: { DisjointSet(a,b) } - DisjointSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} !a[o] || !b[o])); - -// --------------------------------------------------------------- - -// Sequence of T -type Seq; - -function Length(Seq) returns (int); -axiom (forall s: Seq :: { Length(s) } 0 <= Length(s)); - -const EmptySeq: Seq; -axiom Length(EmptySeq) == 0; -axiom (forall s: Seq :: { Length(s) } Length(s) == 0 ==> s == EmptySeq); - -function Singleton(T) returns (Seq); -axiom (forall t: T :: { Length(Singleton(t)) } Length(Singleton(t)) == 1); - -function Append(Seq, Seq) returns (Seq); -axiom (forall s0: Seq, s1: Seq :: { Length(Append(s0,s1)) } - Length(Append(s0,s1)) == Length(s0) + Length(s1)); - -function Index(Seq, int) returns (T); -axiom (forall t: T :: { Index(Singleton(t), 0) } Index(Singleton(t), 0) == t); -axiom (forall s0: Seq, s1: Seq, n: int :: { Index(Append(s0,s1), n) } - (n < Length(s0) ==> Index(Append(s0,s1), n) == Index(s0, n)) && - (Length(s0) <= n ==> Index(Append(s0,s1), n) == Index(s1, n - Length(s0)))); - -function EqualSeq(Seq, Seq) returns (bool); -axiom (forall s0: Seq, s1: Seq :: { EqualSeq(s0,s1) } - EqualSeq(s0,s1) <==> - Length(s0) == Length(s1) && - (forall j: int :: { Index(s0,j) } { Index(s1,j) } - 0 <= j && j < Length(s0) ==> Index(s0,j) == Index(s1,j))); - -function Take(s: Seq, howMany: int) returns (Seq); -axiom (forall s: Seq, n: int :: { Length(Take(s,n)) } - 0 <= n ==> - (n <= Length(s) ==> Length(Take(s,n)) == n) && - (Length(s) < n ==> Length(Take(s,n)) == Length(s))); -axiom (forall s: Seq, n: int, j: int :: { Index(Take(s,n), j) } - 0 <= j && j < n && j < Length(s) ==> - Index(Take(s,n), j) == Index(s, j)); - -function Drop(s: Seq, howMany: int) returns (Seq); -axiom (forall s: Seq, n: int :: { Length(Drop(s,n)) } - 0 <= n ==> - (n <= Length(s) ==> Length(Drop(s,n)) == Length(s) - n) && - (Length(s) < n ==> Length(Drop(s,n)) == 0)); -axiom (forall s: Seq, n: int, j: int :: { Index(Drop(s,n), j) } - 0 <= n && 0 <= j && j < Length(s)-n ==> - Index(Drop(s,n), j) == Index(s, j+n)); - -// --------------------------------------------------------------- diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index 1f5d78df..d098d753 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -3,14 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe -set BPLEXE=%BOOGIEDIR%\Boogie.exe -set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe - -for %%f in (BQueue.bpl) do ( - echo. - echo -------------------- %%f -------------------- - %BPLEXE% %* %%f -) for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy ExtensibleArrayAuto.dfy diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index 93524dfa..9c37549e 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -35,6 +35,10 @@ Dafny program verifier finished with 5 verified, 0 errors Dafny program verifier finished with 3 verified, 0 errors +-------------------- TuringFactorial.dfy -------------------- + +Dafny program verifier finished with 3 verified, 0 errors + -------------------- StoreAndRetrieve.dfy -------------------- Dafny program verifier finished with 22 verified, 0 errors diff --git a/Test/dafny2/TuringFactorial.dfy b/Test/dafny2/TuringFactorial.dfy new file mode 100644 index 00000000..585c998e --- /dev/null +++ b/Test/dafny2/TuringFactorial.dfy @@ -0,0 +1,26 @@ +function Factorial(n: nat): nat +{ + if n == 0 then 1 else n * Factorial(n-1) +} + +method ComputeFactorial(n: int) returns (u: int) + requires 1 <= n; + ensures u == Factorial(n); +{ + var r := 1; + u := 1; + while (r < n) + invariant r <= n; + invariant u == Factorial(r); + { + var v, s := u, 1; + while (s < r + 1) + invariant s <= r + 1; + invariant v == Factorial(r) && u == s * Factorial(r); + { + u := u + v; + s := s + 1; + } + r := r + 1; + } +} diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index 794b7908..b68ba251 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -3,7 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe -set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe REM soon again: SnapshotableTrees.dfy for %%f in ( @@ -14,7 +13,7 @@ for %%f in ( COST-verif-comp-2011-2-MaxTree-datatype.dfy COST-verif-comp-2011-3-TwoDuplicates.dfy COST-verif-comp-2011-4-FloydCycleDetect.dfy - Intervals.dfy TreeFill.dfy + Intervals.dfy TreeFill.dfy TuringFactorial.dfy StoreAndRetrieve.dfy MajorityVote.dfy SegmentSum.dfy ) do ( echo. diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat index efe7b3d5..cd047d39 100644 --- a/Test/vacid0/runtest.bat +++ b/Test/vacid0/runtest.bat @@ -3,8 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe -set BPLEXE=%BOOGIEDIR%\Boogie.exe -set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do ( echo. diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat index 770f41dc..7f7c9b9f 100644 --- a/Test/vstte2012/runtest.bat +++ b/Test/vstte2012/runtest.bat @@ -3,7 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe -set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe for %%f in ( Two-Way-Sort.dfy -- cgit v1.2.3