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 | Alt-Ergo 2.6.0 | CVC4 1.8 | CVC5 1.0.5 | CVC5 1.1.2 | Z3 4.11.2 | Z3 4.13.2 | |
VC for remove_spaces | 0.01 | --- | 0.04 | 0.09 | --- | 0.02 | --- | |
VC for compare_up_to_spaces | --- | --- | --- | --- | --- | --- | --- | |
split_vc | ||||||||
loop invariant init | 0.00 | 0.02 | --- | 0.07 | --- | 0.01 | --- | |
loop invariant init | 0.00 | --- | --- | 0.08 | 0.05 | 0.02 | --- | |
loop invariant init | 0.03 | 0.05 | --- | 0.47 | --- | 0.27 | --- | |
assertion | 0.65 | 0.17 | --- | --- | --- | 0.54 | --- | |
loop variant decrease | 0.01 | --- | --- | 0.07 | 0.04 | 0.02 | --- | |
loop invariant preservation | 0.01 | --- | --- | 0.07 | --- | 0.02 | 0.02 | |
loop invariant preservation | 0.01 | --- | --- | 0.06 | --- | 0.01 | 0.01 | |
loop invariant preservation | 0.01 | --- | 0.05 | 0.07 | --- | --- | --- | |
assertion | 0.65 | 0.22 | --- | --- | --- | 0.52 | --- | |
loop variant decrease | 0.01 | --- | 0.06 | 0.07 | --- | 0.02 | --- | |
loop invariant preservation | 0.01 | --- | 0.04 | 0.05 | --- | 0.01 | --- | |
loop invariant preservation | 0.01 | --- | --- | 0.06 | 0.04 | 0.02 | --- | |
loop invariant preservation | 0.01 | --- | --- | 0.06 | 0.04 | --- | --- | |
assertion | --- | --- | --- | --- | --- | 1.38 | --- | |
assertion | --- | --- | --- | --- | --- | 1.31 | --- | |
postcondition | 0.01 | 0.05 | --- | 0.34 | --- | --- | --- | |
postcondition | 0.04 | --- | --- | 0.10 | 0.06 | --- | --- | |
loop variant decrease | 0.01 | --- | 0.07 | 0.07 | --- | 0.02 | --- | |
loop invariant preservation | 0.01 | --- | --- | 0.08 | 0.04 | 0.02 | --- | |
loop invariant preservation | 0.01 | --- | 0.06 | 0.07 | --- | 0.02 | --- | |
loop invariant preservation | 0.02 | 0.03 | --- | 0.09 | --- | --- | --- | |
postcondition | 0.01 | --- | --- | 0.26 | 0.11 | 0.02 | --- |