## Wrap lines

This micro challenge was proposed by Mattias Ulbrich (KIT) during his KeY tutorial at VerifyThis 2021.

**Authors:** Andrei Paskevich

**Tools:** Why3

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

This micro challenge was proposed by Mattias Ulbrich (KIT) during his KeY tutorial at VerifyThis 2021.

module WrapLines use int.Int use array.Array type char val constant space: char val constant newline: char val (=) (x y: char) : bool ensures { result <-> x = y } (* Returns the index in s that has value c and is at least from, if it exists, and -1 otherwise. *) let index_of (s: array char) (c: char) (from: int) : int requires { 0 <= from <= length s } ensures { result = -1 /\ (forall i. from <= i < length s -> s[i] <> c) \/ from <= result < length s /\ s[result] = c /\ (forall i. from <= i < result -> s[i] <> c) } = let ref k = from in while k < length s do invariant { from <= k <= length s } invariant { forall i. from <= i < k -> s[i] <> c } variant { length s - k } if s[k] = c then return k; k <- k + 1 done; return -1 (* Every line (but the last) has at least line_length characters: *) predicate at_least_line_length (s: array char) (line_length: int) = forall i j. -1 <= i < j < length s -> (i = -1 \/ i <= 0 /\ s[i] = newline) -> s[j] = newline -> j - i >= line_length let wrap_lines (s: array char) (line_length: int) : unit (* initially, no newline at all *) requires { forall i. 0 <= i < length s -> s[i] <> newline } (* the only changes in s are turning ' ' into '\n' *) ensures { forall i. 0 <= i < length s -> s[i] <> old s[i] -> old s[i] = space /\ s[i] = newline } ensures { at_least_line_length s line_length } = let ref last_nl = -1 in let ref last_sp = index_of s space 0 in while last_sp <> -1 do invariant { -1 <= last_nl < length s } invariant { last_sp = -1 \/ last_nl < last_sp < length s /\ s[last_sp] = space } invariant { forall i. last_nl < i < length s -> s[i] = old s[i] } invariant { forall i. 0 <= i < length s -> s[i] <> old s[i] -> old s[i] = space /\ s[i] = newline } invariant { forall i. last_nl < i < last_sp -> s[i] <> newline } invariant { at_least_line_length s line_length } variant { if last_sp = -1 then 0 else length s - last_sp } if last_sp - last_nl > line_length then ( s[last_sp] <- newline; last_nl <- last_sp ); last_sp <- index_of s space (last_sp + 1) done (* Implement a wrap_lines method such that * The original file may already contain '\n' * Every line has at most L characters or does not have a space * If there is an introduced newline character there is no space or newline that could have given a longer line. *) let wrap_lines_plus (s: array char) (line_length : int) : unit requires { line_length >= 0 } (* we only convert spaces into newlines *) ensures { forall i. 0 <= i < length s -> s[i] <> old s[i] -> old s[i] = space /\ s[i] = newline } (* no line segment longer than line_length characters has a space *) ensures { forall i. 0 <= i < length s - line_length -> (forall j. i <= j <= i + line_length -> s[j] <> newline) -> (forall j. i <= j <= i + line_length -> s[j] <> space) } (* no line is broken by an introduced newline if there is a further breakpoint (newline, space or EOF) within (line_length + 1) characters in the original file *) ensures { forall i. -1 <= i < length s -> (0 <= i -> s[i] = newline) -> forall j. i < j <= length s -> j <= i + line_length + 1 -> (j < length s -> old s[j] = space \/ old s[j] = newline) -> forall k. i < k < j -> s[k] = old s[k] } = let ref last_nl = -1 in (* last seen newline or -1 *) let ref last_sp = -1 in (* last seen space, newline or -1 *) (* scan the file and at each breakpoint, decide whether we should have broken the line at the last space character *) for ind = 0 to length s - 1 do invariant { -1 <= last_nl <= last_sp < ind } invariant { 0 <= last_nl -> s[last_nl] = newline } invariant { last_nl < last_sp -> s[last_sp] = space } invariant { forall i. last_nl < i < ind -> s[i] <> newline } invariant { forall i. last_sp < i < ind -> s[i] <> space } invariant { forall i. 0 <= i < ind -> s[i] <> old s[i] -> old s[i] = space /\ s[i] = newline } invariant { forall i. ind <= i < length s -> s[i] = old s[i] } invariant { forall i. 0 <= i < last_sp - line_length -> (forall j. i <= j <= i + line_length -> s[j] <> newline) -> (forall j. i <= j <= i + line_length -> s[j] <> space) } invariant { forall i. -1 <= i < length s -> (0 <= i -> s[i] = newline) -> forall j. i < j <= length s -> j <= i + line_length + 1 -> (j < length s -> old s[j] = space \/ old s[j] = newline) -> forall k. i < k < j -> s[k] = old s[k] } if s[ind] = newline then begin if last_nl < last_sp && last_nl + line_length + 1 < ind then begin s[last_sp] <- newline; end; last_nl <- ind; last_sp <- ind; end else if s[ind] = space then begin if last_nl < last_sp && last_nl + line_length + 1 < ind then begin s[last_sp] <- newline; last_nl <- last_sp; end; last_sp <- ind; end done; if last_nl < last_sp && last_nl + line_length + 1 < length s then s[last_sp] <- newline end module WrapLinesOCaml use int.Int use string.Char use string.OCaml use array.Array let constant space: char = chr 32 let constant newline: char = chr 10 clone export WrapLines with type char = char, val space = space, val newline = newline, val (=) = eq_char end

