Reuse of assumptions/asserts? (continued)

Question

Hello,

By this post I made the following changes and indeed it works but in the following cases of the code it does not, why?

[ContractVerification(false)]
    public static class Assert
    {
        [Conditional("DEBUG")]
        public static void GreaterThan<T>(T value, T lowerBound) where T : IComparable<T>
        {
            Contract.Ensures(value.CompareTo(lowerBound) > 0);
        }

        [Conditional("DEBUG")]
        public static void GreaterThanOrEqual<T>(T value, T lowerBound) where T : IComparable<T>
        {
            Contract.Ensures(value.CompareTo(lowerBound) >= 0);
        }

        [Conditional("DEBUG")]
        public static void LessThan<T>(T value, T upperBound) where T : IComparable<T>
        {
            Contract.Ensures(value.CompareTo(upperBound) < 0);
        }

        [Conditional("DEBUG")]
        public static void LessThanOrEqual<T>(T value, T upperBound) where T : IComparable<T>
        {
            Contract.Ensures(value.CompareTo(upperBound) <= 0);
        }

        [Conditional("DEBUG")]
        public static void NotNull(object value)
        {
            Contract.Ensures(value != null);
        }

        [Conditional("DEBUG")]
        public static void NotNullOrEmpty(string value)
        {
            Contract.Ensures(!string.IsNullOrEmpty(value));
        }

        [Conditional("DEBUG")]
        public static void True(bool value)
        {
            Contract.Ensures(value);
        }

        [Conditional("DEBUG")]
        public static void False(bool value)
        {
            Contract.Ensures(!value);
        }

        [Conditional("DEBUG")]
        public static void InRange<T>(T value, T lowerBound, T upperBound, ExclusionMode exclusionMode = ExclusionMode.None) where T : IComparable<T>
        {
            Contract.Ensures(((exclusionMode | ExclusionMode.LowerBound) == ExclusionMode.LowerBound ? value.CompareTo(lowerBound) > 0 : value.CompareTo(lowerBound) >= 0) && ((exclusionMode | ExclusionMode.UpperBound) == ExclusionMode.UpperBound ? value.CompareTo(upperBound) < 0 : value.CompareTo(upperBound) <= 0));
        }
    }

Now, I got this method which is part of a large project that render the CAPTCHA.

public CaptchaImage RenderCaptcha(int width = 0, int height = 0)
		{
			string text = TextGenerator.GenerateText();

			if (width == 0 || height == 0)
			{
				SizeF size = GetTextDrawingArea(text);

				if (width == 0)
				{
					width = (int)size.Width;
				}

				if (height == 0)
				{
					height = (int)size.Height;
				}
			}

			Assert.GreaterThan(width, 0);
			Assert.GreaterThan(height, 0);

			// ASP.NET: Debugging and hitting F5 in the browser multiple times causes the Graphics object to 
			// throw InvalidOperationException `Object is currently in use elsewhere`,
			// locking on the current object puts the requests on hold while debugging.

			lock (this)
			{
				Bitmap image = new Bitmap(width, height, PixelFormat.Format32bppArgb);

				using (Graphics graphics = Graphics.FromImage(image))
				{
					RenderImage(graphics, text, width, height);
				}

				return CaptchaImage.Create(ExpirationTime, image, text);
			}
		}

The problem is that I get the following errors.

• Warning    CodeContracts: requires unproven: width > 0    e:\Projects\Visual Studio\DotNetAce\Source\DotNetAce.Web.Authentication.Captcha\CaptchaRenderer.cs    124    DotNetAce.Web.Authentication.Captcha
  
• Warning    CodeContracts: requires unproven: height > 0    e:\Projects\Visual Studio\DotNetAce\Source\DotNetAce.Web.Authentication.Captcha\CaptchaRenderer.cs    124    DotNetAce.Web.Authentication.Captcha

More examples.

protected virtual void RenderImage(Graphics graphics, string text, int width, int height)
		{
			Contract.Requires(graphics != null);
			Contract.Requires(!string.IsNullOrEmpty(text));
			Contract.Requires(width > 0);
			Contract.Requires(height > 0);

			Rectangle rectangle = new Rectangle(0, 0, width, height);

			Assert.GreaterThan(rectangle.Width, 0);
			Assert.GreaterThan(rectangle.Height, 0);

			graphics.SmoothingMode = SmoothingMode.AntiAlias;
			graphics.FillRectangle(Style.BackBrush, rectangle);

			StringFormat stringFormat = new StringFormat
			{
				Alignment = StringAlignment.Center,
				LineAlignment = StringAlignment.Center
			};

			using (GraphicsPath path = new GraphicsPath())
			{
				Font font = Style.Font;
				path.AddString(text, font.FontFamily, (int)font.Style, font.Size, rectangle, stringFormat);
				RenderFilters(graphics, path, rectangle);
				graphics.FillPath(Style.TextBrush, path);
			}
		}

