From 9b2a377ea07cbaef78ba3d2acb2b35ac0780ca74 Mon Sep 17 00:00:00 2001
From: Yaakov <yaakov.smith@wisetechglobal.com>
Date: Thu, 19 Nov 2015 13:50:06 +1100
Subject: [PATCH 1/3] Add contracts for System.OperatingSystem

Based on MSDN and Microsoft Reference Source.
---
 .../MsCorlib/System.OperatingSystem.cs        | 38 ++++++++++++++++++-
 1 file changed, 36 insertions(+), 2 deletions(-)

diff --git a/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs b/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs
index dda8e732..f34c332b 100644
--- a/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs
+++ b/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs
@@ -23,12 +23,41 @@ public class OperatingSystem: ICloneable
 
     public PlatformID Platform
     {
-      get { return default(PlatformID); }
+      [Pure]
+      get
+      {
+        Contract.Ensures(Contract.Result<PlatformID>() >= PlatformID.Win32S);
+        Contract.Ensures(Contract.Result<PlatformID>() <= PlatformID.MacOSX);
+        return default(PlatformID);
+      }
+    }
+
+    public string ServicePack
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<string>() != null);
+        return default(string);
+      }
     }
 
     public Version Version
     {
-      get { return default(Version); }
+      [Pure]
+      get
+      {
+        Contract.Ensures(Contract.Result<Version>() != null);
+        return default(Version);
+      }
+    }
+
+    public string VersionString
+    {
+      get
+      {
+        Contract.Ensures(!string.IsNullOrWhitespace(Contract.Result<string>()));
+        return default(Version);
+      }
     }
 
     public object Clone()
@@ -36,9 +65,14 @@ public object Clone()
 
       return default(object);
     }
+
     public OperatingSystem(PlatformID platform, Version version)
     {
+      Contract.Requires(platform >= PlatformID.Win32S)
+      Contract.Requires(platform <= PlatformID.MacOSX)
       Contract.Requires(version != null);
+      Contract.EnsuresOnThrow<ArgumentException>(true, "platform is not a PlatformID enumeration value.")
+      Contract.EnsuresOnThrow<ArgumentNullException>(true, "version is null.")
     }
   }
 }

From 8849a3a24f26e0740f723a8c9e0cc3e2733666eb Mon Sep 17 00:00:00 2001
From: Yaakov <yaakov.smith@wisetechglobal.com>
Date: Thu, 19 Nov 2015 14:28:58 +1100
Subject: [PATCH 2/3] Add [Pure] to OperatingSystem.ServicePack

---
 Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs b/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs
index f34c332b..57602026 100644
--- a/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs
+++ b/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs
@@ -34,6 +34,7 @@ public PlatformID Platform
 
     public string ServicePack
     {
+      [Pure]
       get
       {
         Contract.Ensures(Contract.Result<string>() != null);

From d4bb09ece67ec0d6bae3199beca03ffb16aa4721 Mon Sep 17 00:00:00 2001
From: Yaakov <yaakov.smith@wisetechglobal.com>
Date: Thu, 19 Nov 2015 15:20:42 +1100
Subject: [PATCH 3/3] Fix mismatching return value

---
 Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs b/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs
index 57602026..a7eed6ad 100644
--- a/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs
+++ b/Microsoft.Research/Contracts/MsCorlib/System.OperatingSystem.cs
@@ -57,7 +57,7 @@ public string VersionString
       get
       {
         Contract.Ensures(!string.IsNullOrWhitespace(Contract.Result<string>()));
-        return default(Version);
+        return default(string);
       }
     }