add pre/post conditions and pseudo code