diff options
author | rustanleino <unknown> | 2011-03-26 08:54:54 +0000 |
---|---|---|
committer | rustanleino <unknown> | 2011-03-26 08:54:54 +0000 |
commit | d06300cc9bc9f9c7002fb8e555cf172053cdfa5c (patch) | |
tree | 6c19f930d2b568d7d5128b0642e9d823f6014d6b /Binaries | |
parent | bd9003ec46d72f74c3284a63713336da630769ff (diff) |
Dafny: added "choose" operator on sets
Diffstat (limited to 'Binaries')
-rw-r--r-- | Binaries/DafnyPrelude.bpl | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 1ef8aea7..646b16f1 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -80,6 +80,10 @@ function Set#Disjoint<T>(Set T, Set T) returns (bool); axiom (forall<T> 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<T>(Set T, TickType) returns (T);
+axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }
+ a != Set#Empty() ==> a[Set#Choose(a, tick)]);
+
// ---------------------------------------------------------------
// -- Axiomatization of sequences --------------------------------
// ---------------------------------------------------------------
@@ -347,6 +351,13 @@ 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)));
// ---------------------------------------------------------------
+// -- Non-determinism --------------------------------------------
+// ---------------------------------------------------------------
+
+type TickType;
+var $Tick: TickType;
+
+// ---------------------------------------------------------------
// -- Arithmetic -------------------------------------------------
// ---------------------------------------------------------------
|