hợp đồng Mã, nếu X <Y và Y = Z + 1 tại sao X <Z + 1 không chứng minh

Question

Tôi có một hợp đồng mà thực hiện điều này:

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

Hai đường chuyền phân tích tốt đầu tiên nhưng ba nói rằng khẳng định là chưa được chứng minh, tắt bởi một? xem xét bảo vệ. Nó có vẻ như toán học đơn giản. có cái gì tôi đang mất tích?

thử với các chuỗi chuỗi và các giá trị cục bộ có vẻ hoạt động tốt. Có thể làm với cuộc gọi .Length bằng cách nào đó? Tôi đã cố gắng trao đổi các int để UInt16 để xem nếu nó là do tràn bộ đệm trong một vòng lặp nhưng đó không phải là một trong hai.

Answer 1

Hmm, điều duy nhất tôi có thể nghĩ là máy phân tích tĩnh đang gặp sự cố với các xác nhận này. Theo tôi về điều này:

1. Bạn gọi Contract.Assert(i < delegateParameterTypes.Length);. Giả sử điều này là đúng, chúng tôi tiếp tục.
2. Tại thời điểm này, trình phân tích tĩnh không biết liệu có bất kỳ điều gì đã thay đổi khoảng delegateParameterTypes.Length giữa cuộc gọi sắp xảy ra với Contract.Assert(predicate) và bước 1 ở trên không. Bạn và tôi biết không có gì xảy ra, nhưng các phân tích không - mặc dù thực tế hai dòng mã là liền kề (ai nói rằng không có một số tiểu bang cảm ứng chia sẻ nhà nước ra có một nơi nào đó?)
3. Bạn thực hiện cuộc gọi tiếp theo: Contract.Assert(delegateParameterTypes.Length == methodParameters.Length + (1)); Máy phân tích kiểm tra điều này, và điều này cũng OK.
4. Tại thời điểm này, trình phân tích không biết liệu có bất kỳ điều gì thay đổi về delegateParameterTypes hoặc methodParameters --QED, Assert chưa được chứng minh cho Contract.Assert(i < methodParameters.Length + (1)); trên dòng tiếp theo.

Một lần nữa, có thể có một số trạng thái chung chung được liên kết với những thứ đó và trạng thái đó có thể đã thay đổi giữa hai cuộc gọi thành Contract.Assert. Hãy nhớ rằng, với bạn và tôi, mã có vẻ tuyến tính và đồng bộ. Thực tế là hoặc có thể là khá khác nhau, và các phân tích tĩnh có thể làm cho không có giả định về trạng thái của những đối tượng giữa các cuộc gọi liên tiếp đến Contract.Assert.

gì có thể làm việc, tuy nhiên:

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); 
} 

Bằng cách chỉ định độ dài cho các biến, phân tích tĩnh bây giờ có thể biết rằng những giá trị không thay đổi trong for vòng lặp, hoặc bên ngoài của phương pháp này, trong đó họ được chỉ định. Bây giờ bạn đang so sánh i với các giá trị được biết là không thay đổi. Bây giờ, máy phân tích tĩnh có thể đưa ra một số suy luận về việc so sánh các giá trị này và có thể chứng minh được các xác nhận.