none
Static Checker Warns About Unproven Invariant Proved by Precondition

    Question

  • I have the following class:

    public class CustomEventArgs<T> : EventArgs {
        public T Item { get; }
    
        [ContractInvariantMethod]
        private void ObjectInvariant() {
            // Item is non-null
            Contract.Invariant(Item != null);
        }
    
        public CustomEventArgs(T item) {
            // Argument must be non-null
            Contract.Requires(item != null);
    
            Item = item;
        }
    }

    When running the static checker I get the following warning:

    warning : CodeContracts: invariant unproven: Item != null

    Wouldn't the precondition be enough to prove this? The property is read-only and is only ever assigned in the constructor.

    • Edited by Mikkel Lund Monday, January 11, 2016 8:11 AM
    Thursday, January 07, 2016 9:56 PM

All replies

  • I'm too lazy to find the reference, but read-only auto-properties have this problem. Add a private setter and the problem goes away.
    Monday, January 11, 2016 2:27 AM
  • That works. It's a shame that it can't handle read-only auto-properties out of the box :(
    Monday, January 11, 2016 8:09 AM