add requires/ensures