Wiki Agenda Contact Version française

VerifyThis @ FM 2012, problem 1

Longest Repeated Substring


Authors: Claude Marché / François Bobot

Topics: Array Data Structure / Ghost code / Sorting Algorithms

Tools: Why3

References: VerifyThis @ FM2012

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


download ZIP archive


VerifyThis@fm2012 competition, Challenge 1: Longest Repeated Substring

The following is the original description of the verification task, reproduced verbatim. A reference implementation in Java (based on code by Robert Sedgewick and Kevin Wayne) was also given. The Why3 implementation below follows the Java implementation as faithfully as possible.

Longest Common Prefix (LCP) - 45 minutes

VERIFICATION TASK
-----------------

Longest Common Prefix (LCP) is an algorithm used for text querying. In
the following, we model text as an integer array. You may use other
representations (e.g., Java Strings), if your system supports them.

LCP can be implemented with the pseudocode given below. Formalize and
verify the following informal specification for LCP.

Input:  an integer array a, and two indices x and y into this array
Output: length of the longest common prefix of the subarrays of a
        starting at x and y respectively.

Pseudocode:

    int lcp(int[] a, int x, int y) {
        int l = 0;
        while (x+l<a.length && y+l<a.length && a[x+l]==a[y+l]) {
            l++;
        }
        return l;
    }


ADVANCED
========

BACKGROUND
----------

Together with a suffix array, LCP can be used to solve interesting text
problems, such as finding the longest repeated substring (LRS) in a text.

A suffix array (for a given text) is an array of all suffixes of the
text. For the text [7,8,8,6], the suffix array is
[[7,8,8,6],
   [8,8,6],
     [8,6],
       [6]]

Typically, the suffixes are not stored explicitly as above but
represented as pointers into the original text. The suffixes in a suffix
array  are sorted in lexicographical order. This way, occurrences of
repeated substrings in the original text are neighbors in the suffix
array.

For the above, example (assuming pointers are 0-based integers), the
sorted suffix array is:

[3,0,2,1]

VERIFICATION TASK
-----------------

The attached Java code contains an implementation of a suffix array
(SuffixArray.java), consisting essentially of a lexicographical
comparison on arrays, a sorting routine, and LCP.

The client code (LRS.java) uses these to solve the LRS problem. Verify
that it does so correctly.


First module: longest common prefix

it corresponds to the basic part of the challenge

module LCP

use export int.Int
use import array.Array

is_common_prefix a x y l is true when the prefixes of length l at respective positions x and y in array a are identical. In other words, the array parts ax..x+l-1 and ay..y+l-1 are equal

predicate is_common_prefix (a:array int) (x y l:int) =
  0 <= l /\ x+l <= a.length /\ y+l <= a.length /\
  (forall i:int. 0 <= i < l -> a[x+i] = a[y+i])

This lemma helps for the proof of lcp (but is not mandatory) and is needed later (for le_trans)

lemma not_common_prefix_if_last_char_are_different:
  forall a:array int, x y:int, l:int.
    0 <= l /\ x+l < a.length /\ y+l < a.length /\ a[x+l] <> a[y+l] ->
      not is_common_prefix a x y (l+1)

is_longest_common_prefix a x y l is true when l is the maximal length such that prefixes at positions x and y in array a are identical.

predicate is_longest_common_prefix (a:array int) (x y l:int) =
  is_common_prefix a x y l /\
  forall m:int. l < m -> not (is_common_prefix a x y m)

This lemma helps to proving lcp (but again is not mandatory), and is needed for proving lcp_sym and le_trans lemmas, and the post-condition of compare function in the "absurd" case

lemma longest_common_prefix_succ:
  forall a:array int, x y l:int.
    is_common_prefix a x y l /\ not (is_common_prefix a x y (l+1)) ->
    is_longest_common_prefix a x y l

use export ref.Refint

the first function, that computes the longest common prefix

let lcp (a:array int) (x y:int) : int
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
  ensures { is_longest_common_prefix a x y result }
  = let n = a.length in
    let l = ref 0 in
    while x + !l < n && y + !l < n && a[x + !l] = a[y + !l] do
      invariant { is_common_prefix a x y !l }
      variant { n - !l }
      incr l
    done;
    !l

