Boogie: Basetypes port 1/3: Committing new sources

4 files changed, 536 insertions, 577 deletions

diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj
index 46901fae..eed8639e 100644
--- a/Source/Basetypes/Basetypes.csproj
+++ b/Source/Basetypes/Basetypes.csproj
@@ -1,107 +1,99 @@
-<?xml version="1.0" encoding="utf-8"?>

-<VisualStudioProject>

-  <XEN ProjectType="Local"

-     SchemaVersion="1.0"

-     Name="Basetypes"

-     ProjectGuid="0c692837-77ec-415f-bf04-395e3ed06e9a"

-    >

-    <Build>

-      <Settings ApplicationIcon=""

-         AssemblyName="Basetypes"

-         OutputType="Library"

-         RootNamespace="Basetypes"

-         StartupObject=""

-         StandardLibraryLocation=""

-         TargetPlatform="v2"

-         TargetPlatformLocation=""

-        >

-        <Config Name="Debug"

-           AllowUnsafeBlocks="False"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="False"

-           ConfigurationOverrideFile=""

-           DefineConstants="DEBUG;TRACE"

-           DocumentationFile=""

-           DebugSymbols="True"

-           FileAlignment="4096"

-           IncrementalBuild="True"

-           Optimize="False"

-           OutputPath="bin\debug"

-           RegisterForComInterop="False"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="False"

-           WarningLevel="4"

-           CheckContractAdmissibility="True"

-           CheckPurity="False"

-           />

-        <Config Name="Release"

-           AllowUnsafeBlocks="false"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="false"

-           ConfigurationOverrideFile=""

-           DefineConstants="TRACE"

-           DocumentationFile=""

-           DebugSymbols="false"

-           FileAlignment="4096"

-           IncrementalBuild="false"

-           Optimize="true"

-           OutputPath="bin\release"

-           RegisterForComInterop="false"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="false"

-           WarningLevel="4"

-           CheckContractAdmissibility="True"

-           CheckPurity="False"

-           />

-      </Settings>

-      <References>

-        <Reference Name="System"

-             AssemblyName="System"

-             Private="false"

-             />

-        <Reference Name="System.Data"

-             AssemblyName="System.Data"

-             Private="false"

-             />

-        <Reference Name="System.Xml"

-             AssemblyName="System.Xml"

-             Private="false"

-             />

-        <Reference Name="FSharp.Core"

-             AssemblyName="FSharp.Core"

-             Private="false"

-             HintPath="../../Binaries/FSharp.Core.dll"

-             />

-        <Reference Name="FSharp.PowerPack"

-             AssemblyName="FSharp.PowerPack"

-             Private="false"

-             HintPath="../../Binaries/FSharp.PowerPack.dll"

-             />

-      </References>

-    </Build>

-    <Files>

-      <Include>

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="BigNum.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="Rational.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="..\version.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="Set.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="AssemblyInfo.ssc"

-                 />

-      </Include>

-    </Files>

-  </XEN>

-</VisualStudioProject>
\ No newline at end of file
+<?xml version="1.0" encoding="utf-8"?>

+<Project ToolsVersion="3.5" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

+  <PropertyGroup>

+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

+    <ProductVersion>9.0.30729</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>Basetypes</RootNamespace>

+    <AssemblyName>Basetypes</AssemblyName>

+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>

+    <SignAssembly>true</SignAssembly>

+    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

+    <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly>

+    </CodeContractsCustomRewriterAssembly>

+    <CodeContractsCustomRewriterClass>

+    </CodeContractsCustomRewriterClass>

+    <CodeContractsLibPaths>

+    </CodeContractsLibPaths>

+    <CodeContractsExtraRewriteOptions>

+    </CodeContractsExtraRewriteOptions>

+    <CodeContractsExtraAnalysisOptions>

+    </CodeContractsExtraAnalysisOptions>

+    <CodeContractsBaseLineFile>

+    </CodeContractsBaseLineFile>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="FSharp.Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\FSharp.Core.dll</HintPath>

+    </Reference>

+    <Reference Include="FSharp.PowerPack, Version=1.9.9.9, Culture=neutral, PublicKeyToken=a19089b1c74d0809, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\FSharp.PowerPack.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\Microsoft.Contracts.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

+    <Reference Include="System.Data" />

+    <Reference Include="System.Xml" />

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="BigNum.cs" />

+    <Compile Include="cce.cs" />

+    <Compile Include="Rational.cs" />

+    <Compile Include="Set.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <Folder Include="Properties\" />

+  </ItemGroup>

+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+       Other similar extension points exist, see Microsoft.Common.targets.

+  <Target Name="BeforeBuild">

+  </Target>

+  <Target Name="AfterBuild">

+  </Target>

+  -->

+</Project>
\ No newline at end of file
diff --git a/Source/Basetypes/BigNum.cs b/Source/Basetypes/BigNum.cs
index 33ecf672..f5299f47 100644
--- a/Source/Basetypes/BigNum.cs
+++ b/Source/Basetypes/BigNum.cs
@@ -5,23 +5,24 @@
 //-----------------------------------------------------------------------------

 using System;

 using System.Text;

