From 3bc4a0d8c62655a55a62e2188ab482918562c97d Mon Sep 17 00:00:00 2001 From: Yaakov Date: Tue, 1 Dec 2015 12:42:47 +1100 Subject: [PATCH 1/3] Add contracts for System.Version --- .../MsCorlib/MsCorlib.Contracts10.csproj | 3 +- .../Contracts/MsCorlib/System.Version.cs | 49 ++++++++++++++++++- 2 files changed, 49 insertions(+), 3 deletions(-) diff --git a/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj b/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj index 9055a5be..9eb9f5b4 100644 --- a/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj +++ b/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj @@ -351,7 +351,6 @@ - @@ -905,7 +904,7 @@ Include="System.Security.Principal.WindowsPrincipal.cs" /> --> - + diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Version.cs b/Microsoft.Research/Contracts/MsCorlib/System.Version.cs index 5ea6b5a1..83b10885 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Version.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Version.cs @@ -22,26 +22,42 @@ namespace System public class Version: ICloneable, IComparable { + [Pure] public int Minor { get { return default(int); } } + [Pure] public int Major { get { return default(int); } } + [Pure] public int Revision { get { return default(int); } } + [Pure] public int Build { get { return default(int); } } + [Pure] + public int MajorRevision + { + get { return default(int); } + } + + [Pure] + public int MinorRevision + { + get { return default(int); } + } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static bool operator >= (Version v1, Version v2) { @@ -85,9 +101,27 @@ public object Clone () { return default(object); } +#if SILVERLIGHT || NETFRAMEWORK_4_0 + [Pure] + public static Version Parse(string input) { + Contract.Requires(input != null); + Contract.Ensures(Contract.Result() != null); + return default(Version); + } + [Pure] + public static bool TryParse(string input, out Version result) { + Contract.Requires(input != null); + Contract.Ensures(!Contract.Result() || Contract.ValueAtReturn(out result) != null); + result = default(Version); + return default(bool); + } +#endif #if !SILVERLIGHT public Version () { - + Contract.Ensures(Major == 0); + Contract.Ensures(Minor == 0); + Contract.Ensures(Build == -1); + Contract.Ensures(Revision == -1); } #endif public Version (string version) { @@ -97,12 +131,20 @@ public Version (string version) { public Version (int major, int minor) { Contract.Requires(major >= 0); Contract.Requires(minor >= 0); + Contract.Ensures(Major == major); + Contract.Ensures(Minor == minor); + Contract.Ensures(Build == -1); + Contract.Ensures(Revision == -1); } public Version (int major, int minor, int build) { Contract.Requires(major >= 0); Contract.Requires(minor >= 0); Contract.Requires(build >= 0); + Contract.Ensures(Major == major); + Contract.Ensures(Minor == minor); + Contract.Ensures(Build == build); + Contract.Ensures(Revision == -1); } public Version (int major, int minor, int build, int revision) { @@ -110,6 +152,11 @@ public Version (int major, int minor, int build, int revision) { Contract.Requires(minor >= 0); Contract.Requires(build >= 0); Contract.Requires(revision >= 0); + Contract.Ensures(Major == major); + Contract.Ensures(Minor == minor); + Contract.Ensures(Build == build); + Contract.Ensures(Revision == revision); + } } } From ccc8478ebde9194b87d2a0cac8d798536b4ba91b Mon Sep 17 00:00:00 2001 From: Yaakov Date: Wed, 2 Dec 2015 09:36:15 +1100 Subject: [PATCH 2/3] Add postconditions to System.Version properties --- .../Contracts/MsCorlib/System.Version.cs | 30 +++++++++++++++---- 1 file changed, 24 insertions(+), 6 deletions(-) diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Version.cs b/Microsoft.Research/Contracts/MsCorlib/System.Version.cs index 83b10885..4e2f2ec9 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Version.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Version.cs @@ -25,37 +25,55 @@ public class Version: ICloneable, IComparable [Pure] public int Minor { - get { return default(int); } + get { + Contract.Ensures(Contract.Result() >= 0); + return default(int); + } } [Pure] public int Major { - get { return default(int); } + get { + Contract.Ensures(Contract.Result() >= 0); + return default(int); + } } [Pure] public int Revision { - get { return default(int); } + get { + Contract.Ensures(Contract.Result() >= -1); + return default(int); + } } [Pure] public int Build { - get { return default(int); } + get { + Contract.Ensures(Contract.Result() >= -1); + return default(int); + } } [Pure] public int MajorRevision { - get { return default(int); } + get { + Contract.Ensures(Contract.Result() >= -1); + return default(int); + } } [Pure] public int MinorRevision { - get { return default(int); } + get { + Contract.Ensures(Contract.Result() >= -1); + return default(int); + } } [Pure][Reads(ReadsAttribute.Reads.Nothing)] From 90285daa3d0c5bb72df22224bf21d7bb6598623f Mon Sep 17 00:00:00 2001 From: Yaakov Date: Thu, 3 Dec 2015 08:50:19 +1100 Subject: [PATCH 3/3] Fix return types of System.Version MajorRevision/MinorRevision --- .../Contracts/MsCorlib/System.Version.cs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Version.cs b/Microsoft.Research/Contracts/MsCorlib/System.Version.cs index 4e2f2ec9..8ce66633 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Version.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Version.cs @@ -59,20 +59,20 @@ public int Build } [Pure] - public int MajorRevision + public short MajorRevision { get { - Contract.Ensures(Contract.Result() >= -1); - return default(int); + Contract.Ensures(Contract.Result() >= -1); + return default(short); } } [Pure] - public int MinorRevision + public short MinorRevision { get { - Contract.Ensures(Contract.Result() >= -1); - return default(int); + Contract.Ensures(Contract.Result() >= -1); + return default(short); } }