## Equality up to spaces

Check that two strings are equal up to space characters.

**Auteurs:** Jean-Christophe Filliâtre

**Catégories:** Strings

**Outils:** 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

download ZIP archive

# Why3 Proof Results for Project "equality_up_to_spaces"

## Theory "equality_up_to_spaces.Top": fully verified

Obligations | Alt-Ergo 2.3.3 | CVC5 1.0.5 | Z3 4.11.2 | |

VC for remove_spaces | 0.01 | 0.09 | 0.02 | |

VC for compare_up_to_spaces | --- | --- | --- | |

split_vc | ||||

loop invariant init | 0.00 | 0.07 | 0.01 | |

loop invariant init | 0.00 | 0.08 | 0.02 | |

loop invariant init | 0.03 | 1.02 | 0.35 | |

assertion | 0.65 | --- | 0.75 | |

loop variant decrease | 0.01 | 0.07 | 0.02 | |

loop invariant preservation | 0.01 | 0.07 | 0.02 | |

loop invariant preservation | 0.01 | 0.06 | 0.01 | |

loop invariant preservation | 0.01 | 0.07 | --- | |

assertion | 0.65 | --- | 0.93 | |

loop variant decrease | 0.01 | 0.07 | 0.02 | |

loop invariant preservation | 0.01 | 0.05 | 0.01 | |

loop invariant preservation | 0.01 | 0.06 | 0.02 | |

loop invariant preservation | 0.01 | 0.06 | --- | |

assertion | --- | --- | 1.38 | |

assertion | --- | --- | 1.31 | |

postcondition | 0.01 | 0.34 | Timeout (5.00s) | |

postcondition | 0.04 | 0.10 | --- | |

loop variant decrease | 0.01 | 0.07 | 0.02 | |

loop invariant preservation | 0.01 | 0.08 | 0.02 | |

loop invariant preservation | 0.01 | 0.07 | 0.02 | |

loop invariant preservation | 0.02 | 0.09 | --- | |

postcondition | 0.01 | 0.26 | 0.02 |