+using System.Diagnostics.Contracts;

 

 

 namespace Microsoft.Basetypes {

-  using Microsoft.Contracts;

   using BIM = System.Numerics.BigInteger;

-  

+

   /// <summary>

   /// A thin wrapper around System.Numerics.BigInteger

   /// (to be able to define equality, etc. properly)

   /// </summary>

   public struct BigNum {

-    

+

     // the internal representation

-    [Rep] internal readonly System.Numerics.BigInteger val;

-    public static readonly BigNum ZERO = new BigNum (BIM.Zero);

-    public static readonly BigNum ONE  = new BigNum (BIM.One);

-    public static readonly BigNum MINUS_ONE = new BigNum (-BIM.One);

+    [Rep]

+    internal readonly System.Numerics.BigInteger val;

+    public static readonly BigNum ZERO = new BigNum(BIM.Zero);

+    public static readonly BigNum ONE = new BigNum(BIM.One);

+    public static readonly BigNum MINUS_ONE = new BigNum(-BIM.One);

 

     [Pure]

     public static BigNum FromInt(int v) {

@@ -59,11 +60,11 @@ namespace Microsoft.Basetypes {
 

     public static bool TryParse(string v, out BigNum res) {

       try {

-	    res = BigNum.FromString(v);

+        res = BigNum.FromString(v);

         return true;

-	  } catch (FormatException) {

-	    res = ZERO;

-	    return false;

+      } catch (FormatException) {

+        res = ZERO;

+        return false;

       }

     }

 

@@ -77,46 +78,50 @@ namespace Microsoft.Basetypes {
     // Convert to int; assert that no overflows occur

     public int ToIntSafe {

       get {

-        assert this.InInt32;

+        Contract.Assert(this.InInt32);

         return this.ToInt;

       }

     }

 

     public Rational ToRational {

       get {

-        return new Rational (this, BigNum.ONE);

+        return new Rational(this, BigNum.ONE);

       }

-	}

+    }

 

     internal BigNum(System.Numerics.BigInteger val) {

       this.val = val;

     }

-    

-    public static bool operator==(BigNum x, BigNum y) {

+

+    public static bool operator ==(BigNum x, BigNum y) {

       return (x.val == y.val);

     }

 

-    public static bool operator!=(BigNum x, BigNum y) {

+    public static bool operator !=(BigNum x, BigNum y) {

       return !(x.val == y.val);

     }

 

-    [Pure][Reads(ReadsAttribute.Reads.Nothing)]

+    [Pure]

+    [Reads(ReadsAttribute.Reads.Nothing)]

     public override bool Equals(object obj) {

-      if (obj == null) return false;

-      if (!(obj is BigNum)) return false;

-      

+      if (obj == null)

+        return false;

+      if (!(obj is BigNum))

+        return false;

+

       BigNum other = (BigNum)obj;

       return (this.val == other.val);

     }

-    

+

     [Pure]

     public override int GetHashCode() {

       return this.val.GetHashCode();

     }

-    

+

     [Pure]

-    public override string! ToString() {

-      return (!)val.ToString();

+    public override string/*!*/ ToString() {

+      Contract.Ensures(Contract.Result<string>() != null);

+      return cce.NonNull(val.ToString());

     }

 

     //////////////////////////////////////////////////////////////////////////////

@@ -126,64 +131,75 @@ namespace Microsoft.Basetypes {
     // int32.ToString(format) does) 

 

     [Pure]

-	public string! ToString(string! format) {

-        if (format.StartsWith("d") || format.StartsWith("D")) {

-            string! res = this.Abs.ToString();

-			return addMinus(this.Signum,

-                            prefixWithZeros(extractPrecision(format), res));

-        } else if (format.StartsWith("x") || format.StartsWith("X")) {

-            string! res = this.toHex(format.Substring(0, 1));

-			return addMinus(this.Signum,

-                            prefixWithZeros(extractPrecision(format), res));

-        } else {

-			throw new FormatException("Format " + format + " is not supported");

-        }

-	}

+    public string/*!*/ ToString(string/*!*/ format) {

+      Contract.Requires(format != null);

+      Contract.Ensures(Contract.Result<string>() != null);

+      if (format.StartsWith("d") || format.StartsWith("D")) {

+        string res = this.Abs.ToString();

+        Contract.Assert(res != null);

+        return addMinus(this.Signum,

+                              prefixWithZeros(extractPrecision(format), res));

+      } else if (format.StartsWith("x") || format.StartsWith("X")) {

+        string res = this.toHex(format.Substring(0, 1));

+        Contract.Assert(res != null);

+        return addMinus(this.Signum,

+                              prefixWithZeros(extractPrecision(format), res));

+      } else {

+        throw new FormatException("Format " + format + " is not supported");

+      }

+    }

 

-    private static readonly System.Numerics.BigInteger BI_2_TO_24 = new BIM(0x1000000);
+    private static readonly System.Numerics.BigInteger BI_2_TO_24 = new BIM(0x1000000);

 

     [Pure]

-    private string! toHex(string! format) {

-	    string! res = "";

-        System.Numerics.BigInteger rem = this.Abs.val;

-

-        while (rem > BIM.Zero) {

-          res = ((int)(rem %BI_2_TO_24)).ToString(format) + res;

-          rem = rem / BI_2_TO_24;

-        }

+    private string/*!*/ toHex(string/*!*/ format) {

+      Contract.Requires(format != null);

+      Contract.Ensures(Contract.Result<string>() != null);

+      string res = "";

+      System.Numerics.BigInteger rem = this.Abs.val;

+

+      while (rem > BIM.Zero) {

+        res = ((int)(rem % BI_2_TO_24)).ToString(format) + res;

+        rem = rem / BI_2_TO_24;

+      }

 

-        return res;

+      return res;

     }

 

     [Pure]

-    private int extractPrecision(string! format) {

-        if (format.Length > 1)

-          // will throw a FormatException if the precision is invalid;

-          // that is ok

-          return Int32.Parse(format.Substring(1));

-        // always output at least one digit

-        return 1;

+    private int extractPrecision(string/*!*/ format) {

+      Contract.Requires(format != null);

+      if (format.Length > 1)

+        // will throw a FormatException if the precision is invalid;

+        // that is ok

+        return Int32.Parse(format.Substring(1));

+      // always output at least one digit

+      return 1;

     }

 

     [Pure]

-    private string! addMinus(int signum, string! suffix) {

-        if (signum < 0)

-          return "-" + suffix;

-        return suffix;

+    private string/*!*/ addMinus(int signum, string/*!*/ suffix) {

+      Contract.Requires(suffix != null);

+      Contract.Ensures(Contract.Result<string>() != null);

+      if (signum < 0)

+        return "-" + suffix;

+      return suffix;

     }

 

     [Pure]

-    private string! prefixWithZeros(int minLength, string! suffix) {

-        StringBuilder res = new StringBuilder();

-        while (res.Length + suffix.Length < minLength)

-          res.Append("0");

-        res.Append(suffix);

-        return res.ToString();

+    private string/*!*/ prefixWithZeros(int minLength, string/*!*/ suffix) {

+      Contract.Requires(suffix != null);

+      Contract.Ensures(Contract.Result<string>() != null);

+      StringBuilder res = new StringBuilder();

+      while (res.Length + suffix.Length < minLength)

+        res.Append("0");

+      res.Append(suffix);

+      return res.ToString();

     }

 

     ////////////////////////////////////////////////////////////////////////////

     // Basic arithmetic operations

-    

+

     public BigNum Abs {

       get {

         return new BigNum(BIM.Abs(this.val));

@@ -197,34 +213,34 @@ namespace Microsoft.Basetypes {
     }

 

     [Pure]

-    public static BigNum operator-(BigNum x) {

+    public static BigNum operator -(BigNum x) {

       return x.Neg;

     }

 

     [Pure]

-    public static BigNum operator+(BigNum x, BigNum y) {

+    public static BigNum operator +(BigNum x, BigNum y) {

       return new BigNum(x.val + y.val);

     }

 

     [Pure]

-    public static BigNum operator-(BigNum x, BigNum y) {

+    public static BigNum operator -(BigNum x, BigNum y) {

       return new BigNum(x.val - y.val);

     }

 

     [Pure]

-    public static BigNum operator*(BigNum x, BigNum y) {

+    public static BigNum operator *(BigNum x, BigNum y) {

       return new BigNum(x.val * y.val);

     }

 

     // TODO: check that this has a proper semantics (which? :-))

     [Pure]

-    public static BigNum operator/(BigNum x, BigNum y) {

+    public static BigNum operator /(BigNum x, BigNum y) {

       return new BigNum(x.val / y.val);

     }

 

     // TODO: check that this has a proper semantics (which? :-))

     [Pure]

-    public static BigNum operator%(BigNum x, BigNum y) {

+    public static BigNum operator %(BigNum x, BigNum y) {

       return new BigNum(x.val - ((x.val / y.val) * y.val));

     }

 

@@ -243,27 +259,20 @@ namespace Microsoft.Basetypes {
     /// </summary>

     /// <param name="_y"></param>

     /// <returns></returns>

-    public BigNum Gcd(BigNum _y)

-        ensures !result.IsNegative;

-    {

+    public BigNum Gcd(BigNum _y) {

+      Contract.Ensures(!Contract.Result<BigNum>().IsNegative);

       BigNum x = this.Abs;

       BigNum y = _y.Abs;

 

-      while (true)

-      {

-        if (x < y)

-        {

+      while (true) {

+        if (x < y) {

           y = y % x;

-          if (y.IsZero)

-          {

+          if (y.IsZero) {

             return x;

           }

-        }

-        else

-        {

+        } else {

           x = x % y;

-          if (x.IsZero)

-          {

+          if (x.IsZero) {

             return y;

           }

         }

@@ -275,9 +284,9 @@ namespace Microsoft.Basetypes {
     // Some basic comparison operations

 

     public int Signum {

-	  get {

-		return this.val.Sign;

-	  }

+      get {

+        return this.val.Sign;

+      }

     }

 

     public bool IsPositive {

@@ -300,37 +309,39 @@ namespace Microsoft.Basetypes {
 

     [Pure]

     public int CompareTo(BigNum that) {

-	  if (this.val == that.val) return 0;

-	  if (this.val < that.val) return -1;

-	  return 1;

+      if (this.val == that.val)

+        return 0;

+      if (this.val < that.val)

+        return -1;

+      return 1;

     }

 

     [Pure]

-    public static bool operator<(BigNum x, BigNum y) {

+    public static bool operator <(BigNum x, BigNum y) {

       return (x.val < y.val);

     }

 

     [Pure]

-    public static bool operator>(BigNum x, BigNum y) {

+    public static bool operator >(BigNum x, BigNum y) {

       return (x.val > y.val);

     }

 

     [Pure]

-    public static bool operator<=(BigNum x, BigNum y) {

+    public static bool operator <=(BigNum x, BigNum y) {

       return (x.val <= y.val);

     }

 

     [Pure]

-    public static bool operator>=(BigNum x, BigNum y) {

+    public static bool operator >=(BigNum x, BigNum y) {

       return (x.val >= y.val);

     }

 

-    

+

     private static readonly System.Numerics.BigInteger MaxInt32 =

       new BIM(Int32.MaxValue);

     private static readonly System.Numerics.BigInteger MinInt32 =

       new BIM(Int32.MinValue);

- 

+

     public bool InInt32 {

       get {

         return (val >= MinInt32) && (val <= MaxInt32);

diff --git a/Source/Basetypes/Rational.cs b/Source/Basetypes/Rational.cs
index ca87b223..609970a2 100644
--- a/Source/Basetypes/Rational.cs
+++ b/Source/Basetypes/Rational.cs
@@ -4,31 +4,30 @@
 //

 //-----------------------------------------------------------------------------

 using System;

-using Microsoft.Contracts;

+using System.Diagnostics.Contracts;

 

-namespace Microsoft.Basetypes

-{

+namespace Microsoft.Basetypes {

   using BNM = Microsoft.FSharp.Math.BigRational;

 

   /// <summary>

   /// The representation of a rational number.

   /// </summary>

-  public struct Rational 

-  {

-    public static readonly Rational ZERO = new Rational ((!)BNM.Zero);

-    public static readonly Rational ONE  = new Rational ((!)BNM.One);

-    public static readonly Rational MINUS_ONE = new Rational ((!)(-BNM.One));

+  public struct Rational {

+    public static readonly Rational ZERO = new Rational(cce.NonNull(BNM.Zero));

+    public static readonly Rational ONE = new Rational(cce.NonNull(BNM.One));

+    public static readonly Rational MINUS_ONE = new Rational(cce.NonNull(-BNM.One));

 

     private readonly Microsoft.FSharp.Math.BigRational _val;

 

-    private Microsoft.FSharp.Math.BigRational! val {

+    private Microsoft.FSharp.Math.BigRational val {

       get {

-        if (_val == null)

-          return (!)BNM.Zero;

+        Contract.Ensures(Contract.Result<FSharp.Math.BigRational>() != null);

+        if ((object)_val == null)

+          return cce.NonNull(BNM.Zero);

         else

           return _val;

       }

-	}

+    }

 

 

     //    int numerator;

@@ -39,8 +38,7 @@ namespace Microsoft.Basetypes
     // invariant: numerator != 0 ==> gcd(abs(numerator),denominator) == 1;

     // invariant: numerator == 0 ==> denominator == 1 || denominator == 0;

 

-    private Rational(int x)

-    {

+    private Rational(int x) {

       this._val = BNM.FromInt(x);

     }

 

@@ -48,13 +46,14 @@ namespace Microsoft.Basetypes
       return new Rational(x);

     }

 

-    private Rational(Microsoft.FSharp.Math.BigRational! val) {

+    private Rational(Microsoft.FSharp.Math.BigRational/*!*/ val) {

+      Contract.Requires(val != null);

       this._val = val;

     }

 

     public Rational(BigNum num, BigNum den) {

       System.Diagnostics.Debug.Assert(!den.IsZero);

-      

+

       this._val = BNM.FromBigInt(num.val) / BNM.FromBigInt(den.val);

     }

 

@@ -65,14 +64,13 @@ namespace Microsoft.Basetypes
     /// <summary>

     /// Returns the absolute value of the rational.

     /// </summary>

-    public Rational Abs()

-        ensures result.IsNonNegative;

-    {

-        if (IsNonNegative) {

-            return this;

-        } else {

-            return -this;

-        }

+    public Rational Abs() {

+      Contract.Ensures(Contract.Result<Rational>().IsNonNegative);

+      if (IsNonNegative) {

+        return this;

+      } else {

+        return -this;

+      }

     }

 

     /// <summary>

@@ -80,30 +78,27 @@ namespace Microsoft.Basetypes
     /// of the numerators and denominators of r and s.  If one of r and s is 0, the absolute

     /// value of the other is returned.  If both are 0, 1 is returned.

     /// </summary>

-    public static Rational Gcd(Rational r, Rational s)

-        ensures result.IsPositive;

-    {

-        if (r.IsZero) {

-            if (s.IsZero) {

-                return ONE;

-            } else {

-                return s.Abs();

-            }

-        } else if (s.IsZero) {

-            return r.Abs();

+    public static Rational Gcd(Rational r, Rational s) {

+      Contract.Ensures(Contract.Result<Rational>().IsPositive);

+      if (r.IsZero) {

+        if (s.IsZero) {

+          return ONE;

         } else {

-            return new Rational (r.Numerator.Gcd(s.Numerator),

-                                 r.Denominator.Gcd(s.Denominator));

+          return s.Abs();

         }

+      } else if (s.IsZero) {

+        return r.Abs();

+      } else {

+        return new Rational(r.Numerator.Gcd(s.Numerator),

+                             r.Denominator.Gcd(s.Denominator));

+      }

     }

-    

-    public BigNum Numerator

-    {

-      get

-      {

+

+    public BigNum Numerator {

+      get {

         // Better way to obtain the numerator?

         // The FSharp library does not seem to offer any methods for this

-        string! lin = (!)val.ToString();

+        string/*!*/ lin = cce.NonNull(val.ToString());

         int i = lin.IndexOf('/');

         if (i == -1)

           return new BigNum(BNM.ToBigInt(this.val));

@@ -112,188 +107,159 @@ namespace Microsoft.Basetypes
       }

     }

 

-    public BigNum Denominator

-    {

-      get

-      {

+    public BigNum Denominator {

+      get {

         // Better way to obtain the numerator?

         // The FSharp library does not seem to offer any methods for this

-        string! lin = (!)val.ToString();

+        string/*!*/ lin = cce.NonNull(val.ToString());

         int i = lin.IndexOf('/');

         if (i == -1)

           return BigNum.ONE;

         else

-          return BigNum.FromString(lin.Substring(i+1));

+          return BigNum.FromString(lin.Substring(i + 1));

       }

     }

 

-    public override string! ToString()

-    {

+    public override string/*!*/ ToString() {

+      Contract.Ensures(Contract.Result<string>() != null);

       return String.Format("{0}/{1}", Numerator, Denominator);

     }

 

 

-    public static bool operator==(Rational r, Rational s)

-    {

+    public static bool operator ==(Rational r, Rational s) {

       return (r.val == s.val);

     }

 

-    public static bool operator!=(Rational r, Rational s)

-    {

+    public static bool operator !=(Rational r, Rational s) {

       return !(r.val == s.val);

     }

 

-    public override bool Equals(object obj)

-    {

-      if (obj == null) return false;

+    public override bool Equals(object obj) {

+      if (obj == null)

+        return false;

       return obj is Rational && (Rational)obj == this;

     }

 

-    public override int GetHashCode()

-    {

+    public override int GetHashCode() {

       return this.val.GetHashCode();

     }

 

     public int Signum {

-      get { return this.val.Sign; }

+      get {

+        return this.val.Sign;

+      }

     }

 

-    public bool IsZero

-    {

-      get

-      {

+    public bool IsZero {

+      get {

         return Signum == 0;

       }

     }

 

-    public bool IsNonZero

-    {

-      get

-      {

+    public bool IsNonZero {

+      get {

         return Signum != 0;

       }

     }

 

-    public bool IsIntegral

-    {

-      get

-      {

+    public bool IsIntegral {

+      get {

         // better way?

-        return !((!)this.val.ToString()).Contains("/");

+        return !cce.NonNull(this.val.ToString()).Contains("/");

       }

     }

-    

-    

-    [Pure][Reads(ReadsAttribute.Reads.Nothing)]

-    public bool HasValue (int n) { return this == new Rational(n); }

+

+

+    [Pure]

+    [Reads(ReadsAttribute.Reads.Nothing)]

+    public bool HasValue(int n) {

+      return this == new Rational(n);

+    }

 

     /// <summary>

     /// Returns the rational as an integer.  Requires the rational to be integral.

     /// </summary>

-    public int AsInteger

-    {

-      get

-      {

+    public int AsInteger {

+      get {

         System.Diagnostics.Debug.Assert(this.IsIntegral);

         return Numerator.ToIntSafe;

       }

     }

 

     public BigNum AsBigNum {

-      get

-      {

+      get {

         System.Diagnostics.Debug.Assert(this.IsIntegral);

-        return new BigNum (BNM.ToBigInt(this.val));

+        return new BigNum(BNM.ToBigInt(this.val));

       }

     }

 

-    public double AsDouble

-    {

+    public double AsDouble {

       [Pure]

-      get

-      {

-        if (this.IsZero)

-        {

+      get {

+        if (this.IsZero) {

           return 0.0;

-        } 

-        else

-        {

+        } else {

           return (double)Numerator.ToIntSafe / (double)Denominator.ToIntSafe;

         }

       }

     }

 

-    public bool IsNegative

-    {

+    public bool IsNegative {

       [Pure]

-      get

-      {

+      get {

         return Signum < 0;

       }

     }

 

-    public bool IsPositive

-    {

+    public bool IsPositive {

       [Pure]

-      get

-      {

+      get {

         return 0 < Signum;

       }

     }

 

-    public bool IsNonNegative

-    {

+    public bool IsNonNegative {

       [Pure]

-      get

-      {

+      get {

         return 0 <= Signum;

       }

     }

 

 

-    public static Rational operator-(Rational r)

-    {

-      return new Rational ((!)(BNM.Zero -r.val)); // for whatever reason, the Spec# compiler refuses to accept -r.val (unary negation)

+    public static Rational operator -(Rational r) {

+      return new Rational(cce.NonNull(BNM.Zero - r.val)); // for whatever reason, the Spec# compiler refuses to accept -r.val (unary negation)

     }

 

 

-    public static Rational operator+(Rational r, Rational s)

-    {

-      return new Rational ((!)(r.val + s.val));

+    public static Rational operator +(Rational r, Rational s) {

+      return new Rational(cce.NonNull(r.val + s.val));

     }

 

-    public static Rational operator-(Rational r, Rational s)

-    {

-      return new Rational ((!)(r.val - s.val));

+    public static Rational operator -(Rational r, Rational s) {

+      return new Rational(cce.NonNull((r.val - s.val)));

     }

 

-    public static Rational operator*(Rational r, Rational s)

-    {

-      return new Rational ((!)(r.val * s.val));

+    public static Rational operator *(Rational r, Rational s) {

+      return new Rational(cce.NonNull(r.val * s.val));

     }

 

-    public static Rational operator/(Rational r, Rational s)

-    {

-      return new Rational ((!)(r.val / s.val));

+    public static Rational operator /(Rational r, Rational s) {

+      return new Rational(cce.NonNull(r.val / s.val));

     }

 

-    public static bool operator<=(Rational r, Rational s)

-    {

+    public static bool operator <=(Rational r, Rational s) {

       return (r.val <= s.val);

     }

 

-    public static bool operator>=(Rational r, Rational s)

-    {

+    public static bool operator >=(Rational r, Rational s) {

       return (r.val >= s.val);

     }

 

-    public static bool operator<(Rational r, Rational s)

-    {

+    public static bool operator <(Rational r, Rational s) {

       return (r.val < s.val);

     }

 

-    public static bool operator>(Rational r, Rational s)

-    {

+    public static bool operator >(Rational r, Rational s) {

       return (r.val > s.val);

     }

   }

diff --git a/Source/Basetypes/Set.cs b/Source/Basetypes/Set.cs
index 9286d6f5..e31e5399 100644
--- a/Source/Basetypes/Set.cs
+++ b/Source/Basetypes/Set.cs
@@ -3,280 +3,270 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

-namespace Microsoft.Boogie

-{

-    using System;

-    using System.IO;

-    using System.Collections;

-    using Microsoft.Contracts;

+namespace Microsoft.Boogie {

+  using System;

+  using System.IO;

+  using System.Collections;

+  using System.Diagnostics.Contracts;

+

+  /// <summary>

+  /// A class representing a mathematical set.

+  /// </summary>

+  public class Set : ICloneable, IEnumerable {

+    /*[Own]*/

+    Hashtable ht;

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(ht != null);

+    }

+

+

+    public Set() {

+      ht = new Hashtable();

+      //:base();

+    }

+

+    private Set(Hashtable/*!*/ ht) {

+      Contract.Requires(ht != null);

+      this.ht = ht;

+      //:base();

+    }

+

+    public Set(int capacity) {

+      ht = new Hashtable(capacity);

+      //:base();

+    }

+

+

+    public readonly static Set/*!*/ Empty = new Set();

+

+    public void Clear() {

+      ht.Clear();

+    }

 

     /// <summary>

-    /// A class representing a mathematical set.

+    /// This method idempotently adds "o" to the set.

+    /// In notation:

+    ///   this.SetElements =  this.SetElements_old \union {o};

     /// </summary>

-    public class Set : ICloneable, IEnumerable 

-    {

-        /*[Own]*/ Hashtable! ht;

-

-        public Set() 

-        {

-            ht = new Hashtable();

-            base();

-        }

+    public void Add(object/*!*/ o) {

+      Contract.Requires(o != null);

+      ht[o] = o;

+    }

 

-        private Set(Hashtable! ht) 

-        {

-            this.ht = ht;

-            base();

-        }

+    /// <summary>

+    /// this.SetElements =  this.SetElements_old \union s.SetElements;

+    /// </summary>

+    public void AddRange(Set/*!*/ s) {

+      Contract.Requires(s != null);

+      foreach (object/*!*/ o in s) {

+        Contract.Assert(o != null);

+        Add(o);

+      }

+    }

 

-        public Set(int capacity) 

-        {

-            ht = new Hashtable(capacity);

-            base();

-        }

-        

-        

-        public readonly static Set! Empty = new Set();

+    /// <summary>

+    /// this.SetElements =  this.SetElements_old \setminus {o};

+    /// </summary>

+    public void Remove(object/*!*/ o) {

+      Contract.Requires(o != null);

+      ht.Remove(o);

+    }

 

-        public void Clear() 

-        {

-            ht.Clear();

+    /// <summary>

+    /// this.SetElements =  this.SetElements_old \setminus s.SetElements;

+    /// </summary>

+    public void RemoveRange(Set/*!*/ s) {

+      Contract.Requires(s != null);

+      if (s == this) {

+        ht.Clear();

+      } else {

+        foreach (object/*!*/ o in s) {

+          Contract.Assert(o != null);

+          ht.Remove(o);

         }

+      }

+    }

 

-        /// <summary>

-        /// This method idempotently adds "o" to the set.

-        /// In notation:

-        ///   this.SetElements =  this.SetElements_old \union {o};

-        /// </summary>

-        public void Add(object! o) 

-        {

-            ht[o] = o;

-        }

+    /// <summary>

+    /// Returns an arbitrary element from the set.

+    /// </summary>

+    public object/*!*/ Choose() {

+      Contract.Requires((Count > 0));

+      Contract.Ensures(Contract.Result<object>() != null);

+      IEnumerator iter = GetEnumerator();

+      iter.MoveNext();

+      return cce.NonNull(iter.Current);

+    }

 

-        /// <summary>

-        /// this.SetElements =  this.SetElements_old \union s.SetElements;

-        /// </summary>

-        public void AddRange(Set! s) 

-        {

-            foreach (object! o in s) 

-            {

-                Add(o);

-            }

-        }

+    /// <summary>

+    /// Picks an arbitrary element from the set, removes it, and returns it.

+    /// </summary>

+    public object/*!*/ Take() {

+      Contract.Requires((Count > 0));

+      Contract.Ensures(Contract.Result<object>() != null);

+      Contract.Ensures(Count == Contract.OldValue(Count) - 1);

+      object r = Choose();

+      Remove(r);

+      return r;

+    }

 

-        /// <summary>

-        /// this.SetElements =  this.SetElements_old \setminus {o};

-        /// </summary>

-        public void Remove(object! o) 

-        {

-            ht.Remove(o);

+    public void Intersect(Set/*!*/ s) {

+      Contract.Requires(s != null);

+      Hashtable h = new Hashtable(ht.Count);

+      foreach (object/*!*/ key in ht.Keys) {

+        Contract.Assert(key != null);

+        if (s.ht.ContainsKey(key)) {

+          h.Add(key, key);

         }

+      }

+      ht = h;

+    }

 

-        /// <summary>

-        /// this.SetElements =  this.SetElements_old \setminus s.SetElements;

-        /// </summary>

-        public void RemoveRange(Set! s) 

-        {

-            if (s == this) 

-            {

-                ht.Clear();

-            } 

-            else 

-            {

-                foreach (object! o in s) 

-                {

-                    ht.Remove(o);

-                }

-            }

-        }

-        

-        /// <summary>

-        /// Returns an arbitrary element from the set.

-        /// </summary>

-        public object! Choose()

-          requires Count > 0;

-        {

-            IEnumerator iter = GetEnumerator();

-            iter.MoveNext();

-            return (!)iter.Current;

-        }

-        

-        /// <summary>

-        /// Picks an arbitrary element from the set, removes it, and returns it.

-        /// </summary>

-        public object! Take()

-          requires Count > 0;

-          ensures Count == old(Count) - 1;

-        {

-            object r = Choose();

-            Remove(r);

-            return r;

+    /// <summary>

+    /// The getter returns true iff "o" is in the set.

+    /// The setter adds the value "o" (for "true") or removes "o" (for "false")

+    /// </summary>

+    public bool this[object/*!*/ o] {

+      get {

+        Contract.Requires(o != null);

+        return ht.ContainsKey(o);

+      }

+      set {

+        if (value) {

+          Add(o);

+        } else {

+          Remove(o);

         }

+      }

+    }

 

-        public void Intersect(Set! s) 

-        {

-            Hashtable h = new Hashtable(ht.Count);

-            foreach (object! key in ht.Keys) 

-            {

-                if (s.ht.ContainsKey(key)) 

-                {

-                    h.Add(key, key);

-                }

-            }

-            ht = h;

-        }

-        

-        /// <summary>

-        /// The getter returns true iff "o" is in the set.

-        /// The setter adds the value "o" (for "true") or removes "o" (for "false")

-        /// </summary>

-        public bool this[object! o] 

-        {

-            get 

-            {

-                return ht.ContainsKey(o);

-            }

-            set

-            {

-                if (value) {

-                    Add(o);

-                } else {

-                    Remove(o);

-                }

-            }

-        }

+    /// <summary>

+    /// Returns true iff "o" is an element of "this".

+    /// </summary>

+    /// <param name="o"></param>

+    /// <returns></returns>

+    [Pure]

+    public bool Contains(object/*!*/ o) {

+      Contract.Requires(o != null);

+      if (!this.ht.ContainsKey(o)) {

+        return false;

+      }

+      return true;

+    }

 

-        /// <summary>

-        /// Returns true iff "o" is an element of "this".

-        /// </summary>

-        /// <param name="o"></param>

-        /// <returns></returns>

-        [Pure]

-        public bool Contains(object! o) 

-        {

-          if (!this.ht.ContainsKey(o)) 

-          {

+    /// <summary>

+    /// Returns true iff every element of "s" is an element of "this", that is, if

+    /// "s" is a subset of "this".

+    /// </summary>

+    /// <param name="s"></param>

+    /// <returns></returns>

+    public bool ContainsRange(Set/*!*/ s) {

+      Contract.Requires(s != null);

+      if (s != this) {

+        foreach (object/*!*/ key in s.ht.Keys) {

+          Contract.Assert(key != null);

+          if (!this.ht.ContainsKey(key)) {

             return false;

-          }            

-          return true;

+          }

         }

+      }

+      return true;

+    }

 

-        /// <summary>

-        /// Returns true iff every element of "s" is an element of "this", that is, if

-        /// "s" is a subset of "this".

-        /// </summary>

-        /// <param name="s"></param>

-        /// <returns></returns>

-        public bool ContainsRange(Set! s) 

-        {

-            if (s != this) 

-            {

-                foreach (object! key in s.ht.Keys) 

-                {

-                    if (!this.ht.ContainsKey(key)) 

-                    {

-                        return false;

-                    }

-                }

-            }

-            return true;

-        }

+    public object/*!*/ Clone() {

+      Contract.Ensures(Contract.Result<object>() != null);

+      return new Set((Hashtable/*!*/)cce.NonNull(ht.Clone()));

+    }

 

-        public object! Clone() 

-        {

-            return new Set((Hashtable!)ht.Clone());

-        }

+    public virtual int Count {

+      get {

+        return ht.Count;

+      }

+    }

 

-        public virtual int Count 

-        {

-            get 

-            {

-                return ht.Count;

-            }

-        }

+    [Pure]

+    public IEnumerator/*!*/ GetEnumerator() {

+      Contract.Ensures(Contract.Result<IEnumerator>() != null);

+      return ht.Keys.GetEnumerator();

+    }

 

-        [Pure]

-        public IEnumerator! GetEnumerator() 

-        {

-            return ht.Keys.GetEnumerator();

+    [Pure]

+    public override string/*!*/ ToString() {

+      Contract.Ensures(Contract.Result<string>() != null);

+      string s = null;

+      foreach (object/*!*/ key in ht.Keys) {

+        Contract.Assert(key != null);

+        if (s == null) {

+          s = "{";

+        } else {

+          s += ", ";

         }

+        s += key.ToString();

+      }

+      if (s == null) {

+        return "{}";

+      } else {

+        return s + "}";

+      }

+    }

 

-        [Pure]

-        public override string! ToString() 

-        {

-            string s = null;

-            foreach (object! key in ht.Keys) 

-            {

-                if (s == null) 

-                {

-                    s = "{";

-                } 

-                else 

-                {

-                    s += ", ";

-                }

-                s += key.ToString();

-            }

-            if (s == null) 

-            {

-                return "{}";

-            } 

-            else 

-            {

-                return s + "}";

-            }

-        }

-        

-         public bool AddAll(IEnumerable! objs){

-          foreach (object! o in objs){

-            this.Add(o);

-          }

-          return true;

-        }

-       //----------------------------- Static Methods ---------------------------------

-        

-        // Functional Intersect

-        public static Set! Intersect(Set! a, Set! b) 

-        //  ensures Forall{ object x in result; a[x] && b[x] };

-        {

-            Set! res = (Set!) a.Clone();

-            res.Intersect(b);

-            return res;

-        }

-        // Functional Union

-        public static Set! Union(Set! a, Set! b) 

-        //  ensures Forall{ object x in result; a[x] || b[x] };

-        {

-            Set! res = (Set!) a.Clone();

-            res.AddRange(b);

-            return res;

-        }

- 

-       public delegate bool SetFilter(object! obj);

+    public bool AddAll(IEnumerable/*!*/ objs) {

+      Contract.Requires(objs != null);

+      foreach (object/*!*/ o in objs) {

+        Contract.Assert(o != null);

+        this.Add(o);

+      }

+      return true;

+    }

+    //----------------------------- Static Methods ---------------------------------

+

+    // Functional Intersect

+    public static Set/*!*/ Intersect(Set/*!*/ a, Set/*!*/ b) {

+      Contract.Requires(b != null);

+      Contract.Requires(a != null);

+      Contract.Ensures(Contract.Result<Set>() != null);

+      //Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] ));

+      Set/*!*/ res = (Set/*!*/)cce.NonNull(a.Clone());

+      res.Intersect(b);

+      return res;

+    }

+    // Functional Union

+    public static Set/*!*/ Union(Set/*!*/ a, Set/*!*/ b) {

+      Contract.Requires(a != null);

+      Contract.Requires(b != null);

+      Contract.Ensures(Contract.Result<Set>() != null);

+      //  Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] ));

+      Set/*!*/ res = (Set/*!*/)cce.NonNull(a.Clone());

+      res.AddRange(b);

+      return res;

+    }

+

+    public delegate bool SetFilter(object/*!*/ obj);

 

-       public static Set! Filter(Set! a, SetFilter! filter) 

-       {

-         Set inter = new Set();

+    public static Set/*!*/ Filter(Set/*!*/ a, SetFilter/*!*/ filter) {

+      Contract.Requires(filter != null);

+      Contract.Requires(a != null);

+      Contract.Ensures(Contract.Result<Set>() != null);

+      Set inter = new Set();

 

-         foreach(object! elem in a) 

-         {

-           if (filter(elem))

-           {

-             inter.Add(elem);

-           }

-         }	

-         return inter;

-       }

+      foreach (object/*!*/ elem in a) {

+        Contract.Assert(elem != null);

+        if (filter(elem)) {

+          inter.Add(elem);

+        }

+      }

+      return inter;

+    }

 

   }

- 

-   public interface IWorkList: ICollection

-  {

+

+  public interface IWorkList : ICollection {

     bool Add(object o);

     bool AddAll(IEnumerable objs);

     bool IsEmpty();

     object Pull();

   }

-   

+

 

 }
\ No newline at end of file