From 45b28431b8fcbe3d4551d48ee46ef21215190d26 Mon Sep 17 00:00:00 2001 From: tom-englert Date: Fri, 3 Jul 2015 17:36:49 +0200 Subject: [PATCH 1/3] Disable Contract.Requires that the static checker can't prove. --- .../WindowsBase/System.Windows.Rect.cs | 41 +++++++++++-------- .../WindowsBase/System.Windows.Size.cs | 4 +- 2 files changed, 27 insertions(+), 18 deletions(-) diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs index a6484eee..a318ec0b 100644 --- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs +++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs @@ -16,6 +16,19 @@ using System.ComponentModel; using System.Diagnostics.Contracts; + +// 2015-03-36: tom-englert +// Temporarily disabled checks for Contract.Requires(!this.IsEmpty); +// => This requirement is true, but it's impossible to proof with acceptable effort. +// Even simple code like +// +// var r = new Rect(); +// r.Widht = 10.0; +// +// will create a warning "CodeContracts: requires unproven: !this.IsEmpty. Are you making some assumption on get_Width that the static checker is unaware of?" +// As soon as the checker can infer the proper constraints, this can be enabled again. + + namespace System.Windows { // Summary: @@ -214,7 +227,7 @@ public double Height } set { - Contract.Requires(!this.IsEmpty); + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. Contract.Requires(value >= 0.0 || Double.IsNaN(value)); Contract.Ensures(this.Height == value || Double.IsNaN(value)); @@ -339,7 +352,7 @@ public double Width } set { - Contract.Requires(!this.IsEmpty); + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. Contract.Requires(value >= 0.0 || Double.IsNaN(value)); Contract.Ensures(this.Width == value || Double.IsNaN(value)); @@ -361,7 +374,7 @@ public double X } set { - Contract.Requires(!this.IsEmpty); + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. Contract.Ensures(this.X == value || Double.IsNaN(value)); } @@ -382,7 +395,7 @@ public double Y } set { - Contract.Requires(!this.IsEmpty); + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. Contract.Ensures(this.Y == value || Double.IsNaN(value)); } @@ -484,8 +497,7 @@ public double Y // the rectangle's System.Windows.Rect.Top and System.Windows.Rect.Bottom properties. public void Inflate(Size size) { - Contract.Requires(!this.IsEmpty); - + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.Contract.Requires(!this.IsEmpty); } // // Summary: @@ -500,8 +512,7 @@ public void Inflate(Size size) // The amount by which to expand or shrink the top and bottom sides of the rectangle. public void Inflate(double width, double height) { - Contract.Requires(!this.IsEmpty); - + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. } // // Summary: @@ -523,7 +534,7 @@ public void Inflate(double width, double height) // The resulting rectangle. public static Rect Inflate(Rect rect, Size size) { - Contract.Requires(!rect.IsEmpty); + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. return default(Rect); } @@ -546,7 +557,7 @@ public static Rect Inflate(Rect rect, Size size) // The resulting rectangle. public static Rect Inflate(Rect rect, double width, double height) { - Contract.Requires(!rect.IsEmpty); + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. return default(Rect); } @@ -599,8 +610,7 @@ public static Rect Inflate(Rect rect, double width, double height) // This method is called on the System.Windows.Rect.Empty rectangle. public void Offset(Vector offsetVector) { - Contract.Requires(!this.IsEmpty); - + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. } // // Summary: @@ -618,8 +628,7 @@ public void Offset(Vector offsetVector) // This method is called on the System.Windows.Rect.Empty rectangle. public void Offset(double offsetX, double offsetY) { - Contract.Requires(!this.IsEmpty); - + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. } // // Summary: @@ -641,7 +650,7 @@ public void Offset(double offsetX, double offsetY) // rect is System.Windows.Rect.Empty. public static Rect Offset(Rect rect, Vector offsetVector) { - Contract.Requires(!rect.IsEmpty); + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. return default(Rect); } @@ -668,7 +677,7 @@ public static Rect Offset(Rect rect, Vector offsetVector) // rect is System.Windows.Rect.Empty. public static Rect Offset(Rect rect, double offsetX, double offsetY) { - Contract.Requires(!rect.IsEmpty); + // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. return default(Rect); } diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs index 6e2ea04a..5598ccfb 100644 --- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs +++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs @@ -140,7 +140,7 @@ public double Height } set { - Contract.Requires(!this.IsEmpty); + // Contract.Requires(!this.IsEmpty); => see comment in Rect Contract.Requires(value >= 0.0 || Double.IsNaN(value)); Contract.Ensures(this.Height == value || Double.IsNaN(value)); @@ -179,7 +179,7 @@ public double Width } set { - Contract.Requires(!this.IsEmpty); + // Contract.Requires(!this.IsEmpty); => see comment in Rect Contract.Requires(value >= 0.0 || Double.IsNaN(value)); Contract.Ensures(this.Width == value || Double.IsNaN(value)); From 6a190a3dcbcd6debe1864ba05265ca1c6c37b92c Mon Sep 17 00:00:00 2001 From: tom-englert Date: Fri, 3 Jul 2015 19:23:06 +0200 Subject: [PATCH 2/3] Contracts in System.Math that the checker can't proof. --- .../Contracts/MsCorlib/System.Math.cs | 27 +++++++++++++------ 1 file changed, 19 insertions(+), 8 deletions(-) diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Math.cs b/Microsoft.Research/Contracts/MsCorlib/System.Math.cs index a0a985e0..47f53711 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Math.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Math.cs @@ -93,29 +93,40 @@ public static Decimal Abs(Decimal value) [Pure] public static float Abs(float value) { + Contract.Ensures((Contract.Result() >= 0.0) || float.IsNaN(Contract.Result()) || float.IsPositiveInfinity(Contract.Result())); + + // 2015-03-26: tom-englert + // Disabled, since this was too complex for the checker to understand. + // e.g. new Rect(0, 0, Math.Abs(a), Math.Abs(b)) raised a warning that with and height are unproven to be positive values. + // !NaN ==> >= 0 - Contract.Ensures(float.IsNaN(value) || Contract.Result() >= 0.0); + // Contract.Ensures(float.IsNaN(value) || Contract.Result() >= 0.0); // NaN ==> NaN - Contract.Ensures(!float.IsNaN(value) || float.IsNaN(Contract.Result())); + // Contract.Ensures(!float.IsNaN(value) || float.IsNaN(Contract.Result())); // Infty ==> +Infty - Contract.Ensures(!float.IsInfinity(value) || float.IsPositiveInfinity(Contract.Result())); + // Contract.Ensures(!float.IsInfinity(value) || float.IsPositiveInfinity(Contract.Result())); return default(float); } [Pure] public static double Abs(double value) - { + { + Contract.Ensures((Contract.Result() >= 0.0) || double.IsNaN(Contract.Result()) || double.IsPositiveInfinity(Contract.Result())); + + // 2015-03-26: tom-englert + // Disabled, since this was too complex for the checker to understand. + // e.g. new Rect(0, 0, Math.Abs(a), Math.Abs(b)) raised a warning that with and height are unproven to be positive values. + // !NaN ==> >= 0 - Contract.Ensures(double.IsNaN(value) || Contract.Result() >= 0.0); + // Contract.Ensures(double.IsNaN(value) || Contract.Result() >= 0.0); // NaN ==> NaN - Contract.Ensures(!double.IsNaN(value) || double.IsNaN(Contract.Result())); - + // Contract.Ensures(!double.IsNaN(value) || double.IsNaN(Contract.Result())); // Infty ==> +Infty - Contract.Ensures(!double.IsInfinity(value) || double.IsPositiveInfinity(Contract.Result())); + // Contract.Ensures(!double.IsInfinity(value) || double.IsPositiveInfinity(Contract.Result())); return default(double); } From 07fd582586caa9192799def820e94a7265617f20 Mon Sep 17 00:00:00 2001 From: tom-englert Date: Sat, 4 Jul 2015 16:13:54 +0200 Subject: [PATCH 3/3] Moved comment from code to issue --- .../Contracts/WindowsBase/System.Windows.Rect.cs | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs index a318ec0b..af2ee496 100644 --- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs +++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs @@ -17,18 +17,6 @@ using System.Diagnostics.Contracts; -// 2015-03-36: tom-englert -// Temporarily disabled checks for Contract.Requires(!this.IsEmpty); -// => This requirement is true, but it's impossible to proof with acceptable effort. -// Even simple code like -// -// var r = new Rect(); -// r.Widht = 10.0; -// -// will create a warning "CodeContracts: requires unproven: !this.IsEmpty. Are you making some assumption on get_Width that the static checker is unaware of?" -// As soon as the checker can infer the proper constraints, this can be enabled again. - - namespace System.Windows { // Summary: