Docstring for functions with ensures