none
Reuse of assumptions/asserts? (continued)

    질문

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


    • 편집됨 Eyal Shilony 2012년 7월 6일 금요일 오후 2:51
    2012년 7월 6일 금요일 오전 8:59

모든 응답

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

    2012년 7월 6일 금요일 오후 2:47
  • Can someone shed some light on the subject?

    Regards,

    Eyal Shilony


    • 편집됨 Eyal Shilony 2012년 7월 25일 수요일 오전 9:31
    2012년 7월 10일 화요일 오후 10:12
  • 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


    • 편집됨 Eyal Shilony 2012년 7월 24일 화요일 오전 5:59
    2012년 7월 24일 화요일 오전 5:58