examples/verifythis_2015_relaxed_prefix.mlw

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