Left-pad verified with Why3

left-pad.mlw

module LeftPad
	use import int.Int
	use import int.MinMax
	use import string.Char as C
	use import map.Map as M
	use import string.String as S
	use import string.Buffer as B

 (* string.Buffer.contents only does the length for some reason *)
	val buf2str (b: B.t) : string
		ensures { S.length result = length b }
		ensures { forall i: int. 0 <= i < length b -> M.get b.contents i = result[i] }

	let leftpad (s: string) (c: char) (maxlen: int) : string
	ensures { S.length result = max (old (S.length s)) maxlen }
	ensures { old (S.length s) >= maxlen -> result = (old s) }
	ensures { old (S.length s) < maxlen ->
		let padlen = maxlen - old (S.length s) in
		(forall i: int. 0 <= i < padlen -> result[i] = c)
		/\ (forall i: int. padlen <= i < maxlen -> result[i] = (old s)[i - padlen])
	}
	= if S.length s >= maxlen then s else
		let buf = B.create 0 in
		for i = 0 to maxlen - S.length s - 1 do
			invariant { buf.length = i }
			invariant { forall j: int. 0 <= j < i -> M.get buf.contents j = c }
			add_char buf c
		done;
		add_string buf s;
		buf2str buf
end