Softcontract: Model-based design of error-checking code and property monitors