4

我开始使用启用静态和运行时检查的 C# 代码契约。问题是一些代码契约检查可能会在方法之间重复，我看不出有什么好的方法可以避免这种情况。

我希望完全避免静态分析器警告，如果可能的话不要抑制它。

让我们考虑这个例子：

有以下简单的类。这是业务逻辑模型类的常见示例：

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

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

对于一些基于反射的技术（如 MVC 中的模型绑定、数据库映射），我们需要为模型属性提供公共默认构造函数和公共设置器。所以我们不能保证例如对于 Category 的 Contract.Invariant(!string.IsNullOrEmpty(Name)) 总是正确的。

然后我们在内部 CategoryRepository 类中创建下一个方法。我们假设所有验证都较早通过并且只接受有效类别：

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

到目前为止，一切都很好。然后我们在 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));
    ...
}

问题是：

1）在我们期望通过合同获得有效类别的每个地方，我们需要重复检查，例如：

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

有时我们还需要在 Contract.Assume 方法中进行这些检查。

2）外部类（如文章）应检查类别类的合同。看起来违反了LoW和基本封装原则。

我尝试了下一个解决方案：

1) 将重复代码提取到 Category 类中的纯方法，如下所示：

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

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

并以这种方式使用合同：

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

不是很好的解决方案，也不起作用 - 静态分析器不满意。

2) 为类别定义一个不变量：

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

这个解决方案非常好，允许从 Category 类中删除不必要的检查，但实际上这个不变量是无效的（例如在默认构造函数中）。静态分析器正确检测到这种违规行为。

我做错了什么吗？有一种更方便的方法可以将代码合同与静态分析器一起使用吗？

4

1 回答 1

1

您可以使用popsicle 不变性的想法并做人们可能称之为popsicle 有效性的事情：换句话说，虽然一个对象并非在任何时候都有效，但一旦设置了它的所有属性，它就会变得有效并保持这种状态。

这样，您可以在包含数据的对象中进行有效性检查，并将使用这些对象的代码上的合同简化为简单的thing != null && thing.IsValid().

下面是一些代码来演示这种方法。静态检查器仍然需要一些帮助来证明它a是有效的，因为它的属性是独立设置的，但这可能是您在通过反射构造对象之后想要对它进行的检查。

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);
    }
}
于 2013-11-03T01:01:52.000 回答