## Equality up to spaces

Check that two strings are equal up to space characters.

Authors: Jean-Christophe Filliâtre

Topics: Strings

Tools: Why3

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

Check that two strings are equal up to space characters.

This problem was suggested by Rustan Leino (Amazon Web Services). The trick is in finding a loop invariant that makes the proof easy.

Author: Jean-Christophe FilliĆ¢tre (CNRS)

```use int.Int
use seq.Seq
use seq.FreeMonoid

type char
val constant space: char
val function eq (x y: char): bool ensures { result <-> x = y }
type char_string = seq char

```

The specification uses a function `remove_spaces`. It is recursively defined over a string, from left to right.

```let rec function remove_spaces (s: char_string) : char_string
variant { length s }
=      if length s = 0  then s
else if eq s[0] space then remove_spaces s[1..]
else cons s[0] (remove_spaces s[1..])

```

Code and proof.

It would be natural to have a loop invariant such as

remove_spaces x[..i] = remove_spaces y[..j]

Unfortunately, since `remove_spaces` is defined recursively from left to right, we would have hard time proving such an invariant. So instead we use an invariant which refers to the *suffixes* of `x` and `y`.

```let rec compare_up_to_spaces (x y: char_string) : bool
ensures { result <-> remove_spaces x = remove_spaces y }
= let n = length x in
let m = length y in
let ref i = 0 in
let ref j = 0 in
while i < n || j < m do
invariant { 0 <= i <= n }
invariant { 0 <= j <= m }
invariant { remove_spaces x      = remove_spaces y
<-> remove_spaces x[i..] = remove_spaces y[j..] }
variant   { n - i + m - j }
if i < n && eq x[i] space then begin
assert { remove_spaces x[i..] == remove_spaces x[i+1..] };
i <- i + 1
end else if j < m && eq y[j] space then begin
assert { remove_spaces y[j..] == remove_spaces y[j+1..] };
j <- j + 1
end else begin
assert { i < n ->
remove_spaces x[i..] == cons x[i] (remove_spaces x[i+1..]) };
assert { j < m ->
remove_spaces y[j..] == cons y[j] (remove_spaces y[j+1..]) };
if i = n || j = m then return false;
if not (eq x[i] y[j]) then return false;
i <- i + 1;
j <- j + 1
end
done;
return true
```