using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework;
using Microsoft.VisualStudio.TestTools.UnitTesting; 

namespace Sample
{
    [TestClass]
    [PexClass(typeof(UIntStack))]
    public partial class UIntStackPexBasicTestPUT
    {
        //This PUT test class is a holder for parameterized unit tests generalized from conventional unit tests
        //This PUT test class includes parameterized unit tests generalized from UIntStackPexBasicTest, including
        //conventional test cases that are created from JUnit test cases found at:
        /*
         * 
            http://rockfish-cs.cs.unc.edu/testing/
            http://rockfish-cs.cs.unc.edu/jax/lindsey/
            http://rockfish-cs.cs.unc.edu/JAX/
            http://rockfish-cs.cs.unc.edu/JUnitExamples/

            Here are their related papers:
            http://rockfish.cs.unc.edu/pubs/TR02-012.pdf
            http://rockfish.cs.unc.edu/misc/ajax-SEL02abst.pdf
            http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.1219
         */

        //Naming convention: for a conventional test case testXXX, the PUT generalized from it is testXXXPUT being prefixed by meaningful 
        //words to indicate the purpose of the PUT, such as TestFullPUTCheckFullAfterPop
        //When filling here a PUT, please copy its corresponding conventional unit test above the PUT and comment
        //out the conventional unit test with /* */. When multiple PUTs are created from the same conventional unit test,
        //you need to copy only the conventional unit test once above the first PUT. Below is one example: generalizing 
        //TestFullPUT1, TestFullPUT2, and TestFullPUT3 from TestFull.

        /*
         *
         *public void TestFull()
        // Tests the fulling of the stack. 
        {
            UIntStack numbers = new UIntStack();
            int k = 3;
            int j = 2;
            numbers.Push(k);
            PexAssert.IsTrue(!numbers.IsFull());
            numbers.Push(j);
            PexAssert.IsTrue(numbers.IsFull());
            numbers.Pop();
            PexAssert.IsTrue(!numbers.IsFull());
        }
         */

        [PexMethod]
        public void TestFullPUTCheckFullAfterPushOnNotNearFull([PexAssumeUnderTest]UIntStack numbers, int i)
        {
            PexAssume.IsTrue(numbers.GetNumberOfElements() < (numbers.MaxSize() - 1));
            numbers.Push(i);
            PexAssert.IsTrue(!numbers.IsFull());
        }

        [PexMethod]
        public void TestFullPUTCheckFullAfterPushOnNearFull(UIntStack numbers, int i)
        {
            PexAssume.IsTrue(numbers.GetNumberOfElements() == (numbers.MaxSize() - 1));
            PexAssume.IsTrue(!numbers.IsMember(i));
            numbers.Push(i);
            PexAssert.IsTrue(numbers.IsFull());
        }

        [PexMethod]
        public void TestFullPUTCheckFullAfterPop([PexAssumeUnderTest]UIntStack numbers)
        {
            numbers.Pop();
            PexAssert.IsTrue(!numbers.IsFull());
        }


    }
}