My concern with the proposed DBC for C is the lack of mechanism for expressing the relationship of input values to output values, especially if an aggregate (array or struct, either parameter or static) is being modified by the function. Obviously this would require, in the worst case, making a temporary copy of the input to use in verifying the output, as well as a notation for distinguishing separate input and output values.

Does anyone have thoughts on the tradeoffs and feasibility of automating this?