done modifying requires clause with constraints/initialization ensures from parameter variables
added variables into the assertion as verification statements as well as free variables