download ZIP archive

# Why3 Proof Results for Project "wrap_lines"

## Theory "wrap_lines.WrapLines": fully verified

Obligations | Alt-Ergo 2.3.3 | CVC4 1.7 | ||

VC for index_of | --- | --- | ||

split_vc | ||||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

index in array bounds | 0.00 | --- | ||

postcondition | 0.00 | --- | ||

loop variant decrease | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

postcondition | 0.00 | --- | ||

VC for wrap_lines | --- | --- | ||

split_vc | ||||

precondition | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

index in array bounds | 0.00 | --- | ||

precondition | 0.00 | --- | ||

loop variant decrease | 0.01 | --- | ||

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

loop invariant preservation | 0.00 | --- | ||

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

loop invariant preservation | 0.03 | --- | ||

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

loop invariant preservation | 0.08 | --- | ||

precondition | 0.00 | --- | ||

loop variant decrease | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

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

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

loop invariant preservation | 0.00 | --- | ||

postcondition | 0.00 | --- | ||

postcondition | 0.00 | --- | ||

VC for wrap_lines_plus | --- | --- | ||

split_vc | ||||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.00 | --- | ||

loop invariant init | 0.01 | --- | ||

index in array bounds | 0.00 | --- | ||

index in array bounds | 0.01 | --- | ||

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

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

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

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

loop invariant preservation | 0.04 | --- | ||

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

loop invariant preservation | 0.13 | --- | ||

loop invariant preservation | --- | --- | ||

remove LoopInvariant15,LoopInvariant14,LoopInvariant9,LoopInvariant7,LoopInvariant6,LoopInvariant5,LoopInvariant4,LoopInvariant3,LoopInvariant2,LoopInvariant | ||||

loop invariant preservation | 0.56 | --- | ||

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

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

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

loop invariant preservation | 0.04 | --- | ||

loop invariant preservation | 0.18 | --- | ||

index in array bounds | 0.00 | --- | ||

index in array bounds | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

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

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

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

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

loop invariant preservation | 0.04 | --- | ||

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

loop invariant preservation | 0.12 | --- | ||

loop invariant preservation | --- | 0.10 | ||

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

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

loop invariant preservation | 0.00 | --- | ||

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

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

loop invariant preservation | 0.03 | --- | ||

loop invariant preservation | 0.18 | --- | ||

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

loop invariant preservation | 0.00 | --- | ||

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

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

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

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

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

loop invariant preservation | 0.11 | --- | ||

index in array bounds | 0.00 | --- | ||

postcondition | 0.02 | --- | ||

postcondition | 0.11 | --- | ||

postcondition | 0.58 | --- | ||

postcondition | 0.00 | --- | ||

postcondition | 0.02 | --- | ||

postcondition | 0.10 | --- | ||

out of loop bounds | 0.00 | --- |

## Theory "wrap_lines.WrapLinesOCaml": fully verified

Obligations | Alt-Ergo 2.3.3 | |

VC for space | --- | |

split_vc | ||

precondition | 0.01 | |

VC for newline | --- | |

split_vc | ||

precondition | 0.01 | |

VC for infix ='refn | --- | |

split_vc | ||

postcondition | 0.01 |