Question

I start to use C# Code Contracts with enabled static and runtime checks. The problem is that some code contract checks may be duplicated from method to method and I see no good way to avoid this.

My hope is to avoid static analyzer warnings at all and don't suppress it if possible.

Lets consider the example:

There are following simple classes. This is an usual example of business logic model classes:

class Category
{
    public string Name { get; set; }
}

class Article
{
    public string Title { get; set; }
    public string Content { get; set; }
    public Category Category { get; set; }
}

For some reflection-based techniques (like model binding in MVC, database mapping) we need to provide public default constructor and public setters for model properties. So we can't guarantee that for example for Category the Contract.Invariant(!string.IsNullOrEmpty(Name)) is always true.

Then we create the next method in our internal CategoryRepository class. We assume that all validation passed earlier and accept only valid categories:

public void Add(Category category)
{
    Contract.Requires(category != null);
    Contract.Requires(!string.IsNullOrEmpty(category.Name));
    ...
}

So far so good. Then we add similar method to ArticleRepository:

public void Add(Article article)
{
    Contract.Requires(article != null);
    Contract.Requires(!string.IsNullOrEmpty(article.Title));
    Contract.Requires(!string.IsNullOrEmpty(article.Content));
    Contract.Requires(article.Category != null);
    Contract.Requires(!string.IsNullOrEmpty(article.Category.Name));
    ...
}

The problems are:

1) In every place where we expect a valid Category by contract we need to duplicate checks like:

Contract.Requires(category != null);
Contract.Requires(!string.IsNullOrEmpty(category.Name));

Sometimes we also need to make these checks in Contract.Assume methods.

2) External classes (like Article) should make checks for contracts of Category class. Looks like violation of LoW and basic encapsulation principles.

I tried next solutions:

1) Extract duplicated code to pure method in Category class like this:

[Pure]
public static bool Valid(Category category)
{
    if (category == null)
        return false;

    return !string.IsNullOrEmpty(category.Name);
}

and the use contract this way:

Contract.Requires(Category.Valid(category));

Not very good solution and also it doesn't work - the static analyzer is not satisfied.

2) Define an invariant for Category:

[ContractInvariantMethod]
void Invariant()
{
     Contract.Invariant(!string.IsNullOrEmpty(Name));
}

This solution is quite good and allow to remove unnecessary checks out of Category class, but actually this invariant is no valid (e.g. in default constructor). And static analyzer correctly detects this violation.

Am I doing something wrong and there is a more convenient way to use Code Contracts with static analyzer?

Was it helpful?

Solution

You could use the idea of popsicle immutability and do what one might call popsicle validity: in other words, although an object is not valid at all times, once all of its properties have been set then it becomes valid and stays that way.

That way, you can do the validity checking in the objects containing the data and simplify the contracts on the code that uses those objects to simply thing != null && thing.IsValid().

Here is some code to demonstrate this approach. The static checker still needs some help to prove that a is valid because its properties are set independently, but that's probably a check you would want to do on your object anyway after it is constructed by reflection.

internal class Program
{
    private static void Main()
    {
        var c = new Category();
        c.Name = "Some category";

        var categoryRepository = new CategoryRepository();
        categoryRepository.Add(c);

        var a = new Article();
        a.Category = c;
        a.Content = "Some content";
        a.Title = "Some title";

        var repository = new ArticleRepository();

        // give the static checker a helping hand
        // we don't want to proceed if a is not valid anyway
        if (!a.IsValid)
        {
            throw new InvalidOperationException("Hard to check statically");
            // alternatively, do "Contract.Assume(a.IsValid)"
        }

        repository.Add(a);

        Console.WriteLine("Done");
    }
}

public class Category
{
    private bool _isValid;
    public bool IsValid
    {
        get { return _isValid; }
    }

    private string _name;
    public string Name {
        get { return _name; }
        set
        {
            Contract.Requires(!string.IsNullOrEmpty(value));
            Contract.Ensures(IsValid);

            _name = value;
            _isValid = true;
        }
    }

    [ContractInvariantMethod]
    void Invariant()
    {
        Contract.Invariant(!_isValid || !string.IsNullOrEmpty(_name));
    }
}

public class Article
{
    private bool _isValid;
    public bool IsValid
    {
        get { return _isValid; }
    }

    private string _title;
    public string Title
    {
        get { return _title; }
        set
        {
            Contract.Requires(!string.IsNullOrEmpty(value));
            _title = value;
            CheckIsValid();
        }
    }

    private string _content;
    public string Content
    {
        get { return _content; }
        set
        {
            Contract.Requires(!string.IsNullOrEmpty(value));
            _content = value;
            CheckIsValid();
        }
    }

    private Category _category;
    public Category Category {
        get { return _category; }
        set
        {
            Contract.Requires(value != null);
            Contract.Requires(value.IsValid);
            _category = value;
            CheckIsValid();
        }
    }

    private void CheckIsValid()
    {
        if (!_isValid)
        {
            if (!string.IsNullOrEmpty(_title) &&
                !string.IsNullOrEmpty(_content) &&
                _category != null &&
                _category.IsValid)
            {
                _isValid = true;
            }
        }
    }

    [ContractInvariantMethod]
    void Invariant()
    {
        Contract.Invariant(
            !_isValid ||
                (!string.IsNullOrEmpty(_title) &&
                !string.IsNullOrEmpty(_content) &&
                _category != null &&
                _category.IsValid));
    }
}

public class CategoryRepository
{
    private readonly List<Category> _categories = new List<Category>(); 

    public void Add(Category category)
    {
        Contract.Requires(category != null);
        Contract.Requires(category.IsValid);

        Contract.Ensures(category.IsValid);

        _categories.Add(category);
    }
}

public class ArticleRepository
{
    private readonly List<Article> _articles = new List<Article>();

    public void Add(Article article)
    {
        Contract.Requires(article != null);
        Contract.Requires(article.IsValid);

        Contract.Ensures(article.IsValid);

        _articles.Add(article);
    }
}
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top