"Bất biến không được chứng minh" khi sử dụng phương pháp tạo đối tượng mới cụ thể trong câu lệnh return

Question

Mã đơn giản sau đây sẽ mang lại cảnh báo "không được chứng minh" chưa được kiểm tra bởi Bộ kiểm tra tĩnh của Hợp đồng mã, mặc dù không có cách nào _foo có thể là null. Cảnh báo là cho tuyên bố return bên trong UncalledMethod.

public class Node 
{ 
    public Node(string s1, string s2, string s3, string s4, object o, 
       string s5) 
    { 
    } 
} 

public class Bar 
{ 
    private readonly string _foo; 

    public Bar() 
    { 
     _foo = "foo"; 
    } 

    private object UncalledMethod() 
    { 
     return new Node(string.Empty, string.Empty, string.Empty, string.Empty, 
         GetNode(), string.Empty); 
    } 

    private Node GetNode() 
    { 
     return null; 
    } 

    public string Foo 
    { 
     get 
     { 
      Contract.Ensures(Contract.Result<string>() != null); 
      return _foo; 
     } 
    } 

    [ContractInvariantMethod] 
    private void Invariants() 
    { 
     Contract.Invariant(_foo != null); 
    } 
} 

Ngoài thực tế, cảnh báo đơn giản là không hợp lệ, nó chỉ xảy ra trong một số trường hợp cụ thể. Thay đổi bất kỳ những điều sau đây sẽ làm cho các cảnh báo đi:

1. Inline GetNode nên câu lệnh return trông như thế này:

   return new Node(string.Empty, string.Empty, string.Empty, string.Empty, null, 
          string.Empty); 
   

2. Hủy bỏ bất kỳ tham số s1 đến s5 từ các nhà xây dựng của Node.
3. Thay đổi loại của bất kỳ tham số nào s1 thành s5 từ hàm tạo của Node thành object.

4. Sử dụng một biến tạm thời cho kết quả của GetNode:

   var node = GetNode(); 
       return new Node(string.Empty, string.Empty, string.Empty, string.Empty, 
           node, string.Empty); 
   

5. Thay đổi thứ tự của các tham số của các nhà xây dựng của Node.
6. Kiểm tra tùy chọn "Hiển thị các giả định" trong ngăn cài đặt hợp đồng mã trong cài đặt dự án.

Tôi có thiếu thứ gì đó rõ ràng ở đây hay chỉ đơn giản là lỗi trong trình kiểm tra tĩnh?

---

thiết lập của tôi:

đầu ra của tôi:

C:\{path}\Program.cs(20,9): message : CodeContracts: Suggested ensures: Contract.Ensures(this._foo != null); 
C:\{path}\Program.cs(41,17): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<System.String>() == this._foo); 
C:\{path}\Program.cs(33,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<ConsoleApplication3.Program+Node>() == null); 
C:\{path}\Program.cs(27,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<System.Object>() != null); 
C:\{path}\Program.cs(55,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.ForAll(0, args.Length, __k__ => args[__k__] != 0)); 
CodeContracts: ConsoleApplication3: Validated: 92,3% 
CodeContracts: ConsoleApplication3: Contract density: 1,81 
CodeContracts: ConsoleApplication3: Total methods analyzed 8 
CodeContracts: ConsoleApplication3: Methods with 0 warnings 7 
CodeContracts: ConsoleApplication3: Total method analysis read from the cache 8 
CodeContracts: ConsoleApplication3: Total time 2,522sec. 315ms/method 
CodeContracts: ConsoleApplication3: Retained 0 preconditions after filtering 
CodeContracts: ConsoleApplication3: Inferred 0 object invariants 
CodeContracts: ConsoleApplication3: Retained 0 object invariants after filtering 
CodeContracts: ConsoleApplication3: Detected 0 code fixes 
CodeContracts: ConsoleApplication3: Proof obligations with a code fix: 0 
C:\{path}\Program.cs(27,13): warning : CodeContracts: invariant unproven: _foo != null 
C:\{path}\Program.cs(49,13): warning : + location related to previous warning 
C:\windows\system32\ConsoleApplication3.exe(1,1): message : CodeContracts: Checked 13 assertions: 12 correct 1 unknown 
CodeContracts: ConsoleApplication3: 
CodeContracts: ConsoleApplication3: Background contract analysis done. 

Answer 1

này không còn là một vấn đề với the latest version.