end

module LCP_test

test harness for lcp

use import array.Array
use import LCP

(*
let test () =
  let arr = Array.make 4 0 in
  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
  let x = lcp arr 1 2 in
  assert { is_common_prefix arr 1 2 1};
  assert { not is_common_prefix arr 1 2 2};
  check { x = 1 };
  (* int[] brr = {1,2,3,5}; *)
  let brr = Array.make 4 0 in
  brr[0]<-1; brr[1]<-2; brr[2]<-3; brr[3]<-5;
  let x = lcp brr 1 2 in
  assert { is_common_prefix brr 1 2 0};
  assert { not is_common_prefix brr 1 2 1};
  check { x = 0 };
  (* int[] crr = {1,2,3,5}; *)
  let crr = Array.make 4 0 in
  crr[0]<-1; crr[1]<-2; crr[2]<-3; crr[3]<-5;
  let x = lcp crr 2 3 in
  assert { is_common_prefix crr 2 3 0};
  assert { not is_common_prefix crr 2 3 1};
  check { x = 0 };
  (* int[] drr = {1,2,3,3}; *)
  let drr = Array.make 4 0 in
  drr[0]<-1; drr[1]<-2; drr[2]<-3; drr[3]<-3;
  let x = lcp drr 2 3 in
  assert { is_common_prefix drr 2 3 1};
  assert { not is_common_prefix drr 2 3 2};
  check {x = 1}
*)

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let arr = Array.make 4 0 in
    arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
    let x = lcp arr 1 2 in
    if x <> 1 then raise BenchFailure;
    x

end

Second module: sorting suffixes

module SuffixSort

  use import int.Int
  use import ref.Refint
  use import array.Array
  use LCP

order by prefix

  predicate lt (a : array int) (x y:int) =
     let n = a.length in
     0 <= x <= n /\ 0 <= y <= n /\
     exists l:int. LCP.is_common_prefix a x y l /\
     (y+l < n /\ (x+l = n \/ a[x+l] < a[y+l]))

comparison function, that decides the order of prefixes

let compare (a:array int) (x y:int) : int
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
  ensures { result = 0 -> x = y }
  ensures { result < 0 -> lt a x y }
  ensures { result > 0 -> lt a y x }
  =
  if x = y then 0 else
  let n = a.length in
  let l = LCP.lcp a x y in
  if x + l = n then -1 else
  if y + l = n then 1 else
  if a[x + l] < a[y + l] then -1 else
  if a[x + l] > a[y + l] then 1 else
  absurd

  use map.MapInjection

range a is true when for each i, a[i] is between 0 at a.length-1

  predicate range (a:array int) = MapInjection.range a.elts a.length

for the permut predicate (permutation of elements)

  use array.ArrayPermut

  predicate le (a : array int) (x y:int) = x = y \/ lt a x y

  (* needed for le_trans (for cases x = y /\ le y z and le x y /\ y = z) *)
  lemma lcp_same_index :
    forall a:array int, x:int.
      0 <= x <= a.length -> LCP.is_longest_common_prefix a x x (a.length - x)

  lemma le_trans : forall a:array int, x y z:int.
    le a x y /\ le a y z -> le a x z

spec of sorted in increasing prefix order

  use map.Map

  predicate sorted_sub (a:array int) (data:Map.map int int) (l u:int) =
    forall i1 i2 : int. l <= i1 <= i2 < u ->
      le a (Map.get data i1) (Map.get data i2)

  predicate sorted (a : array int) (data:array int) =
    sorted_sub a data.elts 0 data.length

