foveoos11_challenge3.mlw 1.58 KB
 Jean-Christophe Filliatre committed Oct 05, 2011 1 2 3 4 5 6 7 8 9 `````` (* FoVeOOS 2011 verification competition http://foveoos2011.cost-ic0701.org/verification-competition Challenge 3 *) module TwoEqualElements `````` Andrei Paskevich committed Jun 15, 2018 10 11 12 `````` use int.Int use ref.Refint use array.Array `````` Jean-Christophe Filliatre committed Oct 05, 2011 13 14 15 16 17 `````` predicate appear_twice (a: array int) (v: int) (u: int) = exists i: int. 0 <= i < u /\ a[i] = v /\ exists j: int. 0 <= j < u /\ j <> i /\ a[j] = v `````` Jean-Christophe Filliatre committed Jun 09, 2018 18 `````` let two_equal_elements (a: array int) (n: int) : (v1:int, v2:int) `````` Andrei Paskevich committed Oct 13, 2012 19 20 21 `````` requires { length a = n+2 /\ n >= 2 } requires { forall i: int. 0 <= i < length a -> 0 <= a[i] < n } requires { `````` Jean-Christophe Filliatre committed Oct 05, 2011 22 23 `````` exists v1: int. appear_twice a v1 (n+2) /\ exists v2: int. appear_twice a v2 (n+2) /\ v2 <> v1 } `````` Jean-Christophe Filliatre committed Jun 09, 2018 24 `````` ensures { `````` Andrei Paskevich committed Oct 13, 2012 25 26 `````` appear_twice a v1 (n+2) /\ appear_twice a v2 (n+2) /\ v1 <> v2 } = let deja_vu = make n False in `````` Jean-Christophe Filliatre committed Oct 05, 2011 27 28 29 `````` let v1 = ref (-1) in let v2 = ref (-1) in for i = 0 to n+1 do `````` Andrei Paskevich committed Oct 13, 2012 30 31 32 33 `````` invariant { !v1 = -1 -> !v2 = -1 } invariant { !v1 <> -1 -> appear_twice a !v1 i } invariant { !v2 <> -1 -> appear_twice a !v2 i /\ !v2 <> !v1 } invariant { forall v: int. 0 <= v < n -> `````` Jean-Christophe Filliatre committed Oct 05, 2011 34 `````` if deja_vu[v]=True then exists j: int. 0 <= j < i /\ a[j] = v `````` Andrei Paskevich committed Oct 13, 2012 35 36 37 38 39 `````` else forall j: int. 0 <= j < i -> a[j] <> v } invariant { !v1 = -1 -> forall v: int. 0 <= v < n -> not (appear_twice a v i) } invariant { !v2 = -1 -> forall v: int. 0 <= v < n -> v <> !v1 -> not (appear_twice a v i) } `````` Jean-Christophe Filliatre committed Oct 05, 2011 40 41 42 43 44 45 46 47 48 49 `````` let v = a[i] in if deja_vu[v] then begin if !v1 = -1 then v1 := v else if !v2 = -1 && v <> !v1 then v2 := v end else deja_vu[v] <- True done; (!v1, !v2) end``````