• Warning    CodeContracts: requires unproven: rectangle.Width > 0    e:\Projects\Visual Studio\DotNetAce\Source\DotNetAce.Web.Authentication.Captcha\CaptchaRenderer.cs    187    DotNetAce.Web.Authentication.Captcha
• Warning    CodeContracts: requires unproven: rectangle.Height > 0    e:\Projects\Visual Studio\DotNetAce\Source\DotNetAce.Web.Authentication.Captcha\CaptchaRenderer.cs    187    DotNetAce.Web.Authentication.Captcha

protected char Shuffle()
        {
            for (int i = 0; i < Characters.Length; i++)
            {
                int index = GetRandomNumber(i, Characters.Length);

                if (index >= Characters.Length)
                {
                    throw new IndexOutOfRangeException();
                }

                Assert.LessThan(i, Characters.Length);
                
                char temp = Characters[i];

                Characters[i] = Characters[index];

                Characters[index] = temp;
            }

            return Characters[0];
        }

• Warning    CodeContracts: Array access might be above the upper bound    e:\Projects\Visual Studio\DotNetAce\Source\DotNetAce.Web.Authentication.Captcha\CaptchaTextGenerator.cs    100    DotNetAce.Web.Authentication.Captcha
  

Replacing them with assumptions is obviously working fine but the whole point is to remove some of the duplications I have into one place.

EDIT: I tried to use Contract.Assume together with IComparable directly like so 'Contract.Assume(i.CompareTo(Characters.Length) < 0);' just to check whether it works and apparently it fails on the exact cases above where I assume it shouldn't.

protected char Shuffle()
		{
			for (int i = 0; i < Characters.Length; i++)
			{
				int index = GetRandomNumber(i, Characters.Length);

				if (index >= Characters.Length)
				{
					throw new IndexOutOfRangeException();
				}

				Contract.Assume(i.CompareTo(Characters.Length) < 0);
				
				char temp = Characters[i];

				Characters[i] = Characters[index];

				Characters[index] = temp;
			}

			return Characters[0];
		}

---

Eyal (http://shilony.net), Regards.

Answer 1

I changed it to the following and it seems to work but obviously the generic version is more desirable.

[ContractVerification(false)]
	public static class Assert
	{
		[Conditional("DEBUG")]
		public static void GreaterThan(int value, int lowerBound)
		{
			Contract.Ensures(value > lowerBound);
		}

		[Conditional("DEBUG")]
		public static void GreaterThanOrEqual(int value, int lowerBound)
		{
			Contract.Ensures(value >= lowerBound);
		}

		[Conditional("DEBUG")]
		public static void LessThan(int value, int upperBound)
		{
			Contract.Ensures(value < upperBound);
		}

		[Conditional("DEBUG")]
		public static void LessThanOrEqual(int value, int upperBound)
		{
			Contract.Ensures(value <= upperBound);
		}

		[Conditional("DEBUG")]
		public static void NotNull(object value)
		{
			Contract.Ensures(value != null);
		}

		[Conditional("DEBUG")]
		public static void NotNullOrEmpty(string value)
		{
			Contract.Ensures(!string.IsNullOrEmpty(value));
		}

		[Conditional("DEBUG")]
		public static void True(bool value)
		{
			Contract.Ensures(value);
		}

		[Conditional("DEBUG")]
		public static void False(bool value)
		{
			Contract.Ensures(!value);
		}

		[Conditional("DEBUG")]
		public static void InRange(int value, int lowerBound, int upperBound, ExclusionMode exclusionMode = ExclusionMode.None)
		{
			Contract.Ensures(((exclusionMode | ExclusionMode.LowerBound) == ExclusionMode.LowerBound ? value > lowerBound : value >= lowerBound) && ((exclusionMode | ExclusionMode.UpperBound) == ExclusionMode.UpperBound ? value < upperBound : value <= upperBound));
		}
	}

---

Eyal (http://shilony.net), Regards.

Answer 2

Can someone shed some light on the subject?

---

Regards,

Eyal Shilony

Answer 3

Can anyone say something about it? is there something I'm missing or it's just not possible due to the nature of how CodeContracts work?

---

Regards,

Eyal Shilony