locked
Code Contracts: Deep Invariant for immutability and initialization

    Question

  • Hi,

    First of all, thanks so much for including DbC into the Framework.  This should have a profound effect on all .NET code moving forward.

    I was thinking about some of the ways that I might try to use Code Contracts and I thought about null (Nothing in VB :) checking and how nulls affect code at runtime (remembering back to a recent video of Anders Hejlsberg mentioning that it might have been a mistake for C# to support nulls in the first place given how prevalent it is to get NullReferenceException in real-world apps).  I also thought about how immutability is becoming increasingly important in class designs for the future of parallelism, and the relationship to nulls being that having an immutable class with a bunch of null references isn't typically useful at runtime.

    So it might be nice, if even possible, to support a type of contract that says "enforce immutability and don't allow nulls in any fields or arguments, ever!".  I envision something like this:

    [ImmutableContract(RequiresInitialization = true)]

    public class Stubborn

    {

      public string Value

      {

        get { return str3; }

      }

     

      public int Number

      {

        get { return number; }

        set { /*any impl*/ }    // compile-time error (arguable)

      }

     

      private readonly int number;

      private readonly string str1 = "hello";

      private readonly string str2;

      private string str3;  // compile-time warning (not marked as readonly)

      private string str4;  // compile-time warning (not marked as readonly)

     

      public Stubborn()

      {

        str3 = "hello";

        str1 = null;    // compile-time error (no nulls allowed)

        str2 = Util.GetValue();

        // compile-time error (str2 is not checked for null after assignment)

     

        // compile-time error (str4 is never assigned)

      }

     

      public Stubborn(string str4)

      {

        // compile-time error (str4 argument is never checked for null)

     

        this.str4 = str4;
        str2 = "must initialize";

        str3 = "must initialize";

      }

     

      public void CallMe()

      {

        str4 = "internal value";

        str3 = "public value"// compile-time error (violates immutablilty)

      }

    }

    The idea behind the compile-time error on the Number property's set accessor is that in an immutable type it doesn't make sense to have a writeable property.  Yes, since it's techincally just a method call it could do something other than change mutable data, however, in that case it would probably make more sense as a public method than as a public property anyway.  There should at least be a compile-time warning if set accessors are used.

    - Dave


    http://davesexton.com/blog
    Tuesday, December 02, 2008 11:51 AM

Answers

  • As Manuel pointed out, one can bake non-nullness (and immutability) into the type system itself. This is the path that Spec# (http://research.microsoft.com/specsharp) took. The difficulty is that, as Dave pointed out, non-nullness (and immutability) are object invariants. As Spec# showed, it is very difficult to enforce object invariants in a sound manner. I.e., the type system is sound --- there is no way to observe a variable of type T in a state where it contains anything other than a valid value of type T. To do the same thing for non-nullness requires support from the CLR itself. Code contracts are not intended to be sound and we don't have the necessary support from the runtime. But it would be a great direction to work towards!
    Tuesday, December 16, 2008 9:56 PM

All replies

  • Hi Dave,

    Immutable classes are an interesting concept, not only for verification of sequential code, but also for optimizations in concurrent code.

    At the moment, I don't yet see how the concept is best supported with contracts. It does feel more like a typing property to me than something we want to express with assertions.

    Do you expect this to be enforced only at compile time, or also at runtime?

    Regards,

    -MaF
    Wednesday, December 10, 2008 5:07 PM
  • Hi MaF,

    Thanks for the reply.

    I'd expect this to be enforced at compile-time and also with the option of being enforced at runtime in sort of an AOP manner (intercepting method calls and checking all known state that is used in any way to produce/change public data - like str3 in the CallMe method in my example above).  In my opinion, it's like one global invariant for the class, in more ways than one - also keep in mind the other importance of this particular contract, which is the global null-checking aspect.  This way null checks don't have to be specified explicitly for all fields and all arguments of all methods.  I can see myself being annoyed having to constantly litter my code with contracts for non-null arguments and return values using "Requires" and "Enforces".  As a matter of fact, I already am annoyed even without using contracts yet ;)
     
    I can certainly see why you might want to separate the two behaviors into different contracts: [ImmutableContractAttribute, NoNullsAllowedContractAttribute] :)

    The importance of constraining a class as immutable, aside from the obvious, is that it should help tremendously in testing code such as what Pex generates.  The difference between knowing whether a class is contractually immutable vs. not knowing if immutable is an intention of the author at all could, theoretically, lead to very different results from Pex; e.g., why even bother to test a property for change any time a method is executed if the class is mutable?  - because in that case change is allowed.  But if a class is known to be immutable, that begs for an implicit invariant check on all public properties after any code is executed.  It may also allow for Pex to generate multi-threaded tests since an immutable contract is also a thread-safe contract.

    - Dave
    http://davesexton.com/blog
    Wednesday, December 10, 2008 5:59 PM
  • Hi MaF,

    > It may also allow for Pex to generate multi-threaded tests since an immutable contract is also a thread-safe contract.

    I guess that could mean two different things, both applicable to Pex.

    The first meaning is that Pex could generate code to test the thread-safety of classes that have ImmutableContractAttribute.

    The second meaning is that Pex could generate multi-threaded code to test any other testable aspects of the class that are known not to read or write shared state (is it possible to analyze code and discover what state may be "shared"?  I guess only in "static-typed" mode :).

    The second meaning has the potential to increase the performance of testing on a class and even on a library level as more and more classes are designed to be immutable.  Given that Pex sounds like it's going to be the complete testing package in the future, performance should be a primary concern.

    - Dave


    http://davesexton.com/blog
    Wednesday, December 10, 2008 6:07 PM
  • As Manuel pointed out, one can bake non-nullness (and immutability) into the type system itself. This is the path that Spec# (http://research.microsoft.com/specsharp) took. The difficulty is that, as Dave pointed out, non-nullness (and immutability) are object invariants. As Spec# showed, it is very difficult to enforce object invariants in a sound manner. I.e., the type system is sound --- there is no way to observe a variable of type T in a state where it contains anything other than a valid value of type T. To do the same thing for non-nullness requires support from the CLR itself. Code contracts are not intended to be sound and we don't have the necessary support from the runtime. But it would be a great direction to work towards!
    Tuesday, December 16, 2008 9:56 PM
  • Some tools, such as ReSharper, can take care of most (if not all) of the static immutable issues discussed. I think it would be even better to have something that easily supported the concept of dynamic immutable instances -- in other words, after setting an object to a specific set of values, it is flagged as immutable/readonly from that point forward (with the obvous exception of Dispose/destructor).

    Along the same lines, automatic detection of attempts to access a disposed object would be great.

    Yes we can decorate every method/property accessor with checks gainst boolean flags, but that code clutter is not very impressive. Also different developers/projects would impose different naming etc., which would just add confusion. I think it would be better to have a language mechanism for this, even if it involves a rewriter.
    Sunday, December 21, 2008 6:00 PM