verifythis_2015_relaxed_prefix.mlw 3.98 KB
Newer Older
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
<a href="http://etaps2015.verifythis.org/challenges">the competition web site</a>.

<pre>
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<pat.length; i++) {
            if (pat[i]!=a[i-shift])
                if (shift==0) shift=1;
                    else return false;
        }
        return true;
    }


    public static void main(String[] argv) {
        int[] pat = {1,2,3};
        int[] a1 = {1,3,2,3};
        System.out.println(isRelaxedPrefix(pat, a1));
    }

}



Advanced verification task (if you get bored)
---------------------------------------------

Implement and verify a function relaxedContains(pat, a) returning
whether _a_ contains _pat_ in the above relaxed sense, i.e., whether
_pat_ is a relaxed prefix of any suffix of _a_.
</pre>}

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]

97
  (** The target property. *)
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
134
          if !shift = 1 then begin
135
            assert { forall j. eq_array pat 0 a 0 j ->
136
              eq_array pat (j+1) a j (n-j-1) ->
137 138
              !ignored > j -> pat[j+1+(i-j-1)] = a[j+(i-j-1)]
            };
139 140
            raise NoPrefix
          end;
141 142
          ignored := i;
          shift := 1;
143
        end;
144 145 146 147 148 149 150
      done;
      True
    with NoPrefix ->
      False
    end

end