Wiki Agenda Contact Version française

VerifyThis 2015: solution to problem 1


Authors: Jean-Christophe Filliâtre / Guillaume Melquiond

Topics: Data Structures

Tools: Why3

References: VerifyThis @ ETAPS 2015

see also the index (by topic, by tool, by reference, by year)




VerifyThis @ ETAPS 2015 competition, Challenge 1: Relaxed Prefix

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]

The target property.

  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
          if !shift = 1 then begin
            assert { forall j. eq_array pat 0 a 0 j ->
              eq_array pat (j+1) a j (n-j-1) ->
              !ignored > j -> pat[j+1+(i-j-1)] = a[j+(i-j-1)]
            };
            raise NoPrefix
          end;
          ignored := i;
          shift := 1;
        end;
      done;
      True
    with NoPrefix ->
      False
    end

end

download ZIP archive

Why3 Proof Results for Project "verifythis_2015_relaxed_prefix"

Theory "verifythis_2015_relaxed_prefix.RelaxedPrefix": fully verified in 0.54 s

ObligationsAlt-Ergo (0.99.1)Z3 (4.3.2)
VC for is_relaxed_prefix------
split_goal_wp
  1. postcondition0.01---
2. loop invariant init0.01---
3. loop invariant init0.02---
4. loop invariant init0.02---
5. loop invariant init0.02---
6. assertion------
split_goal_wp
  1. assertion0.02---
7. postcondition0.02---
8. loop invariant preservation0.01---
9. loop invariant preservation0.02---
10. loop invariant preservation0.01---
11. loop invariant preservation0.03---
12. index in array bounds0.02---
13. index in array bounds0.01---
14. assertion------
split_goal_wp
  1. assertion0.02---
15. postcondition0.02---
16. loop invariant preservation0.02---
17. loop invariant preservation0.02---
18. loop invariant preservation0.01---
19. loop invariant preservation0.100.01
20. loop invariant preservation0.02---
21. loop invariant preservation0.01---
22. loop invariant preservation0.01---
23. loop invariant preservation0.08---
24. postcondition0.00---