Temporarily disable code contracts inside a block

621 views Asked by At

Is it possible to disable run time (and compile time) checks on a class using a method call or similar? I am having trouble with my classes with invariants and using them with external libraries that construct instances dynamically. I would like to wrap those calls inside my own calls, which take a potentially partially constructed object, and returns one that is always valid.

Eg consider this code:

using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;

namespace ConsoleApp
{
    class Person
    {
        public string Name { get; set; }
        public string Email { get; set; }
        public string JobTitle { get; set; }

        public Person(string name, string email, string title)
        {
            Name = name;
            Email = email;
            JobTitle = title;
        }

        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(Name != null);
            Contract.Invariant(JobTitle != null);

        }
    }

    public static class ObjectBuilder
    {
        // Just a sample method for building an object dynamically. In my actual code, code using 
        // elastic search, NEST, serializion or entity framework has similar problems.
        public static T BuildFromDictionary<T>(Dictionary<string, object> dict)
        {
            Contract.Requires(dict != null);
            T result = (T)System.Runtime.Serialization.FormatterServices.GetUninitializedObject(typeof (T));
            foreach (var pair in dict)
            {
                string propName = pair.Key;
                var property = typeof (T).GetProperty(propName);
                property.SetValue(result, pair.Value);
            }
            return result;
        }
    }
    class Program
    {
        public static Person CreatePerson()
        {
            Dictionary<string, object> personData = new Dictionary<string, object>();
            personData["Name"] = "Fred";
            personData["Email"] = "[email protected]";
            Person person = ObjectBuilder.BuildFromDictionary<Person>(personData);
            person.JobTitle = "Programmer";
            return person;
        }
        static void Main(string[] args)
        {
            Person person1 = new Person("Bob", "[email protected]", "Hacker");

            Person person = CreatePerson();
            Console.WriteLine(person.Name);


        }
    }
}

This compiles correctly, however will throw an exception on the property.SetValue(result, pair.Value); line. This is because it will call the Name setter, and at that stage Email and JobTitle are null.

What I would like to do is to disable contracts within a code section. Eg, replacing the CreatePerson method with something like this:

    public static Person CreatePerson()
    {
        Dictionary<string, object> personData = new Dictionary<string, object>();
        personData["Name"] = "Fred";
        personData["Email"] = "[email protected]";
        Person person;
        Contract.DisableRunTimeChecks(() =>
        {
            person = ObjectBuilder.BuildFromDictionary<Person>(personData);
            person.JobTitle = "Programmer";

        });
        Contract.CheckInvariants(person);
        return person;
    }

Where Contract.DisableRunTimeChecks disables run time checks for all code within that code block (and any calls made within), and Contract.CheckInvariants runs the ContractInvariantMethod for the given object.

Is this possible to implement somehow, or is there another solution?

One solution I have seen which I don't want to do is to introduce an _initialized field on Person, and making the invariant method check if that is true before doing any checks. This is because the object should always be valid except for one or two of these constructor methods.

1

There are 1 answers

2
fourpastmidnight On

The problem is with the way the invariants are defined. I posted an answer to a similar question here. Please read the answer to the question for the details, but here's a quick couple of paragraphs from that answer that's at the root of the issue here:

From the Code Contracts manual:

Object invariants are conditions that should hold true on each instance of a class whenever that object is visible to a client. They express conditions under which the object is in a "good" state.

There's a peculiar couple of sentences in the manual at the top of page 10:

Invariants are conditionally defined on the full-contract symbol [CONTRACT_FULL]. During runtime checking, invariants are checked at the end of each public method. If an invariant mentions a public method in the same class, then the invariant check that would normally happen at the end of that public method is disabled and checked only at the end of the outermost method call to that class. This also happens if the class is re-entered because of a call to a method on another class.

— text in brackets is mine; this is the compile time symbol the manual is referencing which is defined.

Since properties are really just syntactic sugar for T get_MyPropertyName() and void set_MyPropertyName(T), these sentences would seem to apply to properties, too. Looking in the manual, when they show an example of defining object invariants, they show using private fields in the invariant contract conditions.

So here's how you'll want to define the Person class:

using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;

namespace ConsoleApp
{
    class Person
    {
        private string _name;
        private string _jobTitle;
        // For consistency, I would recommend creating a
        // private backing field for Email, too. But it's not
        // strictly necessary.

        public Person(string name, string email, string title)
        {
            // Are these pre-conditions strict enough??
            // Maybe they are, but just asking.
            Contract.Requires(name != null);
            Contract.Requires(title != null);

            _name = name;
            _jobTitle = title;
            Email = email;
        }

        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(_name != null);
            Contract.Invariant(_jobTitle != null);
        }

        public string Name
        {
            get
            {
                Contract.Ensures(Contract.Result<string>() != null);
                return _name;
            }
            set
            {
                Contract.Requires(value != null);
                _name = value;
            }
        }

        public string JobTitle
        {
            get
            {
                Contract.Ensures(Contract.Result<string>() != null);
                return _jobTitle;
            }
            set
            {
                Contract.Requires(value != null);
                _jobTitle = value;
            }
        }

        public string Email { get; set; }
    }

So to recap: Invariants only tell consumers what they can expect to be true about the object (at runtime) prior to calling any public method and upon any return from a public method. In this case, you're telling the consumer that you guarantee when they call a public method that Person.Name and Person.JobTitle will be non-null, and that when any public method returns to the caller, again, Person.Name and Person.JobTitle will be non-null. However, in order to ensure that these invariants can be maintained (and enforced), the class needs to state the pre-conditions and post-conditions when getting/setting the properties which mutate the values of the private backing fields _name and _jobTitle.