White box testing with PEX

// <copyright file="InsurerPexTest.cs" company="Microsoft">Copyright � Microsoft 2012</copyright>
using System;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Validation;
using Microsoft.VisualStudio.TestTools.UnitTesting;
using SampleApp;
using SampleApp.DAL;
using SampleApp.Entity;

namespace SampleApp
{
    /// <summary>This class contains parameterized unit tests for Insurer</summary>
    [PexClass(typeof(Insurer))]
    [PexAllowedExceptionFromTypeUnderTest(typeof(InvalidOperationException))]
    [PexAllowedExceptionFromTypeUnderTest(typeof(ArgumentException), AcceptExceptionSubtypes = true)]
    [TestClass]
    public partial class InsurerPexTest
    {
        /// <summary>Test stub for .ctor(IDAL)</summary>
        [PexMethod]
        public Insurer Constructor(IDAL dal)
        {
            Insurer target = new Insurer(dal);
            return target;
            // TODO: add assertions to method InsurerPexTest.Constructor(IDAL)
        }

        /// <summary>Test stub for GetInsureAmount(Person)</summary>
        [PexMethod(MaxBranches=20000), PexAllowedException(typeof(NotEligibleException))]
        public float GetInsureAmount([PexAssumeUnderTest]Insurer target, Person p)
        {
            float result = target.GetInsureAmount(p);
            return result;
            // TODO: add assertions to method InsurerPexTest.GetInsureAmount(Insurer, Person)
        }

        [PexMethod, PexAllowedException(typeof(NotEligibleException))]
        public float GetInsureAmount01()
        {
            Insurer target = InsurerFactory.Create01();
            Person p = new Person();
            float result = target.GetInsureAmount(p);
            return result;
            // TODO: add assertions to method InsurerPexTest.GetInsureAmount(Insurer, Person)
        }

        /// <summary>Test stub for IsPersonEligible(Person)</summary>
        [PexMethod]
        public bool IsPersonEligible([PexAssumeUnderTest]Insurer target, Person p)
        {
            bool result = target.IsPersonEligible(p);            
            return result;
            // TODO: add assertions to method InsurerPexTest.IsPersonEligible(Insurer, Person)
        }
    }
}