One of the really fun experiences I've had with SPARK/Frama-C/some dependently typed languages was moving runtime tests into the contracts.
Your function only works on arrays of a certain length? Rip out the test-and-return-error code. Skip asserts (that get removed if you optimize). Put the check in the contract and the code won't compile unless the array is appropriate---which might involve a test at a higher level, where the error is easier to handle---and you get zero run-time cost.
Your function only works on arrays of a certain length? Rip out the test-and-return-error code. Skip asserts (that get removed if you optimize). Put the check in the contract and the code won't compile unless the array is appropriate---which might involve a test at a higher level, where the error is easier to handle---and you get zero run-time cost.