From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/test21/MapAxiomsConsistency.bpl | 206 +++++++++++++++++------------------ 1 file changed, 103 insertions(+), 103 deletions(-) (limited to 'Test/test21/MapAxiomsConsistency.bpl') diff --git a/Test/test21/MapAxiomsConsistency.bpl b/Test/test21/MapAxiomsConsistency.bpl index 4c8302a4..4020c00d 100644 --- a/Test/test21/MapAxiomsConsistency.bpl +++ b/Test/test21/MapAxiomsConsistency.bpl @@ -1,103 +1,103 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" -// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" -// RUN: %diff "%s.p.expect" "%t" -// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" -// RUN: %diff "%s.a.expect" "%t" -// Dafny program verifier version 0.92, Copyright (c) 2003-2008, Microsoft. -// Command Line Options: /trace /typeEncoding:arguments /print:test.bpl test.dfy - -type ref; - -const null: ref; - -type Set T = [T]bool; -function Set#Empty() returns (Set T); -function Set#Singleton(T) returns (Set T); -function Set#UnionOne(Set T, T) returns (Set T); -function Set#Union(Set T, Set T) returns (Set T); -function Set#Intersection(Set T, Set T) returns (Set T); -function Set#Difference(Set T, Set T) returns (Set T); -function Set#Subset(Set T, Set T) returns (bool); -function Set#Equal(Set T, Set T) returns (bool); -function Set#Disjoint(Set T, Set T) returns (bool); - -type Seq _; -function Seq#Length(Seq T) returns (int); -function Seq#Empty() returns (Seq T); -function Seq#Singleton(T) returns (Seq T); -function Seq#Build(s: Seq T, index: int, val: T, newLength: int) returns (Seq T); -function Seq#Append(Seq T, Seq T) returns (Seq T); -function Seq#Index(Seq T, int) returns (T); -function Seq#Contains(Seq T, T) returns (bool); -function Seq#Equal(Seq T, Seq T) returns (bool); -function Seq#SameUntil(Seq T, Seq T, int) returns (bool); -function Seq#Take(s:Seq T, howMany: int) returns (Seq T); -function Seq#Drop(s:Seq T, howMany: int) returns (Seq T); - -type Field _; -type HeapType = [ref,Field alpha]alpha; -function $IsGoodHeap(HeapType) returns (bool); -var $Heap: HeapType where $IsGoodHeap($Heap); -const alloc: Field bool; -function $HeapSucc(HeapType, HeapType) returns (bool); - -const unique Node.list: Field (Seq ref); -const unique Node.footprint: Field [ref]bool; -const unique Node.data: Field ref; -const unique Node.next: Field ref; -function Node.Valid($heap: HeapType, this: ref) returns (bool); - - - - -axiom (forall r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o); - -axiom (forall $Heap: HeapType, this: ref :: { Node.Valid($Heap, this) } this != null && $IsGoodHeap($Heap) ==> Node.Valid($Heap, this) == ($Heap[this, Node.footprint][this] && !$Heap[this, Node.footprint][null] && (forall n: ref :: $Heap[this, Node.footprint][n] ==> $Heap[n, Node.footprint][n] && !$Heap[n, Node.footprint][null] && Set#Subset($Heap[n, Node.footprint], $Heap[this, Node.footprint]) && ($Heap[n, Node.next] == null ==> Seq#Equal($Heap[n, Node.list], Seq#Build(Seq#Empty(), 0, $Heap[n, Node.data], 1))) && ($Heap[n, Node.next] != null ==> $Heap[n, Node.footprint][$Heap[n, Node.next]] && Set#Subset($Heap[$Heap[n, Node.next], Node.footprint], $Heap[n, Node.footprint]) && !$Heap[$Heap[n, Node.next], Node.footprint][n] && Seq#Equal($Heap[n, Node.list], Seq#Append(Seq#Build(Seq#Empty(), 0, $Heap[n, Node.data], 1), $Heap[$Heap[n, Node.next], Node.list])))) && ($Heap[this, Node.next] != null ==> Node.Valid($Heap, $Heap[this, Node.next])))); - - - - -procedure Node.ReverseInPlace(this: ref where this != null && $Heap[this, alloc]) returns (reverse: ref where reverse == null || $Heap[reverse, alloc]); - // user-defined preconditions - free requires Node.Valid($Heap, this); - requires $Heap[this, Node.footprint][this]; - requires !$Heap[this, Node.footprint][null]; - requires $Heap[this, Node.next] != null ==> Node.Valid($Heap, $Heap[this, Node.next]); - modifies $Heap; - // frame condition - // boilerplate - free ensures $HeapSucc(old($Heap), $Heap); - - - -procedure CheckWellformed$$Node.Valid(this: ref where this != null && $Heap[this, alloc]); - - - - - -implementation Node.ReverseInPlace(this: ref) returns (reverse: ref) -{ - var current: ref where current == null || $Heap[current, alloc], $PreLoopHeap0: HeapType, nx: ref where nx == null || $Heap[nx, alloc]; - - // ----- var-declaration statement ----- test.dfy(28,9) - current := $Heap[this, Node.next]; - - - // ----- assignment statement ----- test.dfy(29,13) - reverse := this; - // ----- assignment statement ----- test.dfy(30,18) - $Heap[reverse, Node.next] := null; - assume $IsGoodHeap($Heap); - - - - // ----- assignment statement ----- test.dfy(31,23) - $Heap[reverse, Node.footprint] := // Set#UnionOne(Set#Empty(), reverse); - Set#Singleton(reverse); - - assert current == null; -} - - +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" +// Dafny program verifier version 0.92, Copyright (c) 2003-2008, Microsoft. +// Command Line Options: /trace /typeEncoding:arguments /print:test.bpl test.dfy + +type ref; + +const null: ref; + +type Set T = [T]bool; +function Set#Empty() returns (Set T); +function Set#Singleton(T) returns (Set T); +function Set#UnionOne(Set T, T) returns (Set T); +function Set#Union(Set T, Set T) returns (Set T); +function Set#Intersection(Set T, Set T) returns (Set T); +function Set#Difference(Set T, Set T) returns (Set T); +function Set#Subset(Set T, Set T) returns (bool); +function Set#Equal(Set T, Set T) returns (bool); +function Set#Disjoint(Set T, Set T) returns (bool); + +type Seq _; +function Seq#Length(Seq T) returns (int); +function Seq#Empty() returns (Seq T); +function Seq#Singleton(T) returns (Seq T); +function Seq#Build(s: Seq T, index: int, val: T, newLength: int) returns (Seq T); +function Seq#Append(Seq T, Seq T) returns (Seq T); +function Seq#Index(Seq T, int) returns (T); +function Seq#Contains(Seq T, T) returns (bool); +function Seq#Equal(Seq T, Seq T) returns (bool); +function Seq#SameUntil(Seq T, Seq T, int) returns (bool); +function Seq#Take(s:Seq T, howMany: int) returns (Seq T); +function Seq#Drop(s:Seq T, howMany: int) returns (Seq T); + +type Field _; +type HeapType = [ref,Field alpha]alpha; +function $IsGoodHeap(HeapType) returns (bool); +var $Heap: HeapType where $IsGoodHeap($Heap); +const alloc: Field bool; +function $HeapSucc(HeapType, HeapType) returns (bool); + +const unique Node.list: Field (Seq ref); +const unique Node.footprint: Field [ref]bool; +const unique Node.data: Field ref; +const unique Node.next: Field ref; +function Node.Valid($heap: HeapType, this: ref) returns (bool); + + + + +axiom (forall r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o); + +axiom (forall $Heap: HeapType, this: ref :: { Node.Valid($Heap, this) } this != null && $IsGoodHeap($Heap) ==> Node.Valid($Heap, this) == ($Heap[this, Node.footprint][this] && !$Heap[this, Node.footprint][null] && (forall n: ref :: $Heap[this, Node.footprint][n] ==> $Heap[n, Node.footprint][n] && !$Heap[n, Node.footprint][null] && Set#Subset($Heap[n, Node.footprint], $Heap[this, Node.footprint]) && ($Heap[n, Node.next] == null ==> Seq#Equal($Heap[n, Node.list], Seq#Build(Seq#Empty(), 0, $Heap[n, Node.data], 1))) && ($Heap[n, Node.next] != null ==> $Heap[n, Node.footprint][$Heap[n, Node.next]] && Set#Subset($Heap[$Heap[n, Node.next], Node.footprint], $Heap[n, Node.footprint]) && !$Heap[$Heap[n, Node.next], Node.footprint][n] && Seq#Equal($Heap[n, Node.list], Seq#Append(Seq#Build(Seq#Empty(), 0, $Heap[n, Node.data], 1), $Heap[$Heap[n, Node.next], Node.list])))) && ($Heap[this, Node.next] != null ==> Node.Valid($Heap, $Heap[this, Node.next])))); + + + + +procedure Node.ReverseInPlace(this: ref where this != null && $Heap[this, alloc]) returns (reverse: ref where reverse == null || $Heap[reverse, alloc]); + // user-defined preconditions + free requires Node.Valid($Heap, this); + requires $Heap[this, Node.footprint][this]; + requires !$Heap[this, Node.footprint][null]; + requires $Heap[this, Node.next] != null ==> Node.Valid($Heap, $Heap[this, Node.next]); + modifies $Heap; + // frame condition + // boilerplate + free ensures $HeapSucc(old($Heap), $Heap); + + + +procedure CheckWellformed$$Node.Valid(this: ref where this != null && $Heap[this, alloc]); + + + + + +implementation Node.ReverseInPlace(this: ref) returns (reverse: ref) +{ + var current: ref where current == null || $Heap[current, alloc], $PreLoopHeap0: HeapType, nx: ref where nx == null || $Heap[nx, alloc]; + + // ----- var-declaration statement ----- test.dfy(28,9) + current := $Heap[this, Node.next]; + + + // ----- assignment statement ----- test.dfy(29,13) + reverse := this; + // ----- assignment statement ----- test.dfy(30,18) + $Heap[reverse, Node.next] := null; + assume $IsGoodHeap($Heap); + + + + // ----- assignment statement ----- test.dfy(31,23) + $Heap[reverse, Node.footprint] := // Set#UnionOne(Set#Empty(), reverse); + Set#Singleton(reverse); + + assert current == null; +} + + -- cgit v1.2.3