Linking Quantifier and Array Length

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

The following fails to verify:

assert:
  forall (int[] xs):
    if:
      |xs| > 0
    then:
      exists (int v):
        xs[0] == v

The generated proof is:

 53. exists(int[] xs).(((((|xs| + 1) >= ((0 + 1) + 1))) && (forall(int v).(( () 
 58. exists(int[] xs).((|xs| >= 1) && forall(int v).(v != xs[0]))     (Simp 53) 
 57. (|xs| >= 1) && forall(int v).(v != xs[0])                    (Exists-E 58) 
 54. |xs| >= 1                                                       (And-E 57) 
 56. forall(int v).(v != xs[0])                                      (And-E 57) 
 59. 0 >= 0                                                    (ArrIdx-I 54,56) 
 61. true                                                             (Simp 59) 
./test_array_06.wyal:1: null

It doesn't seem surprising to me that this happens. I'm not sure how best to tackle this even ...

Whiley / WhileyTheoremProver

Linking Quantifier and Array Length #90