Đây có phải là lỗi trong trình kiểm tra hợp đồng tĩnh không?

Question

Nếu tôi viết những dòng này:

public sealed class Foo 
{ 
    private int count; 
    private object owner; 
    private void Bar() 
    { 
     Contract.Requires(count > 0); 
     Contract.Ensures(owner == null || count > 0); 

     if (count == 1) 
      owner = null; 
     --count; 
    } 
} 

Trình kiểm tra hợp đồng tĩnh có thể chứng minh tất cả khẳng định.

Nhưng nếu tôi viết những dòng này thay vì:

public sealed class Foo 
{ 
    private int count; 
    private object owner; 
    private void Bar() 
    { 
     Contract.Requires(count > 0); 
     Contract.Ensures(owner == null || count > 0); 

     --count; 
     if (count == 0) 
      owner = null; 
    } 
} 

Nó tuyên bố các hậu owner == null || count > 0 là chưa được chứng minh.

Tôi nghĩ rằng tôi có thể chứng minh hình thức thứ hai không vi phạm hậu điều này:

// { count > 0 } it's required 
--count; 
// { count == 0 || count > 0 } if it was 1, it's now zero, otherwise it's still greater than zero 
if (count == 0) 
{ 
    // { count == 0 } the if condition is true 
    owner = null; 
    // { count == 0 && owner == null } assignment works 
} 
// { count == 0 && owner == null || count != 0 && count > 0 } either the if was entered or not 
// { owner == null || count > 0 } we can assume a weaker postcondition 

là một cái gì đó sai với bằng chứng của tôi không?

tôi thêm khẳng định trong bằng chứng của tôi như Contract.Assert cuộc gọi đến các mã, và tôi đi đến kết luận rằng nếu tôi thêm chỉ thế này, nó quản lý để chứng minh hậu:

--count; 
Contract.Assert(count == 0 || count > 0) 
if (count == 0) 
    owner = null; 

Nhưng, nếu tôi bây giờ thay đổi cùng một xác nhận đó thành một cách "tự nhiên hơn", nó không thành công:

--count; 
Contract.Assert(count >= 0) 
if (count == 0) 
    owner = null; 

Nó sẽ được kỳ vọng rằng hai xác nhận tương đương, nhưng trình kiểm tra tĩnh xử lý chúng khác nhau.

(Tôi đang sử dụng phiên bản beta 2 của VS10 bằng cách này)

Answer 1

Tôi sẽ không mong đợi điều prover rất phức tạp này sẽ ở trạng thái hoạt động đầy đủ vì nó chỉ là một bản beta sau khi tất cả. Tôi nghĩ rằng đó là một lỗi hoặc ít nhất là một điểm đáng để nâng cao với các nhà phát triển, bởi vì đây là một điều rất đơn giản để kiểm tra tĩnh tự động.

Dù sao, do ngoại hình của sự vật, dấu đảm bảo chỉ ở đó để nói liệu trình kiểm tra hợp đồng tĩnh có thể đảm bảo điều kiện hay không. Điều này không ngụ ý rằng điều kiện không hợp lệ, nó chỉ có nghĩa là nó không thể tìm thấy bằng chứng.

Tôi sẽ lo lắng hơn nhiều về các trường hợp nó nói điều gì đó được đảm bảo không hợp lệ. Điều đó sẽ được tính là lỗi!

Answer 2

Caveat: Tôi biết hoàn toàn không có gì về chi tiết cụ thể của hệ thống hợp đồng .net.

Tuy nhiên, tôi có thể cho bạn biết điều này: theo nghĩa đen là không thể (xem tạm dừng vấn đề) để tạo một trình hoàn chỉnh cho các xác nhận phong phú như hệ thống hỗ trợ.

Vì vậy: đây có phải là lỗi không? Số

Mặt khác, có vẻ hợp lý khi cho rằng đây có thể là trường hợp phổ biến mà người triển khai của người biện hộ có thể muốn thêm vào hệ thống của họ.