From 53281904797b0d78e18a79cc2d140df7ba4b9086 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 26 Mar 2011 08:54:54 +0000
Subject: Dafny: added "choose" operator on sets

---
 Binaries/DafnyPrelude.bpl | 11 +++++++++++
 Binaries/DafnyRuntime.cs  |  6 ++++++
 2 files changed, 17 insertions(+)

(limited to 'Binaries')

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 --------------------------------
 // ---------------------------------------------------------------
@@ -346,6 +350,13 @@ axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,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)));
 
+// ---------------------------------------------------------------
+// -- Non-determinism --------------------------------------------
+// ---------------------------------------------------------------
+
+type TickType;
+var $Tick: TickType;
+
 // ---------------------------------------------------------------
 // -- Arithmetic -------------------------------------------------
 // ---------------------------------------------------------------
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index f32cc85a..63cca64a 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -117,6 +117,12 @@ namespace Dafny
       }
       return new Set<T>(r);
     }
+    public T Choose() {
+      foreach (T t in dict.Keys) {
+        // return the first one
+        return t;
+      }
+    }
   }
   public class Sequence<T>
   {
-- 
cgit v1.2.3