verifythis_2015_relaxed_prefix.mlw 3.98 KB
 Jean-Christophe Filliatre committed Apr 13, 2015 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 `````` (** {1 VerifyThis @ ETAPS 2015 competition, Challenge 1: Relaxed Prefix} {h The following is the original description of the verification task, reproduced verbatim from the competition web site.
RELAXED PREFIX (60 minutes) ===========================   Description -----------  Verify a function isRelaxedPrefix determining if a list _pat_ (for pattern) is a relaxed prefix of another list _a_.  The relaxed prefix property holds iff _pat_ is a prefix of _a_ after removing at most one element from _pat_.   Examples --------  pat = {1,3}   is a relaxed prefix of a = {1,3,2,3} (standard prefix)  pat = {1,2,3} is a relaxed prefix of a = {1,3,2,3} (remove 2 from pat)  pat = {1,2,4} is not a relaxed prefix of a = {1,3,2,3}.   Implementation notes --------------------  You can implement lists as arrays, e.g., of integers. A reference implementation is given below. It may or may not contain errors.   public class Relaxed {      public static boolean isRelaxedPrefix(int[] pat, int[] a) {         int shift = 0;          for(int i=0; i}  The following is the solution by Jean-Christophe Filliâtre (CNRS) and Guillaume Melquiond (Inria) who entered the competition as "team Why3".  *)  module RelaxedPrefix    use import int.Int   use import ref.Ref   use import array.Array    type char    (** [a1[ofs1..ofs1+len]] and [a2[ofs2..ofs2+len]] are valid sub-arrays       and they are equal *)   predicate eq_array (a1: array char) (ofs1: int)                      (a2: array char) (ofs2: int) (len: int) =     0 <= len /\ 0 <= ofs1 /\ 0 <= ofs2 /\     ofs1 + len <= length a1 /\ ofs2 + len <= length a2 /\     forall i: int. 0 <= i < len -> a1[ofs1 + i] = a2[ofs2 + i]  ``````
Jean-Christophe Filliatre committed Apr 17, 2015  97                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  ``````  (** The target property. *) ``````
Jean-Christophe Filliatre committed Apr 13, 2015  98     99     100     101     102     103     104     105     106     107     108     109     110     111     112     113     114     115     116     117     118     119     120     121     122     123     124     125     126     127     128     129     130     131     132     133                                                                                                                                                                                                                                                                                                                                                                                           ``````   predicate is_relaxed_prefix (pat a: array char) =     let n = length pat in        eq_array pat 0 a 0 n     \/ exists i: int. 0 <= i < n /\                       eq_array pat 0 a 0 i /\                       eq_array pat (i+1) a i (n - i - 1)    (** This exception is used to exit the loop as soon as the target       property is no more possible. *)    exception NoPrefix    (** Note regarding the code: the suggested pseudo-code is buggy, as it       may access [a] out of bounds. We fix it by strengthening the       test in the conditional. *)    let is_relaxed_prefix (pat a: array char) : bool     ensures { result <-> is_relaxed_prefix pat a }   =     let n = length pat in     let m = length a in     try       let shift = ref 0 in       let ghost ignored = ref 0 in       for i = 0 to n - 1 do         invariant { 0 <= !shift <= 1 }         invariant { !shift = 1 -> 0 <= !ignored < i }         invariant { m + !shift >= i }         invariant {           if !shift = 0 then eq_array pat 0 a 0 i           else eq_array pat 0 a 0 !ignored /\                eq_array pat (!ignored + 1) a !ignored (i - !ignored - 1) /\                not (eq_array pat 0 a 0 i) /\                (!ignored < m -> pat[!ignored] <> a[!ignored]) }         if i - !shift >= m || pat[i] <> a[i - !shift] then begin ``````
Martin Clochard committed Apr 17, 2015            134                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 ``````          if !shift = 1 then begin ``````
Jean-Christophe Filliatre committed Apr 17, 2015  135                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 ``````            assert { forall j. eq_array pat 0 a 0 j -> ``````
Martin Clochard committed Apr 17, 2015            136                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 ``````              eq_array pat (j+1) a j (n-j-1) -> ``````
Jean-Christophe Filliatre committed Apr 17, 2015  137     138                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         ``````              !ignored > j -> pat[j+1+(i-j-1)] = a[j+(i-j-1)]             }; ``````
Martin Clochard committed Apr 17, 2015            139     140                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         ``````            raise NoPrefix           end; ``````
Jean-Christophe Filliatre committed Apr 13, 2015  141     142                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         ``````          ignored := i;           shift := 1; ``````
Martin Clochard committed Apr 17, 2015            143                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 ``````        end; ``````
Jean-Christophe Filliatre committed Apr 13, 2015  144     145     146     147     148     149     150                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 ``````      done;       True     with NoPrefix ->       False     end  end``````