Skip to content
This repository was archived by the owner on Jul 15, 2023. It is now read-only.

Remove/replace unprovable contracts. #85

Merged
SergeyTeplyakov merged 3 commits into from
Jul 9, 2015
Merged

Remove/replace unprovable contracts. #85

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
45b2843
Disable Contract.Requires that the static checker can't prove.
tom-englert Jul 3, 2015
6a190a3
Contracts in System.Math that the checker can't proof.
tom-englert Jul 3, 2015
07fd582
Moved comment from code to issue
tom-englert Jul 4, 2015
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 19 additions & 8 deletions Microsoft.Research/Contracts/MsCorlib/System.Math.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,29 +93,40 @@ public static Decimal Abs(Decimal value)
[Pure]
public static float Abs(float value)
{
Contract.Ensures((Contract.Result<float>() >= 0.0) || float.IsNaN(Contract.Result<float>()) || float.IsPositiveInfinity(Contract.Result<float>()));
Copy link
Contributor

@sharwell sharwell Jul 9, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 I would prefer this be written as:

Contract.Ensures(float.IsNaN(Contract.Result<float>()) || Contract.Result<float>() >= 0.0);

Copy link
Contributor Author

@tom-englert tom-englert Jul 10, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the checker had a problem to infer IsPositiveInfinity from x >= 0; if s.o. requires x >= 0 && !IsInfinity(x), this could pass if we not explicitly include IsPositiveInfinity!

I will add some test cases once I fully understood the CC regressing testing framework; once we have test cases, we can optimize this and maybe fix the checker to handle double/float more consistently.


// 2015-03-26: tom-englert
Copy link
Contributor

@sharwell sharwell Jul 9, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 If the Contract.Ensures lines below can be preserved in addition to the newly-inserted Contract.Ensures, then this comment can be removed. The new Ensures line is correct and there was no loss of information to include it.

Copy link
Contributor Author

@tom-englert tom-englert Jul 10, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

s.a.

// 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<float>() >= 0.0);
// Contract.Ensures(float.IsNaN(value) || Contract.Result<float>() >= 0.0);
Copy link
Contributor

@sharwell sharwell Jul 9, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

❓ What happens if instead of commenting out these Ensures lines, just just add the new one above?

Copy link
Contributor Author

@tom-englert tom-englert Jul 10, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This would work as well, but I found this would be too confusing - if it's commented, it's more clear that it is not active at all.

Copy link
Contributor

@sharwell sharwell Jul 10, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It only shows in the editor extensions quick info if it's active though. 😄 I created #104 to deal with this later since it was clear that you would benefit from having these changes in the first community preview.


// NaN ==> NaN
Contract.Ensures(!float.IsNaN(value) || float.IsNaN(Contract.Result<float>()));
// Contract.Ensures(!float.IsNaN(value) || float.IsNaN(Contract.Result<float>()));

// Infty ==> +Infty
Contract.Ensures(!float.IsInfinity(value) || float.IsPositiveInfinity(Contract.Result<float>()));
// Contract.Ensures(!float.IsInfinity(value) || float.IsPositiveInfinity(Contract.Result<float>()));

return default(float);
}

[Pure]
public static double Abs(double value)
{
{
Contract.Ensures((Contract.Result<double>() >= 0.0) || double.IsNaN(Contract.Result<double>()) || double.IsPositiveInfinity(Contract.Result<double>()));
Copy link
Contributor

@sharwell sharwell Jul 9, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 I would prefer this be written as:

Contract.Ensures(double.IsNaN(Contract.Result<double>() >= 0.0) || Contract.Result<double>() >= 0.0);

Copy link
Contributor Author

@tom-englert tom-englert Jul 10, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

s.a.


// 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<double>() >= 0.0);
// Contract.Ensures(double.IsNaN(value) || Contract.Result<double>() >= 0.0);

// NaN ==> NaN
Contract.Ensures(!double.IsNaN(value) || double.IsNaN(Contract.Result<double>()));

// Contract.Ensures(!double.IsNaN(value) || double.IsNaN(Contract.Result<double>()));
// Infty ==> +Infty
Contract.Ensures(!double.IsInfinity(value) || double.IsPositiveInfinity(Contract.Result<double>()));
// Contract.Ensures(!double.IsInfinity(value) || double.IsPositiveInfinity(Contract.Result<double>()));

return default(double);
}
Expand Down
29 changes: 13 additions & 16 deletions Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
using System.ComponentModel;
using System.Diagnostics.Contracts;


namespace System.Windows
{
// Summary:
Expand Down Expand Up @@ -214,7 +215,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));
Expand Down Expand Up @@ -339,7 +340,7 @@ public double Width
}
set
{
Contract.Requires(!this.IsEmpty);
// Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
Copy link
Contributor

@sharwell sharwell Jul 3, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💭 It would be really cool if the contract block allowed the use of Contract.Assume, allowing us to immediately start codifying requirements which are valid but not currently supported by the static checker. For example, this method could use the following contract:

Contract.Assume(!this.IsEmpty); // Required, but not currently provable statically
Contract.Requires(value >= 0.0 || Double.IsNaN(value));

Contract.Requires(value >= 0.0 || Double.IsNaN(value));

Contract.Ensures(this.Width == value || Double.IsNaN(value));
Expand All @@ -361,7 +362,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));
}
Expand All @@ -382,7 +383,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));
}
Expand Down Expand Up @@ -484,8 +485,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:
Expand All @@ -500,8 +500,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:
Expand All @@ -523,7 +522,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);
}
Expand All @@ -546,7 +545,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);
}
Expand Down Expand Up @@ -599,8 +598,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:
Expand All @@ -618,8 +616,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:
Expand All @@ -641,7 +638,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);
}
Expand All @@ -668,7 +665,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);
}
Expand Down
4 changes: 2 additions & 2 deletions Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down Expand Up @@ -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));
Expand Down