Code Contracts and failure on private static readonly fields

Question

I have a private static readonly field in my class:

public class MyClass
{
    // ISSUE #1 -- requires unproven: path != null
    private static readonly DirectoryInfo MyDirectory =
        new DirectoryInfo(Settings.Default.MyDirectoryPath);

    protected virtual void SomeMethod()
    {
        if (MyDirectory.Exists)
        {
            // ISSUE #2 -- requires unproven: !string.IsNullOrEmpty(path)
            var catalog = new DirectoryCatalog(MyDirectory.FullName);
        }
    }
}

For issue #1 I used a null coalescing operator to default to some magic string and that fixed it, but I don't really like that solution. I was hoping there was a better solution.

For issue #2 the only thing I can think of is using a Contract.Assumes because if I attempt to use Contract.Requires(MyDirectory.Exists || !String.IsNullOrEmpty(MyDirectory.FullName)); it complains about visibility (private field used in a requires on a protected method).

Answer 1

Issue #1 is a result of Settings.Default.MyDirectoryPath being code generated by Visual Studio without any contracts on the property. This issue is not limited to null strings. Many API's now have contracts that require say a TimeSpan to be non-negative but using a setting directly in the API will generate a Code Contracts warning.

A way to solve this issue is to wrap the setting in a method that has a contract. E.g.:

String GetMyDirectoryPath() {
  Contract.Ensures(Contract.Result<String>() != null);
  var myDirectoryPath = Settings.Default.MyDirectoryPath;
  Contract.Assume(myDirectoryPath != null);
  return myDirectoryPath;
}

Notice how the Contract.Assume really performs validation of your setting (which can't be verified by Code Contracts because it is controlled by an external configuration file). Had it been a TimeSpan that is expected to be non-negative you can either use Contract.Assume to do the validation resulting in a ContractException or some other method using your own exception instead.

Adding this extra layer is somewhat tedious but because the setting is defined outside the application it needs to be run-time validated at some point just as you have to validate interactive user input.

Issue #2 is probably because DirectoryInfo doesn't have any contracts defined. The easist way is to use Contract.Assume. This will make a statement about what you believe is the expected behavior of DirectoryInfo but a run-time check will still be in place to ensure that your belief is correct (provided that you keep the checks in your code).

var path = MyDirectory.FullName;
Contract.Assume(!string.IsNullOrEmpty(path));
var catalog = new DirectoryCatalog(path);

Answer 2

After having used Code Contracts in a current project for a while now I have found that it does force you to rewrite your code at times to correct for issues. You really have two options here.

1. You can add the setting to your project settings to output what the correct attributes to apply are to ignore certain warnings. This is done by adding the "-outputwarnmasks" flag to the "Extra Static Checker Options" under the Advanced section in the Code Contracts tab of the Project file settings. This will add information to the Build Output window giving you the correct attributes to add to ignore the individual cases. (very useful when dealing with Entity Framework).
2. You can rewrite your code to add the proper Requires and Ensures to your code so that the warnings don't appear.

If you want to rewrite the code: To solve Issue #1 you would have to wrap the Settings class and expose a new MyDirectoryPath as a property that isn't code generated so that you can add a check in it and return an empty string and add the Contract.Ensures(Contract.Result<string>() != null) at the top of the Getter for the property.

To solve Issue #2 you would have to wrap you access to the class field inside a private static property that adds the proper Ensures and Requires.

I have usually gone with rewriting the code wherever possible except with Entity Framework/LINQ where you need to add the attributes, especially with complex queries.

** Disclaimer ** These are just the ways I have found to solve the issues as there isn't a great deal of information on other ways of working around these types of items.

Answer 3

Well, for Issue#2, I think you might want to use && not ||. But beyond that, perhaps for Issue#1 you can put those checks in the static constructor? Another option for Issue#2 is to have the method to take the directory as a parameter:

private static readonly DirectoryInfo MyDirectory;

static MyClass()
{
    Contract.Requires(Settings.Default.MyDirectoryPath != null);
    MyDirectory = new DirectoryInfo(Settings.Default.MyDirectoryPath);
}

protected void SomeMethod()
{
    SomeOtherMethod(MyDirectory);
}

protected virtual void SomeOtherMethod(DirectoryInfo directory)
{
    Contract.Requires(directory.Exists && !String.IsNullOrEmpty(directory.FullName));

    var catalog = new DirectoryCatalog(directory.FullName);
}

I don't have much experience working with the Contract API, so I might be off my rocker with all this. :)

Answer 4

Contract.Requires(MyDirectory.Exists || !String.IsNullOrEmpty(MyDirectory.FullName));

Don't do this! MyDirectory.Exists can change at any time and the caller cannot guarantee it. Just throw an exception if the directory doesn't exist - this is what exceptions are for.