changeset 116:1b8e03af0fef

Corrected the while-loop example (do not say formal proof doen't matter!)
author Sigurd Meldgaard <stm@daimi.au.dk>
date Mon, 26 Oct 2009 10:30:14 +0100
parents c4e0cddc0d7d
children a392a52a9ae3
files examples/while-loop.py
diffstat 1 files changed, 2 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/examples/while-loop.py	Mon Oct 26 10:28:09 2009 +0100
+++ b/examples/while-loop.py	Mon Oct 26 10:30:14 2009 +0100
@@ -1,17 +1,5 @@
-
 from pysmcl.ideal_functionality import ideal_functionality
 
-#@proof_burden
-#@ideal_functionality
-def a(c):
-    precondition("c == 5")
-    y = 4
-    a = open(c)
-    if(c>c):
-        pass
-    else:
-        y = 3
-
 
 @ideal_functionality
 def auction(bids):
@@ -21,12 +9,12 @@
     low = 0
     high = len(bids)
     while(low < high):
-        invariant("bids[high] >= 0 && 0 >= bids[low]")
+        invariant("bids[high] >= 0 and 0 >= bids[low]")
         mid = (low + high) // 2
         r = open(bids[mid] >= 0)
         if r:
             high = mid
         else:
-            low = mid
+            low = mid+1
     result(mid)
     return mid