From 9f7c11c0a12a9b802f23d613abeee91a2fb47743 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 5 Mar 2013 17:01:25 -0800 Subject: Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codeplex repositories. --- Binaries/DafnyPrelude.bpl | 649 ---------------------------------------------- Binaries/DafnyRuntime.cs | 574 ---------------------------------------- 2 files changed, 1223 deletions(-) delete mode 100644 Binaries/DafnyPrelude.bpl delete mode 100644 Binaries/DafnyRuntime.cs (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl deleted file mode 100644 index 342b72c1..00000000 --- a/Binaries/DafnyPrelude.bpl +++ /dev/null @@ -1,649 +0,0 @@ -// Dafny prelude -// Created 9 February 2008 by Rustan Leino. -// Converted to Boogie 2 on 28 June 2008. -// Edited sequence axioms 20 October 2009 by Alex Summers. -// Copyright (c) 2008-2010, Microsoft. - -const $$Language$Dafny: bool; // To be recognizable to the ModelViewer as -axiom $$Language$Dafny; // coming from a Dafny program. - -// --------------------------------------------------------------- -// -- References ------------------------------------------------- -// --------------------------------------------------------------- - -type ref; -const null: ref; - -// --------------------------------------------------------------- -// -- Axiomatization of sets ------------------------------------- -// --------------------------------------------------------------- - -type Set T = [T]bool; - -function Set#Empty(): Set T; -axiom (forall o: T :: { Set#Empty()[o] } !Set#Empty()[o]); - -function Set#Singleton(T): Set T; -axiom (forall r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]); -axiom (forall r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o); - -function Set#UnionOne(Set T, T): Set T; -axiom (forall a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] } - Set#UnionOne(a,x)[o] <==> o == x || a[o]); -axiom (forall a: Set T, x: T :: { Set#UnionOne(a, x) } - Set#UnionOne(a, x)[x]); -axiom (forall a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] } - a[y] ==> Set#UnionOne(a, x)[y]); - -function Set#Union(Set T, Set T): Set T; -axiom (forall a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] } - Set#Union(a,b)[o] <==> a[o] || b[o]); -axiom (forall a, b: Set T, y: T :: { Set#Union(a, b), a[y] } - a[y] ==> Set#Union(a, b)[y]); -axiom (forall a, b: Set T, y: T :: { Set#Union(a, b), b[y] } - b[y] ==> Set#Union(a, b)[y]); -axiom (forall a, b: Set T :: { Set#Union(a, b) } - Set#Disjoint(a, b) ==> - Set#Difference(Set#Union(a, b), a) == b && - Set#Difference(Set#Union(a, b), b) == a); - -function Set#Intersection(Set T, Set T): Set T; -axiom (forall a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] } - Set#Intersection(a,b)[o] <==> a[o] && b[o]); - -axiom (forall a, b: Set T :: { Set#Union(Set#Union(a, b), b) } - Set#Union(Set#Union(a, b), b) == Set#Union(a, b)); -axiom (forall a, b: Set T :: { Set#Union(a, Set#Union(a, b)) } - Set#Union(a, Set#Union(a, b)) == Set#Union(a, b)); -axiom (forall a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) } - Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b)); -axiom (forall a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) } - Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b)); - -function Set#Difference(Set T, Set T): Set T; -axiom (forall a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] } - Set#Difference(a,b)[o] <==> a[o] && !b[o]); -axiom (forall a, b: Set T, y: T :: { Set#Difference(a, b), b[y] } - b[y] ==> !Set#Difference(a, b)[y] ); - -function Set#Subset(Set T, Set T): bool; -axiom(forall a: Set T, b: Set T :: { Set#Subset(a,b) } - Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o])); - -function Set#Equal(Set T, Set T): bool; -axiom(forall a: Set T, b: Set T :: { Set#Equal(a,b) } - Set#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o])); -axiom(forall a: Set T, b: Set T :: { Set#Equal(a,b) } // extensionality axiom for sets - Set#Equal(a,b) ==> a == b); - -function Set#Disjoint(Set T, Set T): bool; -axiom (forall a: Set T, b: Set T :: { Set#Disjoint(a,b) } - Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o])); - -function Set#Choose(Set T, TickType): T; -axiom (forall a: Set T, tick: TickType :: { Set#Choose(a, tick) } - a != Set#Empty() ==> a[Set#Choose(a, tick)]); - - -// --------------------------------------------------------------- -// -- Axiomatization of multisets -------------------------------- -// --------------------------------------------------------------- - -function Math#min(a: int, b: int): int; -axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a); -axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b); -axiom (forall a: int, b: int :: { Math#min(a, b) } Math#min(a, b) == a || Math#min(a, b) == b); - -function Math#clip(a: int): int; -axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a); -axiom (forall a: int :: { Math#clip(a) } a < 0 ==> Math#clip(a) == 0); - -type MultiSet T = [T]int; - -function $IsGoodMultiSet(ms: MultiSet T): bool; -// ints are non-negative, used after havocing, and for conversion from sequences to multisets. -axiom (forall ms: MultiSet T :: { $IsGoodMultiSet(ms) } - $IsGoodMultiSet(ms) <==> (forall o: T :: { ms[o] } 0 <= ms[o])); - -function MultiSet#Empty(): MultiSet T; -axiom (forall o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0); - -function MultiSet#Singleton(T): MultiSet T; -axiom (forall r: T, o: T :: { MultiSet#Singleton(r)[o] } (MultiSet#Singleton(r)[o] == 1 <==> r == o) && - (MultiSet#Singleton(r)[o] == 0 <==> r != o)); -axiom (forall r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r)); - -function MultiSet#UnionOne(MultiSet T, T): MultiSet T; -// pure containment axiom (in the original multiset or is the added element) -axiom (forall a: MultiSet T, x: T, o: T :: { MultiSet#UnionOne(a,x)[o] } - 0 < MultiSet#UnionOne(a,x)[o] <==> o == x || 0 < a[o]); -// union-ing increases count by one -axiom (forall a: MultiSet T, x: T :: { MultiSet#UnionOne(a, x) } - MultiSet#UnionOne(a, x)[x] == a[x] + 1); -// non-decreasing -axiom (forall a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] } - 0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]); -// other elements unchanged -axiom (forall a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] } - x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]); - -function MultiSet#Union(MultiSet T, MultiSet T): MultiSet T; -// union-ing is the sum of the contents -axiom (forall a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Union(a,b)[o] } - MultiSet#Union(a,b)[o] == a[o] + b[o]); - -// two containment axioms -axiom (forall a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] } - 0 < a[y] ==> 0 < MultiSet#Union(a, b)[y]); -axiom (forall a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), b[y] } - 0 < b[y] ==> 0 < MultiSet#Union(a, b)[y]); - -// symmetry axiom -axiom (forall a, b: MultiSet T :: { MultiSet#Union(a, b) } - MultiSet#Difference(MultiSet#Union(a, b), a) == b && - MultiSet#Difference(MultiSet#Union(a, b), b) == a); - -function MultiSet#Intersection(MultiSet T, MultiSet T): MultiSet T; -axiom (forall a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Intersection(a,b)[o] } - MultiSet#Intersection(a,b)[o] == Math#min(a[o], b[o])); - -// left and right pseudo-idempotence -axiom (forall a, b: MultiSet T :: { MultiSet#Intersection(MultiSet#Intersection(a, b), b) } - MultiSet#Intersection(MultiSet#Intersection(a, b), b) == MultiSet#Intersection(a, b)); -axiom (forall a, b: MultiSet T :: { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) } - MultiSet#Intersection(a, MultiSet#Intersection(a, b)) == MultiSet#Intersection(a, b)); - -// multiset difference, a - b. clip() makes it positive. -function MultiSet#Difference(MultiSet T, MultiSet T): MultiSet T; -axiom (forall a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Difference(a,b)[o] } - MultiSet#Difference(a,b)[o] == Math#clip(a[o] - b[o])); -axiom (forall a, b: MultiSet T, y: T :: { MultiSet#Difference(a, b), b[y], a[y] } - a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0 ); - -// multiset subset means a must have at most as many of each element as b -function MultiSet#Subset(MultiSet T, MultiSet T): bool; -axiom(forall a: MultiSet T, b: MultiSet T :: { MultiSet#Subset(a,b) } - MultiSet#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <= b[o])); - -function MultiSet#Equal(MultiSet T, MultiSet T): bool; -axiom(forall a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) } - MultiSet#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] == b[o])); -// extensionality axiom for multisets -axiom(forall a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) } - MultiSet#Equal(a,b) ==> a == b); - -function MultiSet#Disjoint(MultiSet T, MultiSet T): bool; -axiom (forall a: MultiSet T, b: MultiSet T :: { MultiSet#Disjoint(a,b) } - MultiSet#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] == 0 || b[o] == 0)); - -// conversion to a multiset. each element in the original set has duplicity 1. -function MultiSet#FromSet(Set T): MultiSet T; -axiom (forall s: Set T, a: T :: { MultiSet#FromSet(s)[a] } - (MultiSet#FromSet(s)[a] == 0 <==> !s[a]) && - (MultiSet#FromSet(s)[a] == 1 <==> s[a])); - -// conversion to a multiset, from a sequence. -function MultiSet#FromSeq(Seq T): MultiSet T; -// conversion produces a good map. -axiom (forall s: Seq T :: { MultiSet#FromSeq(s) } $IsGoodMultiSet(MultiSet#FromSeq(s)) ); -// building axiom -axiom (forall s: Seq T, v: T :: - { MultiSet#FromSeq(Seq#Build(s, v)) } - MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v) - ); -axiom (forall :: MultiSet#FromSeq(Seq#Empty(): Seq T) == MultiSet#Empty(): MultiSet T); - -// concatenation axiom -axiom (forall a: Seq T, b: Seq T :: - { MultiSet#FromSeq(Seq#Append(a, b)) } - MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)) ); - -// update axiom -axiom (forall s: Seq T, i: int, v: T, x: T :: - { MultiSet#FromSeq(Seq#Update(s, i, v))[x] } - 0 <= i && i < Seq#Length(s) ==> - MultiSet#FromSeq(Seq#Update(s, i, v))[x] == - MultiSet#Union(MultiSet#Difference(MultiSet#FromSeq(s), MultiSet#Singleton(Seq#Index(s,i))), MultiSet#Singleton(v))[x] ); - // i.e. MS(Update(s, i, v)) == MS(s) - {{s[i]}} + {{v}} -axiom (forall s: Seq T, x: T :: { MultiSet#FromSeq(s)[x] } - (exists i : int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && x == Seq#Index(s,i)) <==> 0 < MultiSet#FromSeq(s)[x] ); - -// --------------------------------------------------------------- -// -- Axiomatization of sequences -------------------------------- -// --------------------------------------------------------------- - -type Seq T; - -function Seq#Length(Seq T): int; -axiom (forall s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s)); - -function Seq#Empty(): Seq T; -axiom (forall :: Seq#Length(Seq#Empty(): Seq T) == 0); -axiom (forall s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty()); - -function Seq#Singleton(T): Seq T; -axiom (forall t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1); - -function Seq#Build(s: Seq T, val: T): Seq T; -axiom (forall s: Seq T, v: T :: { Seq#Length(Seq#Build(s,v)) } - Seq#Length(Seq#Build(s,v)) == 1 + Seq#Length(s)); -axiom (forall s: Seq T, i: int, v: T :: { Seq#Index(Seq#Build(s,v), i) } - (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == v) && - (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == Seq#Index(s, i))); - -function Seq#Append(Seq T, Seq T): Seq T; -axiom (forall s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) } - Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1)); - -function Seq#Index(Seq T, int): T; -axiom (forall t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t); -axiom (forall s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) } - (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) && - (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0)))); - -function Seq#Update(Seq T, int, T): Seq T; -axiom (forall s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) } - 0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s)); -axiom (forall s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v),n) } - 0 <= n && n < Seq#Length(s) ==> - (i == n ==> Seq#Index(Seq#Update(s,i,v),n) == v) && - (i != n ==> Seq#Index(Seq#Update(s,i,v),n) == Seq#Index(s,n))); - -function Seq#Contains(Seq T, T): bool; -axiom (forall s: Seq T, x: T :: { Seq#Contains(s,x) } - Seq#Contains(s,x) <==> - (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x)); -axiom (forall x: ref :: - { Seq#Contains(Seq#Empty(), x) } - !Seq#Contains(Seq#Empty(), x)); -axiom (forall s0: Seq T, s1: Seq T, x: T :: - { Seq#Contains(Seq#Append(s0, s1), x) } - Seq#Contains(Seq#Append(s0, s1), x) <==> - Seq#Contains(s0, x) || Seq#Contains(s1, x)); - -axiom (forall s: Seq T, v: T, x: T :: - { Seq#Contains(Seq#Build(s, v), x) } - Seq#Contains(Seq#Build(s, v), x) <==> (v == x || Seq#Contains(s, x))); - -axiom (forall s: Seq T, n: int, x: T :: - { Seq#Contains(Seq#Take(s, n), x) } - Seq#Contains(Seq#Take(s, n), x) <==> - (exists i: int :: { Seq#Index(s, i) } - 0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x)); -axiom (forall s: Seq T, n: int, x: T :: - { Seq#Contains(Seq#Drop(s, n), x) } - Seq#Contains(Seq#Drop(s, n), x) <==> - (exists i: int :: { Seq#Index(s, i) } - 0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x)); - -function Seq#Equal(Seq T, Seq T): bool; -axiom (forall s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) } - Seq#Equal(s0,s1) <==> - Seq#Length(s0) == Seq#Length(s1) && - (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) } - 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j))); -axiom (forall a: Seq T, b: Seq T :: { Seq#Equal(a,b) } // extensionality axiom for sequences - Seq#Equal(a,b) ==> a == b); - -function Seq#SameUntil(Seq T, Seq T, int): bool; -axiom (forall s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) } - Seq#SameUntil(s0,s1,n) <==> - (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) } - 0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j))); - -function Seq#Take(s: Seq T, howMany: int): Seq T; -axiom (forall s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) } - 0 <= n ==> - (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) && - (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s))); -axiom (forall s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:weight 25} - 0 <= j && j < n && j < Seq#Length(s) ==> - Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j)); - -function Seq#Drop(s: Seq T, howMany: int): Seq T; -axiom (forall s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) } - 0 <= n ==> - (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) && - (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0)); -axiom (forall s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } {:weight 25} - 0 <= n && 0 <= j && j < Seq#Length(s)-n ==> - Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n)); - -axiom (forall s, t: Seq T :: - { Seq#Append(s, t) } - Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s && - Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t); - -function Seq#FromArray(h: HeapType, a: ref): Seq BoxType; -axiom (forall h: HeapType, a: ref :: - { Seq#Length(Seq#FromArray(h,a)) } - Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a)); -axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h,a): Seq BoxType } - (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i)))); -axiom (forall h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref :: - { Seq#FromArray(update(h, o, f, v), a) } - o != a ==> Seq#FromArray(update(h, o, f, v), a) == Seq#FromArray(h, a) ); -axiom (forall h: HeapType, i: int, v: BoxType, a: ref :: - { Seq#FromArray(update(h, a, IndexField(i), v), a) } - 0 <= i && i < _System.array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) ); -/**** Someday: -axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h, a) } - $IsGoodHeap(h) && - a != null && read(h, a, alloc) && dtype(a) == class._System.array && TypeParams(a, 0) == class._System.bool - ==> - (forall i: int :: { Seq#Index(Seq#FromArray(h, a), i) } - 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> $IsCanonicalBoolBox(Seq#Index(Seq#FromArray(h, a), i)))); -****/ - -// Commutability of Take and Drop with Update. -axiom (forall s: Seq T, i: int, v: T, n: int :: - { Seq#Take(Seq#Update(s, i, v), n) } - 0 <= i && i < n && n <= Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) ); -axiom (forall s: Seq T, i: int, v: T, n: int :: - { Seq#Take(Seq#Update(s, i, v), n) } - n <= i && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n)); -axiom (forall s: Seq T, i: int, v: T, n: int :: - { Seq#Drop(Seq#Update(s, i, v), n) } - 0 <= n && n <= i && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i-n, v) ); -axiom (forall s: Seq T, i: int, v: T, n: int :: - { Seq#Drop(Seq#Update(s, i, v), n) } - 0 <= i && i < n && n < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n)); -// Extension axiom, triggers only on Takes from arrays. -axiom (forall h: HeapType, a: ref, n0, n1: int :: - { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) } - n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field BoxType)) ); -// drop commutes with build. -axiom (forall s: Seq T, v: T, n: int :: - { Seq#Drop(Seq#Build(s, v), n) } - 0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) ); - -// Additional axioms about common things -axiom Seq#Take(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][..0] == [] -axiom Seq#Drop(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][0..] == [] - -// --------------------------------------------------------------- -// -- Axiomatization of Maps ------------------------------------- -// --------------------------------------------------------------- - -type Map U V; - -function Map#Domain(Map U V): [U] bool; -function Map#Elements(Map U V): [U]V; - -function Map#Empty(): Map U V; -axiom (forall u: U :: - { Map#Domain(Map#Empty(): Map U V)[u] } - !Map#Domain(Map#Empty(): Map U V)[u]); - -function Map#Glue([U] bool, [U]V): Map U V; -axiom (forall a: [U] bool, b:[U]V :: - { Map#Domain(Map#Glue(a, b)) } - Map#Domain(Map#Glue(a, b)) == a); -axiom (forall a: [U] bool, b:[U]V :: - { Map#Elements(Map#Glue(a, b)) } - Map#Elements(Map#Glue(a, b)) == b); - - -//Build is used in displays, and for map updates -function Map#Build(Map U V, U, V): Map U V; -/*axiom (forall m: Map U V, u: U, v: V :: - { Map#Domain(Map#Build(m, u, v))[u] } { Map#Elements(Map#Build(m, u, v))[u] } - Map#Domain(Map#Build(m, u, v))[u] && Map#Elements(Map#Build(m, u, v))[u] == v);*/ - -axiom (forall m: Map U V, u: U, u': U, v: V :: - { Map#Domain(Map#Build(m, u, v))[u'] } { Map#Elements(Map#Build(m, u, v))[u'] } - (u' == u ==> Map#Domain(Map#Build(m, u, v))[u'] && - Map#Elements(Map#Build(m, u, v))[u'] == v) && - (u' != u ==> Map#Domain(Map#Build(m, u, v))[u'] == Map#Domain(m)[u'] && - Map#Elements(Map#Build(m, u, v))[u'] == Map#Elements(m)[u'])); - -//equality for maps -function Map#Equal(Map U V, Map U V): bool; -axiom (forall m: Map U V, m': Map U V:: - { Map#Equal(m, m') } - Map#Equal(m, m') <==> (forall u : U :: Map#Domain(m)[u] == Map#Domain(m')[u]) && - (forall u : U :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u])); -// extensionality -axiom (forall m: Map U V, m': Map U V:: - { Map#Equal(m, m') } - Map#Equal(m, m') ==> m == m'); - -function Map#Disjoint(Map U V, Map U V): bool; -axiom (forall m: Map U V, m': Map U V :: - { Map#Disjoint(m, m') } - Map#Disjoint(m, m') <==> (forall o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} !Map#Domain(m)[o] || !Map#Domain(m')[o])); - -// --------------------------------------------------------------- -// -- Boxing and unboxing ---------------------------------------- -// --------------------------------------------------------------- - -type BoxType; - -function $Box(T): BoxType; -function $Unbox(BoxType): T; - -axiom (forall x: T :: { $Box(x) } $Unbox($Box(x)) == x); -axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b); -axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b); -axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b); -axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b); -axiom (forall b: BoxType :: { $Unbox(b): Map BoxType BoxType } $Box($Unbox(b): Map BoxType BoxType) == b); -axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b); -// Note: an axiom like this for bool would not be sound; instead, we do: -function $IsCanonicalBoolBox(BoxType): bool; -axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true)); -axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b); - -// --------------------------------------------------------------- -// -- Encoding of type names ------------------------------------- -// --------------------------------------------------------------- - -type ClassName; -const unique class._System.int: ClassName; -const unique class._System.bool: ClassName; -const unique class._System.set: ClassName; -const unique class._System.seq: ClassName; -const unique class._System.multiset: ClassName; -const unique class._System.array: ClassName; - -function /*{:never_pattern true}*/ dtype(ref): ClassName; -function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName; - -function TypeTuple(a: ClassName, b: ClassName): ClassName; -function TypeTupleCar(ClassName): ClassName; -function TypeTupleCdr(ClassName): ClassName; -// TypeTuple is injective in both arguments: -axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } - TypeTupleCar(TypeTuple(a,b)) == a && - TypeTupleCdr(TypeTuple(a,b)) == b); - -// --------------------------------------------------------------- -// -- Datatypes -------------------------------------------------- -// --------------------------------------------------------------- - -type DatatypeType; - -function /*{:never_pattern true}*/ DtType(DatatypeType): ClassName; // the analog of dtype for datatype values -function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int): ClassName; // the analog of TypeParams - -type DtCtorId; -function DatatypeCtorId(DatatypeType): DtCtorId; - -function DtRank(DatatypeType): int; - -// --------------------------------------------------------------- -// -- Axiom contexts --------------------------------------------- -// --------------------------------------------------------------- - -// used to make sure function axioms are not used while their consistency is being checked -const $ModuleContextHeight: int; -const $FunctionContextHeight: int; -const $InMethodContext: bool; - -// --------------------------------------------------------------- -// -- Fields ----------------------------------------------------- -// --------------------------------------------------------------- - -type Field alpha; - -function FDim(Field T): int; - -function IndexField(int): Field BoxType; -axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1); -function IndexField_Inverse(Field T): int; -axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i); - -function MultiIndexField(Field BoxType, int): Field BoxType; -axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) } FDim(MultiIndexField(f,i)) == FDim(f) + 1); -function MultiIndexField_Inverse0(Field T): Field T; -function MultiIndexField_Inverse1(Field T): int; -axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) } - MultiIndexField_Inverse0(MultiIndexField(f,i)) == f && - MultiIndexField_Inverse1(MultiIndexField(f,i)) == i); - - -function DeclType(Field T): ClassName; - -type NameFamily; -function DeclName(Field T): NameFamily; -function FieldOfDecl(ClassName, NameFamily): Field alpha; -axiom (forall cl : ClassName, nm: NameFamily :: - {FieldOfDecl(cl, nm): Field T} - DeclType(FieldOfDecl(cl, nm): Field T) == cl && DeclName(FieldOfDecl(cl, nm): Field T) == nm); - -// --------------------------------------------------------------- -// -- Allocatedness ---------------------------------------------- -// --------------------------------------------------------------- - -const unique alloc: Field bool; -axiom FDim(alloc) == 0; - -function DtAlloc(DatatypeType, HeapType): bool; -axiom (forall h, k: HeapType, d: DatatypeType :: - { $HeapSucc(h, k), DtAlloc(d, h) } - { $HeapSucc(h, k), DtAlloc(d, k) } - $HeapSucc(h, k) ==> DtAlloc(d, h) ==> DtAlloc(d, k)); - -function GenericAlloc(BoxType, HeapType): bool; -axiom (forall h: HeapType, k: HeapType, d: BoxType :: - { $HeapSucc(h, k), GenericAlloc(d, h) } - { $HeapSucc(h, k), GenericAlloc(d, k) } - $HeapSucc(h, k) ==> GenericAlloc(d, h) ==> GenericAlloc(d, k)); -// GenericAlloc ==> -axiom (forall b: BoxType, h: HeapType :: - { GenericAlloc(b, h), h[$Unbox(b): ref, alloc] } - GenericAlloc(b, h) ==> - $Unbox(b): ref == null || h[$Unbox(b): ref, alloc]); -//seqs -axiom (forall b: BoxType, h: HeapType, i: int :: - { GenericAlloc(b, h), Seq#Index($Unbox(b): Seq BoxType, i) } - GenericAlloc(b, h) && - 0 <= i && i < Seq#Length($Unbox(b): Seq BoxType) ==> - GenericAlloc( Seq#Index($Unbox(b): Seq BoxType, i), h ) ); - -//maps -//seq-like axiom, talking about the range elements -axiom (forall b: BoxType, h: HeapType, i: BoxType :: - { GenericAlloc(b, h), Map#Domain($Unbox(b): Map BoxType BoxType)[i] } - GenericAlloc(b, h) && Map#Domain($Unbox(b): Map BoxType BoxType)[i] ==> - GenericAlloc( Map#Elements($Unbox(b): Map BoxType BoxType)[i], h ) ); -//set-like axiom, talking about the domain elements -axiom (forall b: BoxType, h: HeapType, t: BoxType :: - { GenericAlloc(b, h), Map#Domain($Unbox(b): Map BoxType BoxType)[t] } - GenericAlloc(b, h) && Map#Domain($Unbox(b): Map BoxType BoxType)[t] ==> - GenericAlloc(t, h)); - -//sets -axiom (forall b: BoxType, h: HeapType, t: BoxType :: - { GenericAlloc(b, h), ($Unbox(b): Set BoxType)[t] } - GenericAlloc(b, h) && ($Unbox(b): Set BoxType)[t] ==> - GenericAlloc(t, h)); -axiom (forall b: BoxType, h: HeapType :: - { GenericAlloc(b, h), DtType($Unbox(b): DatatypeType) } - GenericAlloc(b, h) ==> DtAlloc($Unbox(b): DatatypeType, h)); -// ==> GenericAlloc -axiom (forall b: bool, h: HeapType :: - $IsGoodHeap(h) ==> GenericAlloc($Box(b), h)); -axiom (forall x: int, h: HeapType :: - $IsGoodHeap(h) ==> GenericAlloc($Box(x), h)); -axiom (forall r: ref, h: HeapType :: - { GenericAlloc($Box(r), h) } - $IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h)); -// boxes in the heap -axiom (forall r: ref, f: Field BoxType, h: HeapType :: - { GenericAlloc(read(h, r, f), h) } - $IsGoodHeap(h) && r != null && read(h, r, alloc) ==> - GenericAlloc(read(h, r, f), h)); - -// --------------------------------------------------------------- -// -- Arrays ----------------------------------------------------- -// --------------------------------------------------------------- - -function _System.array.Length(a: ref): int; -axiom (forall o: ref :: 0 <= _System.array.Length(o)); - -// --------------------------------------------------------------- -// -- The heap --------------------------------------------------- -// --------------------------------------------------------------- - -type HeapType = [ref,Field alpha]alpha; -function {:inline true} read(H:HeapType, r:ref, f:Field alpha): alpha { H[r, f] } -function {:inline true} update(H:HeapType, r:ref, f:Field alpha, v:alpha): HeapType { H[r,f := v] } - -function $IsGoodHeap(HeapType): bool; -var $Heap: HeapType where $IsGoodHeap($Heap); - -function $HeapSucc(HeapType, HeapType): bool; -axiom (forall h: HeapType, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) } - $IsGoodHeap(update(h, r, f, x)) ==> - $HeapSucc(h, update(h, r, f, x))); -axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) } - $HeapSucc(a,b) && $HeapSucc(b,c) ==> $HeapSucc(a,c)); -axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) } - $HeapSucc(h,k) ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc))); - -// --------------------------------------------------------------- -// -- Useful macros ---------------------------------------------- -// --------------------------------------------------------------- - -// havoc everything in $Heap, except {this}+rds+nw -procedure $YieldHavoc(this: ref, rds: Set BoxType, nw: Set BoxType); - modifies $Heap; - ensures (forall $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } - $o != null && read(old($Heap), $o, alloc) ==> - $o == this || rds[$Box($o)] || nw[$Box($o)] ==> - read($Heap, $o, $f) == read(old($Heap), $o, $f)); - ensures $HeapSucc(old($Heap), $Heap); - -// havoc everything in $Heap, except rds-modi-{this} -procedure $IterHavoc0(this: ref, rds: Set BoxType, modi: Set BoxType); - modifies $Heap; - ensures (forall $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } - $o != null && read(old($Heap), $o, alloc) ==> - rds[$Box($o)] && !modi[$Box($o)] && $o != this ==> - read($Heap, $o, $f) == read(old($Heap), $o, $f)); - ensures $HeapSucc(old($Heap), $Heap); - -// havoc $Heap at {this}+modi+nw -procedure $IterHavoc1(this: ref, modi: Set BoxType, nw: Set BoxType); - modifies $Heap; - ensures (forall $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } - $o != null && read(old($Heap), $o, alloc) ==> - read($Heap, $o, $f) == read(old($Heap), $o, $f) || - $o == this || modi[$Box($o)] || nw[$Box($o)]); - ensures $HeapSucc(old($Heap), $Heap); - -procedure $IterCollectNewObjects(prevHeap: HeapType, newHeap: HeapType, this: ref, NW: Field (Set BoxType)) - returns (s: Set BoxType); - ensures (forall bx: BoxType :: { s[bx] } s[bx] <==> - read(newHeap, this, NW)[bx] || - ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc))); - -// --------------------------------------------------------------- -// -- Non-determinism -------------------------------------------- -// --------------------------------------------------------------- - -type TickType; -var $Tick: TickType; - -// --------------------------------------------------------------- diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs deleted file mode 100644 index ac688143..00000000 --- a/Binaries/DafnyRuntime.cs +++ /dev/null @@ -1,574 +0,0 @@ -using System.Numerics; - -namespace Dafny -{ - using System.Collections.Generic; - - public class Set - { - Dictionary dict; - public Set() { } - Set(Dictionary d) { - dict = d; - } - public static Set Empty { - get { - return new Set(new Dictionary(0)); - } - } - public static Set FromElements(params T[] values) { - Dictionary d = new Dictionary(values.Length); - foreach (T t in values) - d[t] = true; - return new Set(d); - } - public static Set FromCollection(ICollection values) { - Dictionary d = new Dictionary(); - foreach (T t in values) - d[t] = true; - return new Set(d); - } - - public IEnumerable Elements { - get { - return dict.Keys; - } - } - public bool Equals(Set other) { - return dict.Count == other.dict.Count && IsSubsetOf(other); - } - public override bool Equals(object other) { - return other is Set && Equals((Set)other); - } - public override int GetHashCode() { - return dict.GetHashCode(); - } - public bool IsProperSubsetOf(Set other) { - return dict.Count < other.dict.Count && IsSubsetOf(other); - } - public bool IsSubsetOf(Set other) { - if (other.dict.Count < dict.Count) - return false; - foreach (T t in dict.Keys) { - if (!other.dict.ContainsKey(t)) - return false; - } - return true; - } - public bool IsSupersetOf(Set other) { - return other.IsSubsetOf(this); - } - public bool IsProperSupersetOf(Set other) { - return other.IsProperSubsetOf(this); - } - public bool IsDisjointFrom(Set other) { - Dictionary a, b; - if (dict.Count < other.dict.Count) { - a = dict; b = other.dict; - } else { - a = other.dict; b = dict; - } - foreach (T t in a.Keys) { - if (b.ContainsKey(t)) - return false; - } - return true; - } - public bool Contains(T t) { - return dict.ContainsKey(t); - } - public Set Union(Set other) { - if (dict.Count == 0) - return other; - else if (other.dict.Count == 0) - return this; - Dictionary a, b; - if (dict.Count < other.dict.Count) { - a = dict; b = other.dict; - } else { - a = other.dict; b = dict; - } - Dictionary r = new Dictionary(); - foreach (T t in b.Keys) - r[t] = true; - foreach (T t in a.Keys) - r[t] = true; - return new Set(r); - } - public Set Intersect(Set other) { - if (dict.Count == 0) - return this; - else if (other.dict.Count == 0) - return other; - Dictionary a, b; - if (dict.Count < other.dict.Count) { - a = dict; b = other.dict; - } else { - a = other.dict; b = dict; - } - var r = new Dictionary(); - foreach (T t in a.Keys) { - if (b.ContainsKey(t)) - r.Add(t, true); - } - return new Set(r); - } - public Set Difference(Set other) { - if (dict.Count == 0) - return this; - else if (other.dict.Count == 0) - return this; - var r = new Dictionary(); - foreach (T t in dict.Keys) { - if (!other.dict.ContainsKey(t)) - r.Add(t, true); - } - return new Set(r); - } - public T Choose() { - foreach (T t in dict.Keys) { - // return the first one - return t; - } - return default(T); - } - } - public class MultiSet - { - Dictionary dict; - public MultiSet() { } - MultiSet(Dictionary d) { - dict = d; - } - public static MultiSet Empty { - get { - return new MultiSet(new Dictionary(0)); - } - } - public static MultiSet FromElements(params T[] values) { - Dictionary d = new Dictionary(values.Length); - foreach (T t in values) { - var i = 0; - if (!d.TryGetValue(t, out i)) { - i = 0; - } - d[t] = i + 1; - } - return new MultiSet(d); - } - public static MultiSet FromCollection(ICollection values) { - Dictionary d = new Dictionary(); - foreach (T t in values) { - var i = 0; - if (!d.TryGetValue(t, out i)) { - i = 0; - } - d[t] = i + 1; - } - return new MultiSet(d); - } - public static MultiSet FromSeq(Sequence values) { - Dictionary d = new Dictionary(); - foreach (T t in values.Elements) { - var i = 0; - if (!d.TryGetValue(t, out i)) { - i = 0; - } - d[t] = i + 1; - } - return new MultiSet(d); - } - public static MultiSet FromSet(Set values) { - Dictionary d = new Dictionary(); - foreach (T t in values.Elements) { - d[t] = 1; - } - return new MultiSet(d); - } - - public bool Equals(MultiSet other) { - return other.IsSubsetOf(this) && this.IsSubsetOf(other); - } - public override bool Equals(object other) { - return other is MultiSet && Equals((MultiSet)other); - } - public override int GetHashCode() { - return dict.GetHashCode(); - } - public bool IsProperSubsetOf(MultiSet other) { - return !Equals(other) && IsSubsetOf(other); - } - public bool IsSubsetOf(MultiSet other) { - foreach (T t in dict.Keys) { - if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t]) - return false; - } - return true; - } - public bool IsSupersetOf(MultiSet other) { - return other.IsSubsetOf(this); - } - public bool IsProperSupersetOf(MultiSet other) { - return other.IsProperSubsetOf(this); - } - public bool IsDisjointFrom(MultiSet other) { - foreach (T t in dict.Keys) { - if (other.dict.ContainsKey(t)) - return false; - } - foreach (T t in other.dict.Keys) { - if (dict.ContainsKey(t)) - return false; - } - return true; - } - public bool Contains(T t) { - return dict.ContainsKey(t); - } - public MultiSet Union(MultiSet other) { - if (dict.Count == 0) - return other; - else if (other.dict.Count == 0) - return this; - var r = new Dictionary(); - foreach (T t in dict.Keys) { - var i = 0; - if (!r.TryGetValue(t, out i)) { - i = 0; - } - r[t] = i + dict[t]; - } - foreach (T t in other.dict.Keys) { - var i = 0; - if (!r.TryGetValue(t, out i)) { - i = 0; - } - r[t] = i + other.dict[t]; - } - return new MultiSet(r); - } - public MultiSet Intersect(MultiSet other) { - if (dict.Count == 0) - return this; - else if (other.dict.Count == 0) - return other; - var r = new Dictionary(); - foreach (T t in dict.Keys) { - if (other.dict.ContainsKey(t)) { - r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]); - } - } - return new MultiSet(r); - } - public MultiSet Difference(MultiSet other) { // \result == this - other - if (dict.Count == 0) - return this; - else if (other.dict.Count == 0) - return this; - var r = new Dictionary(); - foreach (T t in dict.Keys) { - if (!other.dict.ContainsKey(t)) { - r.Add(t, dict[t]); - } else if (other.dict[t] < dict[t]) { - r.Add(t, dict[t] - other.dict[t]); - } - } - return new MultiSet(r); - } - public IEnumerable Elements { - get { - List l = new List(); - foreach (T t in dict.Keys) { - int n; - dict.TryGetValue(t, out n); - for (int i = 0; i < n; i ++) { - l.Add(t); - } - } - return l; - } - } - } - - public class Map - { - Dictionary dict; - public Map() { } - Map(Dictionary d) { - dict = d; - } - public static Map Empty { - get { - return new Map(new Dictionary()); - } - } - public static Map FromElements(params Pair[] values) { - Dictionary d = new Dictionary(values.Length); - foreach (Pair p in values) { - d[p.Car] = p.Cdr; - } - return new Map(d); - } - public static Map FromCollection(List> values) { - Dictionary d = new Dictionary(values.Count); - foreach (Pair p in values) { - d[p.Car] = p.Cdr; - } - return new Map(d); - } - public bool Equals(Map other) { - foreach (U u in dict.Keys) { - V v1, v2; - if (!dict.TryGetValue(u, out v1)) { - return false; // this shouldn't happen - } - if (!other.dict.TryGetValue(u, out v2)) { - return false; // other dictionary does not contain this element - } - if (!v1.Equals(v2)) { - return false; - } - } - foreach (U u in other.dict.Keys) { - if (!dict.ContainsKey(u)) { - return false; // this shouldn't happen - } - } - return true; - } - public override bool Equals(object other) { - return other is Map && Equals((Map)other); - } - public override int GetHashCode() { - return dict.GetHashCode(); - } - public bool IsDisjointFrom(Map other) { - foreach (U u in dict.Keys) { - if (other.dict.ContainsKey(u)) - return false; - } - foreach (U u in other.dict.Keys) { - if (dict.ContainsKey(u)) - return false; - } - return true; - } - public bool Contains(U u) { - return dict.ContainsKey(u); - } - public V Select(U index) { - return dict[index]; - } - public Map Update(U index, V val) { - Dictionary d = new Dictionary(dict); - d[index] = val; - return new Map(d); - } - public IEnumerable Domain { - get { - return dict.Keys; - } - } - } - public class Sequence - { - T[] elmts; - public Sequence() { } - public Sequence(T[] ee) { - elmts = ee; - } - public static Sequence Empty { - get { - return new Sequence(new T[0]); - } - } - public static Sequence FromElements(params T[] values) { - return new Sequence(values); - } - public BigInteger Length { - get { return new BigInteger(elmts.Length); } - } - public T[] Elements { - get { - return elmts; - } - } - public IEnumerable UniqueElements { - get { - var st = Set.FromElements(elmts); - return st.Elements; - } - } - public T Select(BigInteger index) { - return elmts[(int)index]; - } - public Sequence Update(BigInteger index, T t) { - T[] a = (T[])elmts.Clone(); - a[(int)index] = t; - return new Sequence(a); - } - public bool Equals(Sequence other) { - int n = elmts.Length; - return n == other.elmts.Length && EqualUntil(other, n); - } - public override bool Equals(object other) { - return other is Sequence && Equals((Sequence)other); - } - public override int GetHashCode() { - return elmts.GetHashCode(); - } - bool EqualUntil(Sequence other, int n) { - for (int i = 0; i < n; i++) { - if (!elmts[i].Equals(other.elmts[i])) - return false; - } - return true; - } - public bool IsProperPrefixOf(Sequence other) { - int n = elmts.Length; - return n < other.elmts.Length && EqualUntil(other, n); - } - public bool IsPrefixOf(Sequence other) { - int n = elmts.Length; - return n <= other.elmts.Length && EqualUntil(other, n); - } - public Sequence Concat(Sequence other) { - if (elmts.Length == 0) - return other; - else if (other.elmts.Length == 0) - return this; - T[] a = new T[elmts.Length + other.elmts.Length]; - System.Array.Copy(elmts, 0, a, 0, elmts.Length); - System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length); - return new Sequence(a); - } - public bool Contains(T t) { - int n = elmts.Length; - for (int i = 0; i < n; i++) { - if (t.Equals(elmts[i])) - return true; - } - return false; - } - public Sequence Take(BigInteger n) { - int m = (int)n; - if (elmts.Length == m) - return this; - T[] a = new T[m]; - System.Array.Copy(elmts, a, m); - return new Sequence(a); - } - public Sequence Drop(BigInteger n) { - if (n.IsZero) - return this; - int m = (int)n; - T[] a = new T[elmts.Length - m]; - System.Array.Copy(elmts, m, a, 0, elmts.Length - m); - return new Sequence(a); - } - } - public struct Pair - { - public readonly A Car; - public readonly B Cdr; - public Pair(A a, B b) { - this.Car = a; - this.Cdr = b; - } - } - public partial class Helpers { - // Computing forall/exists quantifiers - public static bool QuantBool(bool frall, System.Predicate pred) { - if (frall) { - return pred(false) && pred(true); - } else { - return pred(false) || pred(true); - } - } - public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate pred) { - for (BigInteger i = lo; i < hi; i++) { - if (pred(i) != frall) { return !frall; } - } - return frall; - } - public static bool QuantSet(Dafny.Set set, bool frall, System.Predicate pred) { - foreach (var u in set.Elements) { - if (pred(u) != frall) { return !frall; } - } - return frall; - } - public static bool QuantMap(Dafny.Map map, bool frall, System.Predicate pred) { - foreach (var u in map.Domain) { - if (pred(u) != frall) { return !frall; } - } - return frall; - } - public static bool QuantSeq(Dafny.Sequence seq, bool frall, System.Predicate pred) { - foreach (var u in seq.Elements) { - if (pred(u) != frall) { return !frall; } - } - return frall; - } - public static bool QuantDatatype(IEnumerable set, bool frall, System.Predicate pred) { - foreach (var u in set) { - if (pred(u) != frall) { return !frall; } - } - return frall; - } - // Enumerating other collections - public delegate Dafny.Set ComprehensionDelegate(); - public delegate Dafny.Map MapComprehensionDelegate(); - public static IEnumerable AllBooleans { - get { - yield return false; - yield return true; - } - } - // pre: b != 0 - // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation) - public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) { - if (0 <= a.Sign) { - if (0 <= b.Sign) { - // +a +b: a/b - return BigInteger.Divide(a, b); - } else { - // +a -b: -(a/(-b)) - return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b))); - } - } else { - if (0 <= b.Sign) { - // -a +b: -((-a-1)/b) - 1 - return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1; - } else { - // -a -b: ((-a-1)/(-b)) + 1 - return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1; - } - } - } - // pre: b != 0 - // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation) - public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) { - var bp = BigInteger.Abs(b); - if (0 <= a.Sign) { - // +a: a % b' - return BigInteger.Remainder(a, bp); - } else { - // c = ((-a) % b') - // -a: b' - c if c > 0 - // -a: 0 if c == 0 - var c = BigInteger.Remainder(BigInteger.Negate(a), bp); - return c.IsZero ? c : BigInteger.Subtract(bp, c); - } - } - public static Sequence SeqFromArray(T[] array) { - return new Sequence(array); - } - // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the - // method if possible. Method "ExpressionSequence" would be a good candidate for it: - // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)] - public static U ExpressionSequence(T t, U u) - { - return u; - } - } -} -- cgit v1.2.3