let sort (a:array int) (data : array int)
  requires { data.length = a.length }
  requires { range data }
  ensures { sorted a data }
  ensures { ArrayPermut.permut_all (old data) data }
  =
   'Init:
   for i = 0 to data.length - 1 do
     invariant { ArrayPermut.permut_all (at data 'Init) data   }
     invariant { sorted_sub a data.elts 0 i  }
     invariant { range data }
     let j = ref i in
     while !j > 0 && compare a data[!j-1] data[!j] > 0 do
       invariant { 0 <= !j <= i }
       invariant { range data }
       invariant { ArrayPermut.permut_all (at data 'Init) data   }
       invariant { sorted_sub a data.elts 0 !j }
       invariant { sorted_sub a data.elts !j (i+1) }
       invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
                     le a data[k1] data[k2] }
       variant { !j }
       'L:
       let b = !j - 1 in
       let t = data[!j] in
       data[!j] <- data[b];
       data[b] <- t;
       assert { ArrayPermut.exchange (at data 'L) data (!j-1) !j };
       decr j
     done;
     (* needed to prove the invariant [sorted_sub a data.elts 0 i] *)
     assert { !j > 0 -> le a data[!j-1] data[!j] }
   done

end

module SuffixSort_test

  use import int.Int
  use import array.Array
  use LCP
  use SuffixSort

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let arr = Array.make 4 0 in
    (* [7,8,8,6] *)
    arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-6;
    let suf = Array.make 4 0 in
    for i = 0 to 3 do
      invariant { forall j:int. 0 <= j < i -> suf[j] = j }
      suf[i] <- i
    done;
    SuffixSort.sort arr suf;
    (* should be [3,0,2,1] *)
    if suf[0] <> 3 then raise BenchFailure;
    if suf[1] <> 0 then raise BenchFailure;
    if suf[2] <> 2 then raise BenchFailure;
    if suf[3] <> 1 then raise BenchFailure;
    suf

end

Third module: Suffix Array Data Structure

module SuffixArray

use import int.Int
use import array.Array
use LCP
use SuffixSort
use map.Map
use map.MapInjection

predicate permutation (m:Map.map int int) (u : int) =
  MapInjection.range m u /\ MapInjection.injective m u

type suffixArray = {
    values : array int;
    suffixes : array int;
}
invariant { self.values.length = self.suffixes.length /\
  permutation self.suffixes.elts self.suffixes.length /\
  SuffixSort.sorted self.values self.suffixes }

let select (s:suffixArray) (i:int) : int
  requires { 0 <= i < s.values.length }
  ensures { result = s.suffixes[i] }
  = s.suffixes[i]

use array.ArrayPermut

needed to establish invariant in function create

lemma permut_permutation : forall a1 a2:array int.
  ArrayPermut.permut_all a1 a2 /\ permutation a1.elts a1.length ->
    permutation a2.elts a2.length

constructor of suffixArray structure

let create (a:array int) : suffixArray
  ensures { result.values = a }
= let n = a.length in
  let suf = Array.make n 0 in
  for i = 0 to n-1 do
    invariant { forall j:int. 0 <= j < i -> suf[j] = j }
    suf[i] <- i done;
  SuffixSort.sort a suf;
  { values = a; suffixes = suf }

let lcp (s:suffixArray) (i:int) : int
  requires { 0 < i < s.values.length }
  ensures { LCP.is_longest_common_prefix s.values
              s.suffixes[i-1] s.suffixes[i] result }
= LCP.lcp s.values s.suffixes[i] s.suffixes[i-1]

end

module SuffixArray_test

use import array.Array
use import SuffixArray

(*
let test () =
  let arr = Array.make 4 0 in
  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
  let sa = create arr in
  assert { sa.suffixes[0] = 0 };
  assert { sa.suffixes[1] = 1 };
  assert { sa.suffixes[2] = 2 };
  assert { sa.suffixes[3] = 3 };
  let x = lcp sa 1 in
  check {x = 0};
  (* int[] brr = {1,2,3,5}; *)
  let brr = Array.make 4 0 in
  brr[0]<-1; brr[1]<-2; brr[2]<-3; brr[3]<-5;
  let sa = create brr in
  let x = lcp sa 1 in
  check {x = 0 (* TODO *)};
  (* int[] crr = {1,2,3,5}; *)
  let crr = Array.make 4 0 in
  crr[0]<-1; crr[1]<-2; crr[2]<-3; crr[3]<-5;
  let sa = create crr in
  let x = lcp sa 2 in
  check {x = 0 (* TODO *)};
  (* int[] drr = {1,2,3,3}; *)
  let drr = Array.make 4 0 in
  drr[0]<-1; drr[1]<-2; drr[2]<-3; drr[3]<-3;
  let sa = create drr in
  let x = lcp sa 2 in
  check {x = 0 (* TODO *)}
*)

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let arr = Array.make 4 0 in
    (* [7,8,8,6] *)
    arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-6;
    let sa = create arr in
    if sa.suffixes[0] <> 3 then raise BenchFailure;
    if sa.suffixes[1] <> 0 then raise BenchFailure;
    if sa.suffixes[2] <> 2 then raise BenchFailure;
    if sa.suffixes[3] <> 1 then raise BenchFailure;
    sa

end

Fourth module: Longest Repeated Substring

module LRS

  use import int.Int
  use import ref.Ref
  use import array.Array
  use map.MapInjection
  use LCP
  use SuffixSort
  use SuffixArray

additional properties relating le and longest_common_prefix

(* needed for [lrs] function, last before last assert *)
lemma lcp_sym :
  forall a:array int, x y l:int.
     0 <= x <= a.length /\ 0 <= y <= a.length ->
       LCP.is_longest_common_prefix a x y l ->
       LCP.is_longest_common_prefix a y x l

allows CVC to prove the next lemma

lemma le_le_common_prefix:
    forall a:array int, x y z l:int.
     SuffixSort.le a x y /\ SuffixSort.le a y z ->
     LCP.is_common_prefix a x z l -> LCP.is_common_prefix a y z l

proved by Alt-Ergo and CVC. But only by Alt-Ergo if previous lemma is removed

  lemma le_le_longest_common_prefix:
    forall a:array int, x y z l m :int.
     SuffixSort.le a x y /\ SuffixSort.le a y z ->
     LCP.is_longest_common_prefix a x z l /\
     LCP.is_longest_common_prefix a y z m
       -> l <= m

  val solStart : ref int
  val solLength : ref int
  val ghost solStart2 : ref int

  let lrs (a:array int) : unit
    requires { a.length > 0 }
    ensures { 0 <= !solLength <= a.length }
    ensures { 0 <= !solStart <= a.length }
    ensures { 0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
              LCP.is_longest_common_prefix a !solStart !solStart2 !solLength }
    ensures { forall x y l:int.
                0 <= x < y < a.length /\
                LCP.is_longest_common_prefix a x y l ->
                !solLength >= l }
  =
    let sa = SuffixArray.create a in
    solStart := 0;
    solLength := 0;
    solStart2 := a.length;
    for i=1 to a.length - 1 do
      invariant { 0 <= !solLength <= a.length }
      invariant { 0 <= !solStart <= a.length }
      invariant {
           0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
           LCP.is_longest_common_prefix a !solStart !solStart2 !solLength }
      invariant { forall j k l:int.
                  0 <= j < k < i /\
                  LCP.is_longest_common_prefix a
                    sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] l ->
                  !solLength >= l }
      let l = SuffixArray.lcp sa i in
      if l > !solLength then begin
         solStart := SuffixArray.select sa i;
         solStart2 := SuffixArray.select sa (i-1);
         solLength := l
      end
    done;

the following assert needs lcp_sym lemma

    assert { forall j k l:int.
                0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
                 LCP.is_longest_common_prefix a
                 sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] l ->
              !solLength >= l};
    (* we state explicitly that sa.suffixes is surjective *)
    assert { forall x y:int.
                0 <= x < y < a.length ->
                exists j k : int.
                  0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
                  x = sa.SuffixArray.suffixes[j] /\
                  y = sa.SuffixArray.suffixes[k] };
    ()

end

module LRS_test

  use import array.Array
  use import ref.Ref
  use import LRS

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let arr = Array.make 4 0 in
    (* [7,8,8,6] *)
    arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-6;
    lrs arr;
    if !solStart <> 1 then raise BenchFailure;
    if !solLength <> 1 then raise BenchFailure;
    (!solStart, !solLength)

end

Why3 Proof Results for Project "verifythis_fm2012_LRS"

Theory "verifythis_fm2012_LRS.LCP": fully verified in 4.74 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Eprover (1.8-001)Vampire (0.6)Z3 (4.3.2)
not_common_prefix_if_last_char_are_different0.01------------0.01
longest_common_prefix_succ0.02------------0.06
VC for lcp------------------
split_goal_wp
  1. loop invariant init0.020.020.02------0.02
2. index in array bounds0.020.030.010.020.020.02
3. index in array bounds0.020.030.000.020.020.02
4. loop invariant preservation0.01---------------
5. loop variant decrease0.020.020.020.541.160.01
6. postcondition0.01---------------
7. postcondition0.020.020.010.061.03---
8. postcondition0.030.020.000.111.24---

Theory "verifythis_fm2012_LRS.LCP_test": fully verified in 0.02 s

ObligationsAlt-Ergo (0.99.1)
VC for bench0.02

Theory "verifythis_fm2012_LRS.SuffixSort": fully verified in 13.19 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Eprover (1.8-001)Vampire (0.6)Z3 (4.3.2)
VC for compare------------------
split_goal_wp
  1. postcondition0.010.000.000.000.000.00
2. postcondition0.010.020.00------0.00
3. postcondition0.020.000.00------0.00
4. precondition0.020.020.000.000.000.02
5. precondition0.020.010.000.000.000.02
6. postcondition0.000.010.000.000.000.00
7. postcondition0.020.020.020.20------
8. postcondition0.020.010.000.010.050.00
9. postcondition0.010.020.000.000.000.00
10. postcondition0.020.010.000.030.020.00
11. postcondition0.02---------------
12. index in array bounds0.010.020.010.03---0.02
13. index in array bounds0.020.020.000.02---0.02
14. postcondition0.000.020.000.000.010.00
15. postcondition0.000.030.02---------
16. postcondition0.010.020.000.040.020.00
17. index in array bounds0.020.020.000.000.000.00
18. index in array bounds0.020.010.010.000.000.00
19. postcondition0.010.000.000.000.000.00
20. postcondition0.020.010.010.030.020.00
21. postcondition0.02---------------
22. unreachable point0.02---------------
lcp_same_index0.010.010.02------0.01
le_trans0.10---------------
VC for sort------------------
split_goal_wp
  1. postcondition0.010.010.02------0.02
2. postcondition0.010.020.020.310.340.03
3. loop invariant init0.010.020.020.460.340.02
4. loop invariant init0.010.020.02------0.03
5. loop invariant init0.010.000.010.010.010.02
6. loop invariant init0.010.020.020.010.010.02
7. loop invariant init0.010.010.020.010.010.04
8. loop invariant init0.010.010.020.080.040.03
9. loop invariant init0.010.010.020.010.00---
10. loop invariant init0.020.02------------
11. loop invariant init0.010.010.010.130.120.05
12. type invariant0.020.020.020.010.000.02
13. index in array bounds0.010.020.02---1.040.04
14. index in array bounds0.000.020.02------0.03
15. precondition0.020.020.03---0.220.06
16. precondition0.020.020.020.370.210.05
17. index in array bounds0.010.020.020.010.000.03
18. index in array bounds0.010.020.020.010.010.00
19. index in array bounds0.020.020.020.020.010.04
20. index in array bounds0.020.020.020.010.010.03
21. assertion0.04---------------
22. loop invariant preservation0.020.030.020.030.220.04
23. loop invariant preservation---0.05---------0.51
inline_goal
  1. loop invariant preservation0.42---------------
24. loop invariant preservation2.000.130.16---------
25. loop invariant preservation---0.050.39---------
26. loop invariant preservation---------------0.37
27. loop invariant preservation---0.05------------
28. loop variant decrease0.01---0.040.030.15---
29. assertion0.020.030.020.120.02---
30. loop invariant preservation0.020.020.020.010.010.04
31. loop invariant preservation0.16---0.21---------
32. loop invariant preservation0.020.020.020.010.010.07
33. assertion0.020.020.020.010.010.00
34. loop invariant preservation0.020.020.020.010.000.04
35. loop invariant preservation0.000.020.020.080.03---
36. loop invariant preservation0.010.020.020.010.000.06
37. type invariant0.010.010.010.010.000.02
38. postcondition0.010.020.020.130.00---
39. postcondition0.010.020.020.070.030.03

Theory "verifythis_fm2012_LRS.SuffixSort_test": fully verified in 0.16 s

ObligationsAlt-Ergo (0.99.1)
VC for bench0.16

Theory "verifythis_fm2012_LRS.SuffixArray": fully verified in 11.24 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Coq (8.4pl6)Eprover (1.8-001)Vampire (0.6)Z3 (4.3.2)
VC for select0.010.010.03---0.010.010.03
permut_permutation---------1.12---------
VC for create---------------------
split_goal_wp
  1. array creation size0.010.010.02---0.010.010.00
2. precondition0.010.010.02---0.010.010.00
3. precondition0.010.020.03---0.040.200.03
4. type invariant0.010.050.02---------0.05
5. loop invariant init0.010.020.03---0.080.040.00
6. type invariant0.010.010.03---0.000.000.02
7. index in array bounds0.000.010.03---0.710.520.02
8. loop invariant preservation0.010.020.05---------0.03
9. type invariant0.020.010.04---0.000.000.02
10. precondition0.010.050.02---0.010.010.00
11. precondition0.010.020.04------0.240.03
12. type invariant0.080.100.06------3.51---
VC for lcp---------------------
split_goal_wp
  1. index in array bounds0.010.030.03---------0.03
2. index in array bounds0.010.010.03---------0.03
3. precondition0.010.050.02------3.000.06
4. precondition0.020.040.02---------0.06
5. postcondition0.03---0.02------------

Theory "verifythis_fm2012_LRS.SuffixArray_test": fully verified in 0.02 s

ObligationsAlt-Ergo (0.99.1)
VC for bench0.02

Theory "verifythis_fm2012_LRS.LRS": fully verified in 25.79 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Coq (8.4pl6)Eprover (1.8-001)Vampire (0.6)Z3 (4.3.2)
lcp_sym0.01---0.02------------
le_le_common_prefix0.10------------------
le_le_longest_common_prefix0.190.060.11---0.02------
VC for lrs---------------------
split_goal_wp
  1. assertion0.020.020.03---------0.04
2. assertion0.020.020.03---------0.05
3. postcondition0.020.020.03---0.020.010.04
4. postcondition0.020.040.03---0.010.010.08
5. postcondition0.030.030.08---------0.04
6. postcondition0.030.030.03---------0.05
7. loop invariant init0.010.030.03---0.010.010.08
8. loop invariant init0.020.020.03---0.010.010.04
9. loop invariant init0.020.020.07---------0.04
10. loop invariant init0.020.030.03---------0.05
11. precondition0.010.020.04---0.492.930.04
12. precondition0.020.020.03---0.090.010.04
13. precondition0.020.040.06---------0.04
14. loop invariant preservation0.020.160.04---0.313.250.05
15. loop invariant preservation0.030.170.03---0.223.870.05
16. loop invariant preservation0.160.180.03------------
17. loop invariant preservation---3.69---------------
18. loop invariant preservation0.000.040.03---0.080.010.08
19. loop invariant preservation0.010.020.03---0.080.010.05
20. loop invariant preservation0.030.020.03---0.010.05---
21. loop invariant preservation---2.150.04------------
22. assertion0.030.150.05---1.10------
23. assertion---------1.61---------
24. postcondition0.010.020.03---0.100.010.05
25. postcondition0.010.040.03---0.100.000.08
26. postcondition0.020.050.03---0.010.05---
27. postcondition---------1.31---------

Theory "verifythis_fm2012_LRS.LRS_test": fully verified in 0.01 s

ObligationsAlt-Ergo (0.99.1)
VC for bench0.01