locked
C# 6.0 / Read Only Auto-Properties / Invariants RRS feed

  • Question

  • I think there are few bugs in the instrumentation / static analysier related to C# 6.0 and read only auto properties:
    Is there any plans to add the new syntax?

    Here is an example:

    public WebHeaderCollection Header { get;  } = new WebHeaderCollection();

    It seems unable to detect that this is a read only auto property and would have a provable invariant of 

    Contract.Invariant(this.Header != null);

    There is an obvious work around: don't use the new syntax

    public ClassCtor() 
    {	
        this.Header = new WebHeaderCollection();
    }
    
    public WebHeaderCollection Header { get; private set; } 

    Tuesday, September 29, 2015 12:37 PM

All replies

  • To elaborate on this a little bit, even if you put the invariant in a contract invariant method the static analyzer complains.  At the moment, it appears that there is no way to make Code Contracts work with the new readonly auto properties.  I'm guessing the generated bytecode for them doesn't match the old style generated bytecode and so the static analyzer doesn't notice it is an auto-property.
    • Proposed as answer by Micah Zoltu Sunday, November 22, 2015 7:18 PM
    • Unproposed as answer by Micah Zoltu Sunday, November 22, 2015 7:18 PM
    Sunday, November 22, 2015 7:17 PM
  • It appears this is being tracked over on GitHub: https://github.com/Microsoft/CodeContracts/issues/303
    • Proposed as answer by Micah Zoltu Sunday, November 22, 2015 7:19 PM
    Sunday, November 22, 2015 7:19 PM