Stack.cs

using System;
using System.Diagnostics.Contracts;

namespace Stack
{
    public class StackEmpty : Exception { }

    public class Stack
    {
        private object[] arr;

        private int nextFree;

        public Stack(int len)
        {
            Contract.Requires(len > 0);

            arr = new object[len];
            nextFree = 0;
        }

        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(arr != null);
            Contract.Invariant(arr.Length > 0);
            Contract.Invariant(nextFree <= arr.Length);
            Contract.Invariant(nextFree >= 0);
        }

        public bool IsEmpty
        {
            get
            {
                return nextFree == 0;
            }
        }

        public void Push(object x)
        {
            Contract.Requires(x != null);

            if (nextFree >= arr.Length)
            {
                Array.Resize<object>(ref arr, arr.Length * 2);
            }
            arr[nextFree] = x;
            nextFree = nextFree + 1;
        }

        public object Pop()
        {
            if (nextFree < 1)
                throw new StackEmpty();

            nextFree = nextFree - 1;
            object x = arr[nextFree];
            arr[nextFree] = null;
            return x;
        }
    }
}