From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Test/textbook/BQueue.bpl | 864 +++++++++++++++++++------------------- Test/textbook/Bubble.bpl | 164 ++++---- Test/textbook/DivMod.bpl | 130 +++--- Test/textbook/DutchFlag.bpl | 142 +++---- Test/textbook/Find.bpl | 80 ++-- Test/textbook/McCarthy-91.bpl | 28 +- Test/textbook/TuringFactorial.bpl | 70 +-- 7 files changed, 739 insertions(+), 739 deletions(-) (limited to 'Test/textbook') 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 = [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)); - -// --------------------------------------------------------------- +// 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 = [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/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)); -- cgit v1.2.3