Commit 04c5c6ce authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

nim.py: passable with trywhy3

parent 7c1e9071
#@ predicate win(n) #@ predicate win(n)
#@ predicate lose(n) #@ predicate lose(n)
#@ assume forall n. n >= 1 -> lose(n) -> win(n) -> False #@ assume forall n. n >= 1 -> not lose(n) or not win(n)
#@ assume lose(1) #@ assume lose(1)
#@ assume forall n. n >= 1 and lose(n) -> win(n+1) \ #@ assume forall n. n >= 1 and lose(n) -> win(n+1) \
...@@ -9,7 +8,6 @@ ...@@ -9,7 +8,6 @@
#@ assume forall n. n >= 1 and win(n) and win(n+1) \ #@ assume forall n. n >= 1 and win(n) and win(n+1) \
#@ and win(n+2) -> lose(n+3) #@ and win(n+2) -> lose(n+3)
# @ assume forall n. n >= 1 -> (lose(n) <-> n % 4 == 1)
def lemma(n): def lemma(n):
#@ requires n >= 1 #@ requires n >= 1
#@ ensures lose(n) <-> n % 4 == 1 #@ ensures lose(n) <-> n % 4 == 1
...@@ -23,9 +21,9 @@ def lemma(n): ...@@ -23,9 +21,9 @@ def lemma(n):
start = int(input("start = ")) start = int(input("start = "))
#@ assume start >= 1 #@ assume start >= 1
n = start n = start
while n > 0: while n >= 1:
#@ invariant lose(start) -> lose(n) #@ invariant win(n) -> win(start)
#@ assert win(n) -> win(start) #@ variant n
print(n, " matches") print(n, " matches")
k = int(input("your turn: ")) k = int(input("your turn: "))
#@ assume k == 1 or k == 2 or k == 3 #@ assume k == 1 or k == 2 or k == 3
...@@ -35,7 +33,6 @@ while n > 0: ...@@ -35,7 +33,6 @@ while n > 0:
print("you lose") print("you lose")
break break
if n == 1: if n == 1:
#@ assert win(n + k)
#@ assert win(start) #@ assert win(start)
print("you win") print("you win")
break break
...@@ -50,5 +47,3 @@ while n > 0: ...@@ -50,5 +47,3 @@ while n > 0:
lemma(n-k) lemma(n-k)
#@ assert win(n) -> lose(n - k) #@ assert win(n) -> lose(n - k)
n = n - k n = n - k
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment