## 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; iThe 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 equalpredicate 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 NoPrefixNote 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

Obligations | Alt-Ergo (0.99.1) | Z3 (4.3.2) | ||

VC for is_relaxed_prefix | --- | --- | ||

split_goal_wp | ||||

1. postcondition | 0.01 | --- | ||

2. loop invariant init | 0.01 | --- | ||

3. loop invariant init | 0.02 | --- | ||

4. loop invariant init | 0.02 | --- | ||

5. loop invariant init | 0.02 | --- | ||

6. assertion | --- | --- | ||

split_goal_wp | ||||

1. assertion | 0.02 | --- | ||

7. postcondition | 0.02 | --- | ||

8. loop invariant preservation | 0.01 | --- | ||

9. loop invariant preservation | 0.02 | --- | ||

10. loop invariant preservation | 0.01 | --- | ||

11. loop invariant preservation | 0.03 | --- | ||

12. index in array bounds | 0.02 | --- | ||

13. index in array bounds | 0.01 | --- | ||

14. assertion | --- | --- | ||

split_goal_wp | ||||

1. assertion | 0.02 | --- | ||

15. postcondition | 0.02 | --- | ||

16. loop invariant preservation | 0.02 | --- | ||

17. loop invariant preservation | 0.02 | --- | ||

18. loop invariant preservation | 0.01 | --- | ||

19. loop invariant preservation | 0.10 | 0.01 | ||

20. loop invariant preservation | 0.02 | --- | ||

21. loop invariant preservation | 0.01 | --- | ||

22. loop invariant preservation | 0.01 | --- | ||

23. loop invariant preservation | 0.08 | --- | ||

24. postcondition | 0.00 | --- |