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

namespace CreditCard
{
    [PexClass(typeof(CreditCardValidator))]
    partial class CreditCardValidator
    {
        public const int MASTERCARD = 0;
        public const int VISA = 1;
        public const int DISCOVER = 2;
        public const int AMERICANEXPRESS = 3; 
      
        static public bool isVisaMatch(string card) {
            string PREFIX = "4";
            return (
                card.Substring(0, 1).Equals(PREFIX)
                    && (card.Length == 13 || card.Length == 16));
        }

        static public bool isAmexMatch(string card)
        {
            //string PREFIX = "34,37,";
            string prefix2 = card.Substring(0, 2);
            return ((prefix2.IndexOf("34") != -1) ||
                    (prefix2.IndexOf("37") != -1))
                     && (card.Length == 15);
        }

        static public bool isDiscoverMatch(string card)
        {
             string PREFIX = "6011";       
             return (card.Substring(0, 4).Equals(PREFIX) && (card.Length == 16));
        }

        static public bool isMasterMatch(string card)
        {
           //string PREFIX = "51,52,53,54,55,";
           string prefix2 = card.Substring(0, 2);
            return (prefix2.Equals("51") ||
                prefix2.Equals("52") ||
                prefix2.Equals("53") ||
                prefix2.Equals("54") ||
                prefix2.Equals("55")) && (card.Length == 16);
        }

        public static bool Validate(string cardNumber, int type)
        {
            if (cardNumber == null)
                throw new ArgumentNullException("cardNumber");

            switch (type) {
                case VISA: 
                  if (!isVisaMatch(cardNumber))
                    throw new ArgumentNullException("cardNumber");
                  break;
                case MASTERCARD:
                  if (!isMasterMatch(cardNumber))
                      throw new ArgumentNullException("cardNumber");
                  break;
                case DISCOVER:
                  if (!isDiscoverMatch(cardNumber))
                      throw new ArgumentNullException("cardNumber");
                  break;
                case AMERICANEXPRESS:
                  if (!isAmexMatch(cardNumber))
                      throw new ArgumentNullException("cardNumber");
                  break;
                default:
                    throw new ArgumentNullException("cardNumber");
            }

            int sum = 0;
            for (int i = 0; i < cardNumber.Length; i++)
            {
                int digit = cardNumber[i] - '0';
                if (digit < 0 || digit > 9)
                    return false;

                if ((cardNumber.Length - i) % 2 != 0)
                    sum += digit;
                else if (digit < 5)
                    sum += digit * 2;
                else
                    sum += digit * 2 - 9;
            }
            return sum % 10 == 0;
        }        


        //Below are parameterized unit tests for which Pex generates test inputs
	//The generated test inputs try to pass the validation check

        [PexMethod(MaxRuns = 3000, MaxBranches = 1000)]
        public void TestRealCreditCard()
        {
            if (Validate("111", MASTERCARD))
                PexAssert.IsTrue(false);
        }

        [PexMethod(MaxRuns = 3000, MaxBranches = 1000)]
        public void TestCreditCard(string s, int type)
        {
            //PexAssume.IsTrue(type == MASTERCARD);
            //PexAssume.IsTrue(type == VISA);
            //PexAssume.IsTrue(!s.Equals("4286004800000"));

            //PexAssume.IsTrue(type == DISCOVER);
            //PexAssume.IsTrue(type == AMERICANEXPRESS);
            if (Validate(s, type))
                PexAssert.IsTrue(false);
        }
     
    }
}