如何在 C# 中实现具有前置/后置条件和不变量的 Stack 类？

Question

有没有人有关于如何/什么是在 C# 中实现 Stack 类的最佳方法的示例或想法？我知道已经有一个 Stack 类，但我需要了解如何实际实现 Stack 类。

我还需要有关如何在 C# 中使用 Contract 来指定此类的前置条件、后置条件和不变量的建议。我想我以前在 ASP.NET MVC 架构中创建模型时使用过类似的东西，但我不完全确定它是否是相同的东西并且以相同的方式工作。 （我对先决条件/后置条件/不变量有点迷失，如果您还不能告诉我 - 所以请耐心等待。）

我的主要问题 - 有人可以给我关于的建议吗为诸如堆栈之类的类正确使用契约。

是的，我已经付出了努力：

public interface IStack
{
        void Push(Object e);
        Object Pop();
        Object Top();
        void EnsureCapacity();
    }
}

   public class Stack : IStack
{
    private Object[] elements;
    private int size = 0;

    public Stack()
    {
        elements = new Object[0];
    }

    public void Push(Object e)
    {
        // check if this array capacity has been reached and increase if needed
        EnsureCapacity();
        elements[size++] = e;
    }

    public Object Pop()
    {
        // check if the method call is invalid for the object's current state
        if (size == 0) throw new InvalidOperationException("Stack.Pop");

        Object result = elements[--size];
        elements[size] = null;

        return result;
    }

    public Object Top()
    {
        // check if the method call is invalid for the object's current state
        if (size == 0) throw new InvalidOperationException("Stack.top");
        return elements[(size - 1)];
    }

    private void EnsureCapacity()
    {
        if (elements.Length == size)
        {
            Object[] oldElements = elements;
            elements = new Object[(2 * size + 1)];
        }
    }
}

Answer 1

如果您愿意，为了开始使用 Microsoft 代码合同，我曾发表过一篇关于它的博客文章 。这篇文章涵盖了前置条件、后置条件和不变量的基本知识。

作为这些概念的总结，您可以将它们视为如下：

• 前提条件是在执行方法之前必须满足的条件——客户端向您的方法承诺的内容。
• 就您班级的客户而言，不变性是必须始终保持公开真实的东西。
• 后置条件是方法执行后必须成立的条件——您的方法向客户端承诺的内容。

所以，在我的脑海中，对于堆栈来说，一个容易想到的事情可能是一个不变量。如果您使用数组对堆栈进行建模，则可以在该类上声明一个不变量，即该数组永远不会设置为 null，例如，您可以定义该不变量方法：

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

看起来您已经有了一个前提条件pop 方法 - 您想说用户有责任确保执行 pop 时堆栈不为空。因此，在 pop 方法的开头，您需要：

Contract.Requires(size > 0);

最后，您可以在 pop 上指定一个后置条件，该大小将始终小于 pop 操作之前的大小（如果您愿意，您可以得到更具体的信息） )：

Contract.Ensures(Contract.OldValue<int>(size) > size);

祝你好运——合同很酷而且很有用。这是一种非常干净的编码方式。

Answer 2

C# 中实现的许多集合都是基于数组的。您可以使用数组并将元素添加到末尾，保留顶部 elemnet 的索引并在推送新元素时增加它，当然，当新对象出现并且存在时，数组将“必须动态扩展”（被新元素替换）当前数组中没有它们的位置。

代码合同在 http://research.microsoft.com 上提供了非常好的文档/en-us/projects/contracts/userdoc.pdf