search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

Variable Ordering Effect #91

Closed DavePearce closed 6 years ago

DavePearce commented 7 years ago

The following passes verification:

define contains(int[] env, int n) is:
   exists(int i):
        n <= i
        env[i] == 0

assert "loop invariant not restored":
    forall(int[] env, int n):
        if:
            contains(env,n)
            env[n] != 0
        then:
            contains(env,n+1)

But, if we rename i to p as follows:

define contains(int[] env, int n) is:
   exists(int p):
        n <= p
        env[p] == 0

The key problem seems to be the relative ordering between variable n and i. If i is renamed to something alphabetically above n then it fails. The invalid proof is:

 164. exists(int[] items, int[] nitems, int n).(((invariant(items, n) && upd () 
 170. exists(int[] items, int[] nitems, int n).(invariant(items, n)  (Simp 164) 
 169. invariant(items, n) && update(items, nitems, n) && (0 == n (Exists-E 170) 
 150. invariant(items, n)                                           (And-E 169) 
 153. update(items, nitems, n)                                      (And-E 169) 
 165. 0 == nitems[n]                                                (And-E 169) 
 168. !invariant(nitems, 1 + n)                                     (And-E 169) 
 183. forall(int i).(((((i + 1) >= (n + 1))) || ((items[i] == 0)) (Macro-I 150) 
 197. (|items| == |nitems|) && forall(int j).(((j == n) || (items (Macro-I 153) 
 212. exists(int i).((((((1 + n) + 1) >= ((i + 1) + 1))) && ((nit (Macro-I 168) 
 216. forall(int i).((i >= n) || (0 == items[i]))                    (Simp 183) 
 218. (|items| == |nitems|) && forall(int j).((j == n) || (items[j]  (Simp 197) 
 222. exists(int i).((n >= i) && (0 != nitems[i]))                   (Simp 212) 
 186. |items| == |nitems|                                           (And-E 218) 
 217. forall(int j).((j == n) || (items[j] == nitems[j]))           (And-E 218) 
 221. (n >= i) && (0 != nitems[i])                               (Exists-E 222) 
 223. |nitems| >= (n + 1)                                    (ArrIdx-I 186,165) 
 224. |nitems| >= (i + 1)                                    (ArrIdx-I 186,222) 
 228. (n == n) || (items[n] == nitems[n])                    (Forall-I 217,165) 
 219. n >= i                                                        (And-E 221) 
 220. 0 != nitems[i]                                                (And-E 221) 
 229. |nitems| >= (1 + n)                                            (Simp 223) 
 231. |nitems| >= (1 + i)                                            (Simp 224) 
 233. true                                                           (Simp 228) 
 237. (-1 + |nitems|) >= i                                      (Ieq-I 219,223) 
 238. i >= 0                                                 (ArrIdx-I 224,220) 
 243. (nitems[i] >= (0 + 1)) || (0 >= (nitems[i] + 1))              (Neq-C 220) 
 244. n >= 0                                                 (ArrIdx-I 229,165) 
 245. (-1 + |nitems|) >= 0                                      (Ieq-I 238,231) 
 249. (nitems[i] >= 1) || (0 >= (1 + nitems[i]))                     (Simp 243) 
 250. |nitems| >= 1                                                  (Simp 245) 
┌──────────────────────────────────────────────────────────────────────────────┐
│ 246. nitems[i] >= 1                                               (Or-E 249) │
│ 254. (i == n) || (items[i] == nitems[i])                  (Forall-I 217,246) │
│┌─────────────────────────────────────────────────────────────────────────────┤
││ 251. i == n                                                      (Or-E 254) │
││ 255. 0 == nitems[i]                                          (Eq-S 165,251) │
││ 263. 0 >= 1                                                  (Eq-S 246,255) │
││ 142. false                                                       (Simp 263) │
│├─────────────────────────────────────────────────────────────────────────────┤
││ 253. items[i] == nitems[i]                                       (Or-E 254) │
││ 267. items[i] >= 1                                           (Eq-S 246,253) │
││ 268. |items| >= (i + 1)                                  (ArrIdx-I 186,253) │
││ 271. (i >= n) || (0 == items[i])                         (Forall-I 216,253) │
││ 272. |items| >= (1 + i)                                          (Simp 268) │
││┌────────────────────────────────────────────────────────────────────────────┤
│││ 269. i >= n                                                     (Or-E 271) │
│││ 273. n == i                                                (Ieq-I 269,219) │
│││ 251. i == n                                                (Ieq-I 269,219) │
│││ 274. (-1 + |nitems|) >= n                                  (Ieq-I 269,231) │
│││ 276. (-1 + |items|) >= n                                   (Ieq-I 269,272) │
│││ 277. i == i                                                 (Eq-S 251,273) │
│││ 278. |items| >= (1 + n)                                         (Simp 276) │
││├────────────────────────────────────────────────────────────────────────────┤
│││ 270. 0 == items[i]                                              (Or-E 271) │
││└────────────────────────────────────────────────────────────────────────────┤
│└─────────────────────────────────────────────────────────────────────────────┤
├──────────────────────────────────────────────────────────────────────────────┤
│ 248. 0 >= (1 + nitems[i])                                         (Or-E 249) │
└──────────────────────────────────────────────────────────────────────────────┘

In contrast, the valid proof is:

  164. exists(int[] items, int[] nitems, int n).(((invariant(items, n) && upd () 
 170. exists(int[] items, int[] nitems, int n).(invariant(items, n)  (Simp 164) 
 169. invariant(items, n) && update(items, nitems, n) && (0 == n (Exists-E 170) 
 150. invariant(items, n)                                           (And-E 169) 
 153. update(items, nitems, n)                                      (And-E 169) 
 165. 0 == nitems[n]                                                (And-E 169) 
 168. !invariant(nitems, 1 + n)                                     (And-E 169) 
 183. forall(int p).(((((p + 1) >= (n + 1))) || ((items[p] == 0)) (Macro-I 150) 
 197. (|items| == |nitems|) && forall(int j).(((j == n) || (items (Macro-I 153) 
 212. exists(int p).((((((1 + n) + 1) >= ((p + 1) + 1))) && ((nit (Macro-I 168) 
 216. forall(int p).((p >= n) || (0 == items[p]))                    (Simp 183) 
 218. (|items| == |nitems|) && forall(int j).((j == n) || (items[j]  (Simp 197) 
 222. exists(int p).((n >= p) && (0 != nitems[p]))                   (Simp 212) 
 217. forall(int j).((j == n) || (items[j] == nitems[j]))           (And-E 218) 
 221. (n >= p) && (0 != nitems[p])                               (Exists-E 222) 
 219. n >= p                                                        (And-E 221) 
 220. 0 != nitems[p]                                                (And-E 221) 
 235. (nitems[p] >= (0 + 1)) || (0 >= (nitems[p] + 1))              (Neq-C 220) 
 241. (nitems[p] >= 1) || (0 >= (1 + nitems[p]))                     (Simp 235) 
┌──────────────────────────────────────────────────────────────────────────────┐
│ 238. nitems[p] >= 1                                               (Or-E 241) │
│ 245. (n == p) || (items[p] == nitems[p])                  (Forall-I 217,238) │
│┌─────────────────────────────────────────────────────────────────────────────┤
││ 242. n == p                                                      (Or-E 245) │
││ 246. 0 == nitems[p]                                          (Eq-S 165,242) │
││ 254. 0 >= 1                                                  (Eq-S 238,246) │
││ 142. false                                                       (Simp 254) │
│├─────────────────────────────────────────────────────────────────────────────┤
││ 244. items[p] == nitems[p]                                       (Or-E 245) │
││ 255. items[p] >= 1                                           (Eq-S 238,244) │
││ 259. (p >= n) || (0 == items[p])                         (Forall-I 216,244) │
││┌────────────────────────────────────────────────────────────────────────────┤
│││ 257. p >= n                                                     (Or-E 259) │
│││ 242. n == p                                                (Ieq-I 257,219) │
│││ 246. 0 == nitems[p]                                         (Eq-S 165,242) │
│││ 258. 0 == items[p]                                          (Eq-S 246,244) │
│││ 254. 0 >= 1                                                 (Eq-S 255,258) │
│││ 142. false                                                      (Simp 254) │
││├────────────────────────────────────────────────────────────────────────────┤
│││ 258. 0 == items[p]                                              (Or-E 259) │
│││ 254. 0 >= 1                                                 (Eq-S 255,258) │
│││ 142. false                                                      (Simp 254) │
││└────────────────────────────────────────────────────────────────────────────┤
│└─────────────────────────────────────────────────────────────────────────────┤
├──────────────────────────────────────────────────────────────────────────────┤
│ 240. 0 >= (1 + nitems[p])                                         (Or-E 241) │
│ 245. (n == p) || (items[p] == nitems[p])                  (Forall-I 217,240) │
│┌─────────────────────────────────────────────────────────────────────────────┤
││ 242. n == p                                                      (Or-E 245) │
││ 246. 0 == nitems[p]                                          (Eq-S 165,242) │
││ 263. 0 >= (1 + 0)                                            (Eq-S 240,246) │
││ 142. false                                                       (Simp 263) │
│├─────────────────────────────────────────────────────────────────────────────┤
││ 244. items[p] == nitems[p]                                       (Or-E 245) │
││ 265. 0 >= (1 + items[p])                                     (Eq-S 240,244) │
││ 259. (p >= n) || (0 == items[p])                         (Forall-I 216,244) │
││┌────────────────────────────────────────────────────────────────────────────┤
│││ 257. p >= n                                                     (Or-E 259) │
│││ 242. n == p                                                (Ieq-I 257,219) │
│││ 246. 0 == nitems[p]                                         (Eq-S 165,242) │
│││ 258. 0 == items[p]                                          (Eq-S 246,244) │
│││ 263. 0 >= (1 + 0)                                           (Eq-S 265,258) │
│││ 142. false                                                      (Simp 263) │
││├────────────────────────────────────────────────────────────────────────────┤
│││ 258. 0 == items[p]                                              (Or-E 259) │
│││ 263. 0 >= (1 + 0)                                           (Eq-S 265,258) │
│││ 142. false                                                      (Simp 263) │
││└────────────────────────────────────────────────────────────────────────────┤
│└─────────────────────────────────────────────────────────────────────────────┤
└──────────────────────────────────────────────────────────────────────────────┘