summaryrefslogtreecommitdiff
path: root/Test/textbook
diff options
context:
space:
mode:
Diffstat (limited to 'Test/textbook')
-rw-r--r--Test/textbook/BQueue.bpl864
-rw-r--r--Test/textbook/Bubble.bpl164
-rw-r--r--Test/textbook/DivMod.bpl130
-rw-r--r--Test/textbook/DutchFlag.bpl142
-rw-r--r--Test/textbook/Find.bpl80
-rw-r--r--Test/textbook/McCarthy-91.bpl28
-rw-r--r--Test/textbook/TuringFactorial.bpl70
7 files changed, 739 insertions, 739 deletions
diff --git a/Test/textbook/BQueue.bpl b/Test/textbook/BQueue.bpl
index f224334c..3fdc407c 100644
--- a/Test/textbook/BQueue.bpl
+++ b/Test/textbook/BQueue.bpl
@@ -1,432 +1,432 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// 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 = <x>[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<alpha> o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o]
- ==> h0[o,f] == h1[o,f])
- &&
- (forall<alpha> 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<alpha> o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o]
- ==> h0[o,f] == h1[o,f])
- &&
- (forall<alpha> 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<alpha> o: ref, f: Field alpha :: { newHeap[o,f] }
- o != null && oldHeap[o,alloc] ==>
- oldHeap[o,f] == newHeap[o,f] || set[o]));
-
-function ModifiesOnlySetField<alpha>(oldHeap: HeapType, newHeap: HeapType,
- set: [ref]bool, field: Field alpha) returns (bool);
-axiom (forall<alpha> oldHeap: HeapType, newHeap: HeapType, set: [ref]bool, field: Field alpha ::
- { ModifiesOnlySetField(oldHeap, newHeap, set, field) }
- ModifiesOnlySetField(oldHeap, newHeap, set, field) <==>
- NoDeallocs(oldHeap, newHeap) &&
- (forall<beta> 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));
-
-// ---------------------------------------------------------------
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// 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 = <x>[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<alpha> o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o]
+ ==> h0[o,f] == h1[o,f])
+ &&
+ (forall<alpha> 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<alpha> o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o]
+ ==> h0[o,f] == h1[o,f])
+ &&
+ (forall<alpha> 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<alpha> o: ref, f: Field alpha :: { newHeap[o,f] }
+ o != null && oldHeap[o,alloc] ==>
+ oldHeap[o,f] == newHeap[o,f] || set[o]));
+
+function ModifiesOnlySetField<alpha>(oldHeap: HeapType, newHeap: HeapType,
+ set: [ref]bool, field: Field alpha) returns (bool);
+axiom (forall<alpha> oldHeap: HeapType, newHeap: HeapType, set: [ref]bool, field: Field alpha ::
+ { ModifiesOnlySetField(oldHeap, newHeap, set, field) }
+ ModifiesOnlySetField(oldHeap, newHeap, set, field) <==>
+ NoDeallocs(oldHeap, newHeap) &&
+ (forall<beta> 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/textbook/Bubble.bpl b/Test/textbook/Bubble.bpl
index 702b2cc9..a3f16baa 100644
--- a/Test/textbook/Bubble.bpl
+++ b/Test/textbook/Bubble.bpl
@@ -1,82 +1,82 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Bubble Sort, where the specification says the output is a permutation of
-// the input.
-
-// Introduce a constant 'N' and postulate that it is non-negative
-const N: int;
-axiom 0 <= N;
-
-// Declare a map from integers to integers. In the procedure below, 'a' will be
-// treated as an array of 'N' elements, indexed from 0 to less than 'N'.
-var a: [int]int;
-
-// This procedure implements Bubble Sort. One of the postconditions says that,
-// in the final state of the procedure, the array is sorted. The other
-// postconditions say that the final array is a permutation of the initial
-// array. To write that part of the specification, the procedure returns that
-// permutation mapping. That is, out-parameter 'perm' injectively maps the
-// numbers [0..N) to [0..N), as stated by the second and third postconditions.
-// The final postcondition says that 'perm' describes how the elements in
-// 'a' moved: what is now at index 'i' used to be at index 'perm[i]'.
-// Note, the specification says nothing about the elements of 'a' outside the
-// range [0..N). Moreover, Boogie does not prove that the program will terminate.
-
-procedure BubbleSort() returns (perm: [int]int)
- modifies a;
- // array is sorted
- ensures (forall i, j: int :: 0 <= i && i <= j && j < N ==> a[i] <= a[j]);
- // perm is a permutation
- ensures (forall i: int :: 0 <= i && i < N ==> 0 <= perm[i] && perm[i] < N);
- ensures (forall i, j: int :: 0 <= i && i < j && j < N ==> perm[i] != perm[j]);
- // the final array is that permutation of the input array
- ensures (forall i: int :: 0 <= i && i < N ==> a[i] == old(a)[perm[i]]);
-{
- var n, p, tmp: int;
-
- n := 0;
- while (n < N)
- invariant n <= N;
- invariant (forall i: int :: 0 <= i && i < n ==> perm[i] == i);
- {
- perm[n] := n;
- n := n + 1;
- }
-
- while (true)
- invariant 0 <= n && n <= N;
- // array is sorted from n onwards
- invariant (forall i, k: int :: n <= i && i < N && 0 <= k && k < i ==> a[k] <= a[i]);
- // perm is a permutation
- invariant (forall i: int :: 0 <= i && i < N ==> 0 <= perm[i] && perm[i] < N);
- invariant (forall i, j: int :: 0 <= i && i < j && j < N ==> perm[i] != perm[j]);
- // the current array is that permutation of the input array
- invariant (forall i: int :: 0 <= i && i < N ==> a[i] == old(a)[perm[i]]);
- {
- n := n - 1;
- if (n < 0) {
- break;
- }
-
- p := 0;
- while (p < n)
- invariant p <= n;
- // array is sorted from n+1 onwards
- invariant (forall i, k: int :: n+1 <= i && i < N && 0 <= k && k < i ==> a[k] <= a[i]);
- // perm is a permutation
- invariant (forall i: int :: 0 <= i && i < N ==> 0 <= perm[i] && perm[i] < N);
- invariant (forall i, j: int :: 0 <= i && i < j && j < N ==> perm[i] != perm[j]);
- // the current array is that permutation of the input array
- invariant (forall i: int :: 0 <= i && i < N ==> a[i] == old(a)[perm[i]]);
- // a[p] is at least as large as any of the first p elements
- invariant (forall k: int :: 0 <= k && k < p ==> a[k] <= a[p]);
- {
- if (a[p+1] < a[p]) {
- tmp := a[p]; a[p] := a[p+1]; a[p+1] := tmp;
- tmp := perm[p]; perm[p] := perm[p+1]; perm[p+1] := tmp;
- }
-
- p := p + 1;
- }
- }
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Bubble Sort, where the specification says the output is a permutation of
+// the input.
+
+// Introduce a constant 'N' and postulate that it is non-negative
+const N: int;
+axiom 0 <= N;
+
+// Declare a map from integers to integers. In the procedure below, 'a' will be
+// treated as an array of 'N' elements, indexed from 0 to less than 'N'.
+var a: [int]int;
+
+// This procedure implements Bubble Sort. One of the postconditions says that,
+// in the final state of the procedure, the array is sorted. The other
+// postconditions say that the final array is a permutation of the initial
+// array. To write that part of the specification, the procedure returns that
+// permutation mapping. That is, out-parameter 'perm' injectively maps the
+// numbers [0..N) to [0..N), as stated by the second and third postconditions.
+// The final postcondition says that 'perm' describes how the elements in
+// 'a' moved: what is now at index 'i' used to be at index 'perm[i]'.
+// Note, the specification says nothing about the elements of 'a' outside the
+// range [0..N). Moreover, Boogie does not prove that the program will terminate.
+
+procedure BubbleSort() returns (perm: [int]int)
+ modifies a;
+ // array is sorted
+ ensures (forall i, j: int :: 0 <= i && i <= j && j < N ==> a[i] <= a[j]);
+ // perm is a permutation
+ ensures (forall i: int :: 0 <= i && i < N ==> 0 <= perm[i] && perm[i] < N);
+ ensures (forall i, j: int :: 0 <= i && i < j && j < N ==> perm[i] != perm[j]);
+ // the final array is that permutation of the input array
+ ensures (forall i: int :: 0 <= i && i < N ==> a[i] == old(a)[perm[i]]);
+{
+ var n, p, tmp: int;
+
+ n := 0;
+ while (n < N)
+ invariant n <= N;
+ invariant (forall i: int :: 0 <= i && i < n ==> perm[i] == i);
+ {
+ perm[n] := n;
+ n := n + 1;
+ }
+
+ while (true)
+ invariant 0 <= n && n <= N;
+ // array is sorted from n onwards
+ invariant (forall i, k: int :: n <= i && i < N && 0 <= k && k < i ==> a[k] <= a[i]);
+ // perm is a permutation
+ invariant (forall i: int :: 0 <= i && i < N ==> 0 <= perm[i] && perm[i] < N);
+ invariant (forall i, j: int :: 0 <= i && i < j && j < N ==> perm[i] != perm[j]);
+ // the current array is that permutation of the input array
+ invariant (forall i: int :: 0 <= i && i < N ==> a[i] == old(a)[perm[i]]);
+ {
+ n := n - 1;
+ if (n < 0) {
+ break;
+ }
+
+ p := 0;
+ while (p < n)
+ invariant p <= n;
+ // array is sorted from n+1 onwards
+ invariant (forall i, k: int :: n+1 <= i && i < N && 0 <= k && k < i ==> a[k] <= a[i]);
+ // perm is a permutation
+ invariant (forall i: int :: 0 <= i && i < N ==> 0 <= perm[i] && perm[i] < N);
+ invariant (forall i, j: int :: 0 <= i && i < j && j < N ==> perm[i] != perm[j]);
+ // the current array is that permutation of the input array
+ invariant (forall i: int :: 0 <= i && i < N ==> a[i] == old(a)[perm[i]]);
+ // a[p] is at least as large as any of the first p elements
+ invariant (forall k: int :: 0 <= k && k < p ==> a[k] <= a[p]);
+ {
+ if (a[p+1] < a[p]) {
+ tmp := a[p]; a[p] := a[p+1]; a[p+1] := tmp;
+ tmp := perm[p]; perm[p] := perm[p+1]; perm[p+1] := tmp;
+ }
+
+ p := p + 1;
+ }
+ }
+}
diff --git a/Test/textbook/DivMod.bpl b/Test/textbook/DivMod.bpl
index bdbc4f19..0af38ec8 100644
--- a/Test/textbook/DivMod.bpl
+++ b/Test/textbook/DivMod.bpl
@@ -1,65 +1,65 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// This file contains two definitions of integer div/mod (truncated division, as is
-// used in C, C#, Java, and several other languages, and Euclidean division, which
-// has mathematical appeal and is used by SMT Lib) and proves the correct
-// correspondence between the two.
-//
-// Rustan Leino, 23 Sep 2010
-
-function abs(x: int): int { if 0 <= x then x else -x }
-
-function divt(int, int): int;
-function modt(int, int): int;
-
-axiom (forall a,b: int :: divt(a,b)*b + modt(a,b) == a);
-axiom (forall a,b: int ::
- (0 <= a ==> 0 <= modt(a,b) && modt(a,b) < abs(b)) &&
- (a < 0 ==> -abs(b) < modt(a,b) && modt(a,b) <= 0));
-
-function dive(int, int): int;
-function mode(int, int): int;
-
-axiom (forall a,b: int :: dive(a,b)*b + mode(a,b) == a);
-axiom (forall a,b: int :: 0 <= mode(a,b) && mode(a,b) < abs(b));
-
-procedure T_from_E(a,b: int) returns (q,r: int)
- requires b != 0;
- // It would be nice to prove:
- // ensures q == divt(a,b);
- // ensures r == modt(a,b);
- // but since we know that the axioms about divt/modt have unique solutions (for
- // non-zero b), we just prove that the axioms hold.
- ensures q*b + r == a;
- ensures 0 <= a ==> 0 <= r && r < abs(b);
- ensures a < 0 ==> -abs(b) < r && r <= 0;
-{
- // note, this implementation uses only dive/mode
- var qq,rr: int;
- qq := dive(a,b);
- rr := mode(a,b);
-
- q := if 0 <= a || rr == 0 then qq else if 0 <= b then qq+1 else qq-1;
- r := if 0 <= a || rr == 0 then rr else if 0 <= b then rr-b else rr+b;
- assume {:captureState "end of T_from_E"} true;
-}
-
-procedure E_from_T(a,b: int) returns (q,r: int)
- requires b != 0;
- // It would be nice to prove:
- // ensures q == dive(a,b);
- // ensures r == mode(a,b);
- // but since we know that the axioms about dive/mode have unique solutions (for
- // non-zero b), we just prove that the axioms hold.
- ensures q*b + r == a;
- ensures 0 <= r;
- ensures r < abs(b);
-{
- // note, this implementation uses only divt/modt
- var qq,rr: int;
- qq := divt(a,b);
- rr := modt(a,b);
-
- q := if 0 <= rr then qq else if 0 < b then qq-1 else qq+1;
- r := if 0 <= rr then rr else if 0 < b then rr+b else rr-b;
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// This file contains two definitions of integer div/mod (truncated division, as is
+// used in C, C#, Java, and several other languages, and Euclidean division, which
+// has mathematical appeal and is used by SMT Lib) and proves the correct
+// correspondence between the two.
+//
+// Rustan Leino, 23 Sep 2010
+
+function abs(x: int): int { if 0 <= x then x else -x }
+
+function divt(int, int): int;
+function modt(int, int): int;
+
+axiom (forall a,b: int :: divt(a,b)*b + modt(a,b) == a);
+axiom (forall a,b: int ::
+ (0 <= a ==> 0 <= modt(a,b) && modt(a,b) < abs(b)) &&
+ (a < 0 ==> -abs(b) < modt(a,b) && modt(a,b) <= 0));
+
+function dive(int, int): int;
+function mode(int, int): int;
+
+axiom (forall a,b: int :: dive(a,b)*b + mode(a,b) == a);
+axiom (forall a,b: int :: 0 <= mode(a,b) && mode(a,b) < abs(b));
+
+procedure T_from_E(a,b: int) returns (q,r: int)
+ requires b != 0;
+ // It would be nice to prove:
+ // ensures q == divt(a,b);
+ // ensures r == modt(a,b);
+ // but since we know that the axioms about divt/modt have unique solutions (for
+ // non-zero b), we just prove that the axioms hold.
+ ensures q*b + r == a;
+ ensures 0 <= a ==> 0 <= r && r < abs(b);
+ ensures a < 0 ==> -abs(b) < r && r <= 0;
+{
+ // note, this implementation uses only dive/mode
+ var qq,rr: int;
+ qq := dive(a,b);
+ rr := mode(a,b);
+
+ q := if 0 <= a || rr == 0 then qq else if 0 <= b then qq+1 else qq-1;
+ r := if 0 <= a || rr == 0 then rr else if 0 <= b then rr-b else rr+b;
+ assume {:captureState "end of T_from_E"} true;
+}
+
+procedure E_from_T(a,b: int) returns (q,r: int)
+ requires b != 0;
+ // It would be nice to prove:
+ // ensures q == dive(a,b);
+ // ensures r == mode(a,b);
+ // but since we know that the axioms about dive/mode have unique solutions (for
+ // non-zero b), we just prove that the axioms hold.
+ ensures q*b + r == a;
+ ensures 0 <= r;
+ ensures r < abs(b);
+{
+ // note, this implementation uses only divt/modt
+ var qq,rr: int;
+ qq := divt(a,b);
+ rr := modt(a,b);
+
+ q := if 0 <= rr then qq else if 0 < b then qq-1 else qq+1;
+ r := if 0 <= rr then rr else if 0 < b then rr+b else rr-b;
+}
diff --git a/Test/textbook/DutchFlag.bpl b/Test/textbook/DutchFlag.bpl
index 8bac6aec..f5ee73bb 100644
--- a/Test/textbook/DutchFlag.bpl
+++ b/Test/textbook/DutchFlag.bpl
@@ -1,71 +1,71 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// The partition step of Quick Sort picks a 'pivot' element from a specified subsection
-// of a given integer array. It then partially sorts the elements of the array so that
-// elements smaller than the pivot end up to the left of the pivot and elements larger
-// than the pivot end up to the right of the pivot. Finally, the index of the pivot is
-// returned.
-// The procedure below always picks the first element of the subregion as the pivot.
-// The specification of the procedure talks about the ordering of the elements, but
-// does not say anything about keeping the multiset of elements the same.
-
-var A: [int]int;
-const N: int;
-
-procedure Partition(l: int, r: int) returns (result: int)
- requires 0 <= l && l+2 <= r && r <= N;
- modifies A;
- ensures l <= result && result < r;
- ensures (forall k: int, j: int :: l <= k && k < result && result <= j && j < r ==> A[k] <= A[j]);
- ensures (forall k: int :: l <= k && k < result ==> A[k] <= old(A)[l]);
- ensures (forall k: int :: result <= k && k < r ==> old(A)[l] <= A[k]);
-{
- var pv, i, j, tmp: int;
-
- pv := A[l];
- i := l;
- j := r-1;
- // swap A[l] and A[j]
- tmp := A[l];
- A[l] := A[j];
- A[j] := tmp;
- goto LoopHead;
-
- // The following loop iterates while 'i < j'. In each iteration,
- // one of the three alternatives (A, B, or C) is chosen in such
- // a way that the assume statements will evaluate to true.
- LoopHead:
- // The following the assert statements give the loop invariant
- assert (forall k: int :: l <= k && k < i ==> A[k] <= pv);
- assert (forall k: int :: j <= k && k < r ==> pv <= A[k]);
- assert l <= i && i <= j && j < r;
- goto A, B, C, exit;
-
- A:
- assume i < j;
- assume A[i] <= pv;
- i := i + 1;
- goto LoopHead;
-
- B:
- assume i < j;
- assume pv <= A[j-1];
- j := j - 1;
- goto LoopHead;
-
- C:
- assume i < j;
- assume A[j-1] < pv && pv < A[i];
- // swap A[j-1] and A[i]
- tmp := A[i];
- A[i] := A[j-1];
- A[j-1] := tmp;
- assert A[i] < pv && pv < A[j-1];
- i := i + 1;
- j := j - 1;
- goto LoopHead;
-
- exit:
- assume i == j;
- result := i;
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// The partition step of Quick Sort picks a 'pivot' element from a specified subsection
+// of a given integer array. It then partially sorts the elements of the array so that
+// elements smaller than the pivot end up to the left of the pivot and elements larger
+// than the pivot end up to the right of the pivot. Finally, the index of the pivot is
+// returned.
+// The procedure below always picks the first element of the subregion as the pivot.
+// The specification of the procedure talks about the ordering of the elements, but
+// does not say anything about keeping the multiset of elements the same.
+
+var A: [int]int;
+const N: int;
+
+procedure Partition(l: int, r: int) returns (result: int)
+ requires 0 <= l && l+2 <= r && r <= N;
+ modifies A;
+ ensures l <= result && result < r;
+ ensures (forall k: int, j: int :: l <= k && k < result && result <= j && j < r ==> A[k] <= A[j]);
+ ensures (forall k: int :: l <= k && k < result ==> A[k] <= old(A)[l]);
+ ensures (forall k: int :: result <= k && k < r ==> old(A)[l] <= A[k]);
+{
+ var pv, i, j, tmp: int;
+
+ pv := A[l];
+ i := l;
+ j := r-1;
+ // swap A[l] and A[j]
+ tmp := A[l];
+ A[l] := A[j];
+ A[j] := tmp;
+ goto LoopHead;
+
+ // The following loop iterates while 'i < j'. In each iteration,
+ // one of the three alternatives (A, B, or C) is chosen in such
+ // a way that the assume statements will evaluate to true.
+ LoopHead:
+ // The following the assert statements give the loop invariant
+ assert (forall k: int :: l <= k && k < i ==> A[k] <= pv);
+ assert (forall k: int :: j <= k && k < r ==> pv <= A[k]);
+ assert l <= i && i <= j && j < r;
+ goto A, B, C, exit;
+
+ A:
+ assume i < j;
+ assume A[i] <= pv;
+ i := i + 1;
+ goto LoopHead;
+
+ B:
+ assume i < j;
+ assume pv <= A[j-1];
+ j := j - 1;
+ goto LoopHead;
+
+ C:
+ assume i < j;
+ assume A[j-1] < pv && pv < A[i];
+ // swap A[j-1] and A[i]
+ tmp := A[i];
+ A[i] := A[j-1];
+ A[j-1] := tmp;
+ assert A[i] < pv && pv < A[j-1];
+ i := i + 1;
+ j := j - 1;
+ goto LoopHead;
+
+ exit:
+ assume i == j;
+ result := i;
+}
diff --git a/Test/textbook/Find.bpl b/Test/textbook/Find.bpl
index 5a77c621..758ba4cc 100644
--- a/Test/textbook/Find.bpl
+++ b/Test/textbook/Find.bpl
@@ -1,40 +1,40 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Declare a constant 'K' and a function 'f' and postulate that 'K' is
-// in the image of 'f'
-const K: int;
-function f(int) returns (int);
-axiom (exists k: int :: f(k) == K);
-
-// This procedure will find a domain value 'k' that 'f' maps to 'K'. It will
-// do that by recursively enlarging the range where no such domain value exists.
-// Note, Boogie does not prove termination.
-procedure Find(a: int, b: int) returns (k: int)
- requires a <= b;
- requires (forall j: int :: a < j && j < b ==> f(j) != K);
- ensures f(k) == K;
-{
- goto A, B, C; // nondeterministically choose one of these 3 goto targets
-
- A:
- assume f(a) == K; // assume we get here only if 'f' maps 'a' to 'K'
- k := a;
- return;
-
- B:
- assume f(b) == K; // assume we get here only if 'f' maps 'b' to 'K'
- k := b;
- return;
-
- C:
- assume f(a) != K && f(b) != K; // neither of the two above
- call k := Find(a-1, b+1);
- return;
-}
-
-// This procedure shows one way to call 'Find'
-procedure Main() returns (k: int)
- ensures f(k) == K;
-{
- call k := Find(0, 0);
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Declare a constant 'K' and a function 'f' and postulate that 'K' is
+// in the image of 'f'
+const K: int;
+function f(int) returns (int);
+axiom (exists k: int :: f(k) == K);
+
+// This procedure will find a domain value 'k' that 'f' maps to 'K'. It will
+// do that by recursively enlarging the range where no such domain value exists.
+// Note, Boogie does not prove termination.
+procedure Find(a: int, b: int) returns (k: int)
+ requires a <= b;
+ requires (forall j: int :: a < j && j < b ==> f(j) != K);
+ ensures f(k) == K;
+{
+ goto A, B, C; // nondeterministically choose one of these 3 goto targets
+
+ A:
+ assume f(a) == K; // assume we get here only if 'f' maps 'a' to 'K'
+ k := a;
+ return;
+
+ B:
+ assume f(b) == K; // assume we get here only if 'f' maps 'b' to 'K'
+ k := b;
+ return;
+
+ C:
+ assume f(a) != K && f(b) != K; // neither of the two above
+ call k := Find(a-1, b+1);
+ return;
+}
+
+// This procedure shows one way to call 'Find'
+procedure Main() returns (k: int)
+ ensures f(k) == K;
+{
+ call k := Find(0, 0);
+}
diff --git a/Test/textbook/McCarthy-91.bpl b/Test/textbook/McCarthy-91.bpl
index 6bfbcb04..b4244b8d 100644
--- a/Test/textbook/McCarthy-91.bpl
+++ b/Test/textbook/McCarthy-91.bpl
@@ -1,14 +1,14 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// McCarthy 91 function
-procedure F(n: int) returns (r: int)
- ensures 100 < n ==> r == n - 10;
- ensures n <= 100 ==> r == 91;
-{
- if (100 < n) {
- r := n - 10;
- } else {
- call r := F(n + 11);
- call r := F(r);
- }
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// McCarthy 91 function
+procedure F(n: int) returns (r: int)
+ ensures 100 < n ==> r == n - 10;
+ ensures n <= 100 ==> r == 91;
+{
+ if (100 < n) {
+ r := n - 10;
+ } else {
+ call r := F(n + 11);
+ call r := F(r);
+ }
+}
diff --git a/Test/textbook/TuringFactorial.bpl b/Test/textbook/TuringFactorial.bpl
index dffc36ab..de00e3c0 100644
--- a/Test/textbook/TuringFactorial.bpl
+++ b/Test/textbook/TuringFactorial.bpl
@@ -1,35 +1,35 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// A Boogie version of Turing's additive factorial program, from "Checking a large routine"
-// published in the "Report of a Conference of High Speed Automatic Calculating Machines",
-// pp. 67-69, 1949.
-
-procedure ComputeFactorial(n: int) returns (u: int)
- requires 1 <= n;
- ensures u == Factorial(n);
-{
- var r, v, s: int;
- r, u := 1, 1;
-TOP: // B
- assert r <= n;
- assert u == Factorial(r);
- v := u;
- if (n <= r) { return; }
- s := 1;
-INNER: // E
- assert s <= r;
- assert v == Factorial(r) && u == s * Factorial(r);
- u := u + v;
- s := s + 1;
- assert s - 1 <= r;
- if (s <= r) { goto INNER; }
- r := r + 1;
- goto TOP;
-}
-
-function Factorial(int): int;
-axiom Factorial(0) == 1;
-axiom (forall n: int :: {Factorial(n)} 1 <= n ==> Factorial(n) == n * Factorial_Aux(n-1));
-
-function Factorial_Aux(int): int;
-axiom (forall n: int :: {Factorial(n)} Factorial(n) == Factorial_Aux(n));
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// A Boogie version of Turing's additive factorial program, from "Checking a large routine"
+// published in the "Report of a Conference of High Speed Automatic Calculating Machines",
+// pp. 67-69, 1949.
+
+procedure ComputeFactorial(n: int) returns (u: int)
+ requires 1 <= n;
+ ensures u == Factorial(n);
+{
+ var r, v, s: int;
+ r, u := 1, 1;
+TOP: // B
+ assert r <= n;
+ assert u == Factorial(r);
+ v := u;
+ if (n <= r) { return; }
+ s := 1;
+INNER: // E
+ assert s <= r;
+ assert v == Factorial(r) && u == s * Factorial(r);
+ u := u + v;
+ s := s + 1;
+ assert s - 1 <= r;
+ if (s <= r) { goto INNER; }
+ r := r + 1;
+ goto TOP;
+}
+
+function Factorial(int): int;
+axiom Factorial(0) == 1;
+axiom (forall n: int :: {Factorial(n)} 1 <= n ==> Factorial(n) == n * Factorial_Aux(n-1));
+
+function Factorial_Aux(int): int;
+axiom (forall n: int :: {Factorial(n)} Factorial(n) == Factorial_Aux(n));
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 19:04:10 +0000