none
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.


    Friday, July 06, 2012 8:59 AM

All replies

  • 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.

    Friday, July 06, 2012 2:47 PM
  • Can someone shed some light on the subject?

    Regards,

    Eyal Shilony


    Tuesday, July 10, 2012 10:12 PM
  • 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


    Tuesday, July 24, 2012 5:58 AM