Static Checker Warns About Unproven Invariant Proved by Precondition RRS feed

  • Question

  • I have the following class:

    public class CustomEventArgs<T> : EventArgs {
        public T Item { get; }
        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 7, 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