Code contracts if X <Y and Y = Z + 1, why X <Z + 1 is not proven

Question

I have a contract that does this:

for (int i = 0; i < delegateParameterTypes.Length; i++) { Contract.Assert(i < delegateParameterTypes.Length); Contract.Assert(delegateParameterTypes.Length == methodParameters.Length + (1)); // QED Contract.Assert(i < methodParameters.Length + (1)); } 

The first two analyzes go well, but the third says that the statement is unproven, turned off by one? consider security. This is like simple math. is there something i'm missing?

trying to use it with string arrays, and local values ​​work fine. Maybe somehow related to the .Length call? I tried replacing int with UInt16 to find out if this is due to a buffer overflow in the loop, but that is not the case either.

Answer 1

Hmm, the only thing I can think of is that the static analyzer has a problem with these statements. Follow me on this:

• You call Contract.Assert(i < delegateParameterTypes.Length); . Assuming this is so, we continue.
• At this point, the static analyzer does not know if anything about delegateParameterTypes.Length has changed between the call that should happen with Contract.Assert(predicate) and with step 1 above. You and I do not know anything, but the analyzer does not do this - despite the fact that the two lines of code are adjacent (who will say that there is some kind of stream touching some general state somewhere?)
• You make the following call: Contract.Assert(delegateParameterTypes.Length == methodParameters.Length + (1)); The analyzer checks this, and this is also normal.
• At this point, the analyzer has no idea whether anything has changed in relation to delegateParameterTypes or methodParameters - QED, Assert is not confirmed for Contract.Assert(i < methodParameters.Length + (1)); on the next line.

Again, there may be some general global state associated with these things, and that state could be changed between two calls to Contract.Assert . Remember that for you and for me, the code looks linear and synchronous. The reality may or may be completely different, and the static analyzer cannot make any assumptions about the state of these objects between successive calls to Contract.Assert .

Which may work, however:

 int delegateParameterTypesLength = delegateParameterTypes.Length; int methodParametersLength = methodParameters.Length + 1; for (int i = 0; i < delegateParameterTypesLength; i++) { Contract.Assert(delegateParameterTypesLength == methodParametersLength); // QED Contract.Assert(i < methodParametersLength); } 

By assigning lengths to variables, the static analyzer can now know that these values ​​do not change in the for loop or outside the method in which they are assigned. Now you are comparing i with values ​​that are not known to change. Now the static analyzer can draw some conclusions about comparing these values ​​and should be able to prove the statements.