merge

13 files changed, 101 insertions, 149 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 5e69b179..e7c1fb77 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -385,7 +385,7 @@ namespace Microsoft.Boogie {
 

       Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToInputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();

       Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToOutputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();

-      Dictionary<Block/*!*/, Hashtable/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Hashtable/*!*/>();

+      Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>();

       Dictionary<Block/*!*/, LoopProcedure/*!*/>/*!*/ loopHeaderToLoopProc = new Dictionary<Block/*!*/, LoopProcedure/*!*/>();

       Dictionary<Block/*!*/, CallCmd/*!*/>/*!*/ loopHeaderToCallCmd1 = new Dictionary<Block/*!*/, CallCmd/*!*/>();

       Dictionary<Block, CallCmd> loopHeaderToCallCmd2 = new Dictionary<Block, CallCmd>();

@@ -402,7 +402,7 @@ namespace Microsoft.Boogie {
         IdentifierExprSeq callOutputs2 = new IdentifierExprSeq();

         List<AssignLhs> lhss = new List<AssignLhs>();

         List<Expr> rhss = new List<Expr>();

-        Hashtable substMap = new Hashtable(); // Variable -> IdentifierExpr

+        Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>(); // Variable -> IdentifierExpr

 

         VariableSeq/*!*/ targets = new VariableSeq();

         HashSet<Variable> footprint = new HashSet<Variable>();

@@ -2359,9 +2359,9 @@ namespace Microsoft.Boogie {
   }

 

   public class Procedure : DeclWithFormals {

-    public RequiresSeq/*!*/ Requires;

+    public List<Requires>/*!*/ Requires;

     public IdentifierExprSeq/*!*/ Modifies;

-    public EnsuresSeq/*!*/ Ensures;

+    public List<Ensures>/*!*/ Ensures;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Requires != null);

@@ -2376,7 +2376,7 @@ namespace Microsoft.Boogie {
     public readonly ProcedureSummary/*!*/ Summary;

 

     public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams,

-      RequiresSeq/*!*/ requires, IdentifierExprSeq/*!*/ modifies, EnsuresSeq/*!*/ ensures)

+      List<Requires>/*!*/ requires, IdentifierExprSeq/*!*/ modifies, List<Ensures>/*!*/ ensures)

       : this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -2390,7 +2390,7 @@ namespace Microsoft.Boogie {
     }

 

     public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams,

-      RequiresSeq/*!*/ @requires, IdentifierExprSeq/*!*/ @modifies, EnsuresSeq/*!*/ @ensures, QKeyValue kv

+      List<Requires>/*!*/ @requires, IdentifierExprSeq/*!*/ @modifies, List<Ensures>/*!*/ @ensures, QKeyValue kv

       )

       : base(tok, name, typeParams, inParams, outParams) {

       Contract.Requires(tok != null);

@@ -2531,7 +2531,7 @@ namespace Microsoft.Boogie {
                            VariableSeq inputs, VariableSeq outputs, IdentifierExprSeq globalMods)

           : base(Token.NoToken, impl.Name + "_loop_" + header.ToString(),

                new TypeVariableSeq(), inputs, outputs,

-               new RequiresSeq(), globalMods, new EnsuresSeq())

+               new List<Requires>(), globalMods, new List<Ensures>())

       {

           enclosingImpl = impl;

       }

@@ -2914,17 +2914,17 @@ namespace Microsoft.Boogie {
       }

     }

 

-    private Hashtable/*Variable->Expr*//*?*/ formalMap = null;

+    private Dictionary<Variable, Expr>/*?*/ formalMap = null;

     public void ResetImplFormalMap() {

       this.formalMap = null;

     }

-    public Hashtable /*Variable->Expr*//*!*/ GetImplFormalMap() {

+    public Dictionary<Variable, Expr>/*!*/ GetImplFormalMap() {

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

 

       if (this.formalMap != null)

         return this.formalMap;

       else {

-        Hashtable /*Variable->Expr*//*!*/ map = new Hashtable /*Variable->Expr*/ (InParams.Length + OutParams.Length);

+        Dictionary<Variable, Expr>/*!*/ map = new Dictionary<Variable, Expr> (InParams.Length + OutParams.Length);

 

         Contract.Assume(this.Proc != null);

         Contract.Assume(InParams.Length == Proc.InParams.Length);

@@ -2948,7 +2948,7 @@ namespace Microsoft.Boogie {
         if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

           Console.WriteLine("Implementation.GetImplFormalMap on {0}:", this.Name);

           using (TokenTextWriter stream = new TokenTextWriter("<console>", Console.Out, false)) {

-            foreach (DictionaryEntry e in map) {

+            foreach (var e in map) {

               Console.Write("  ");

               cce.NonNull((Variable/*!*/)e.Key).Emit(stream, 0);

               Console.Write("  --> ");

@@ -3224,39 +3224,6 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class RequiresSeq : PureCollections.Sequence {

-    public RequiresSeq(params Requires[]/*!*/ args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public new Requires/*!*/ this[int index] {

-      get {

-        Contract.Ensures(Contract.Result<Requires>() != null);

-

-        return cce.NonNull((Requires/*!*/)base[index]);

-      }

-      set {

-        base[index] = value;

-      }

-    }

-  }

-

-  public sealed class EnsuresSeq : PureCollections.Sequence {

-    public EnsuresSeq(params Ensures[]/*!*/ args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public new Ensures/*!*/ this[int index] {

-      get {

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

-        return cce.NonNull((Ensures/*!*/)base[index]);

-      }

-      set {

-        base[index] = value;

-      }

-    }

-  }

-

   public sealed class VariableSeq : List<Variable> {

     public VariableSeq(params Variable[]/*!*/ args)

       : base(args) {

@@ -3266,14 +3233,6 @@ namespace Microsoft.Boogie {
       : base(varSeq) {

       Contract.Requires(varSeq != null);

     }

-    public new Variable this[int index] {

-      get {

-        return (Variable)base[index];

-      }

-      set {

-        base[index] = value;

-      }

-    }

     public void Emit(TokenTextWriter stream, bool emitAttributes) {

       Contract.Requires(stream != null);

       string sep = "";

@@ -3303,7 +3262,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class TypeSeq : PureCollections.Sequence {

+  public sealed class TypeSeq : List<Type> {

     public TypeSeq(params Type[]/*!*/ args)

       : base(args) {

       Contract.Requires(args != null);

@@ -3312,19 +3271,9 @@ namespace Microsoft.Boogie {
       : base(varSeq) {

       Contract.Requires(varSeq != null);

     }

-    public new Type/*!*/ this[int index] {

-      get {

-        Contract.Ensures(Contract.Result<Type>() != null);

-

-        return cce.NonNull((Type/*!*/)base[index]);

-      }

-      set {

-        base[index] = value;

-      }

-    }

     public List<Type/*!*/>/*!*/ ToList() {

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));

-      List<Type/*!*/>/*!*/ res = new List<Type/*!*/>(Length);

+      List<Type/*!*/>/*!*/ res = new List<Type/*!*/>(Count);

       foreach (Type/*!*/ t in this) {

         Contract.Assert(t != null);

         res.Add(t);

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 3005aaa6..47f5505e 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2040,9 +2040,9 @@ namespace Microsoft.Boogie {
     protected override Cmd ComputeDesugaring() {

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

       CmdSeq newBlockBody = new CmdSeq();

-      Hashtable /*Variable -> Expr*/ substMap = new Hashtable/*Variable -> Expr*/();

-      Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/();

-      Hashtable /*Variable -> Expr*/ substMapBound = new Hashtable/*Variable -> Expr*/();

+      Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();

+      Dictionary<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>();

+      Dictionary<Variable, Expr> substMapBound = new Dictionary<Variable, Expr>();

       VariableSeq/*!*/ tempVars = new VariableSeq();

 

       // proc P(ins) returns (outs)

@@ -2113,7 +2113,7 @@ namespace Microsoft.Boogie {
       Substitution s = Substituter.SubstitutionFromHashtable(substMapBound);

       bool hasWildcard = (wildcardVars.Length != 0);

       Expr preConjunction = null;

-      for (int i = 0; i < this.Proc.Requires.Length; i++) {

+      for (int i = 0; i < this.Proc.Requires.Count; i++) {

         Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);

         if (!req.Free && !IsFree) {

           if (hasWildcard) {

@@ -2149,7 +2149,7 @@ namespace Microsoft.Boogie {
       #region assume Pre[ins := cins] with formal paramters

       if (hasWildcard) {

         s = Substituter.SubstitutionFromHashtable(substMap);

-        for (int i = 0; i < this.Proc.Requires.Length; i++) {

+        for (int i = 0; i < this.Proc.Requires.Count; i++) {

           Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);

           if (!req.Free) {

             Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());

@@ -2335,7 +2335,7 @@ namespace Microsoft.Boogie {
 

   public class AssertCmd : PredicateCmd, IPotentialErrorNode {

     public Expr OrigExpr;

-    public Hashtable /*Variable -> Expr*/ IncarnationMap;

+    public Dictionary<Variable, Expr> IncarnationMap;

 

     // TODO: convert to use generics

     private object errorData;

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 14534929..24622d8b 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1817,7 +1817,7 @@ namespace Microsoft.Boogie {
         tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

         return null;

       } else {

-        Contract.Assert(actualResultType.Length == 1);

+        Contract.Assert(actualResultType.Count == 1);

         tpInstantiation =

           SimpleTypeParamInstantiation.From(Func.TypeParameters, resultingTypeArgs);

         return actualResultType[0];

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 8c355f72..81d44756 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -447,9 +447,9 @@ namespace Microsoft.Boogie {
       Contract.Requires(actualArgs != null);

       Contract.Requires(opName != null);

       Contract.Requires(tc != null);

-      Contract.Requires(formalArgs.Length == actualArgs.Length);

+      Contract.Requires(formalArgs.Count == actualArgs.Length);

       Contract.Requires((formalOuts == null) == (actualOuts == null));

-      Contract.Requires(formalOuts == null || formalOuts.Length == cce.NonNull(actualOuts).Length);

+      Contract.Requires(formalOuts == null || formalOuts.Count == cce.NonNull(actualOuts).Length);

       Contract.Requires(tc == null || opName != null);//Redundant

       Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));

 

@@ -462,7 +462,7 @@ namespace Microsoft.Boogie {
         subst.Add(tv, proxy);

       }

 

-      for (int i = 0; i < formalArgs.Length; i++) {

+      for (int i = 0; i < formalArgs.Count; i++) {

         Type formal = formalArgs[i].Substitute(subst);

         Type actual = cce.NonNull(cce.NonNull(actualArgs[i]).Type);

         // if the type variables to be matched occur in the actual

@@ -479,7 +479,7 @@ namespace Microsoft.Boogie {
       }

 

       if (formalOuts != null) {

-        for (int i = 0; i < formalOuts.Length; ++i) {

+        for (int i = 0; i < formalOuts.Count; ++i) {

           Type formal = formalOuts[i].Substitute(subst);

           Type actual = cce.NonNull(cce.NonNull(actualOuts)[i].Type);

           // if the type variables to be matched occur in the actual

@@ -524,13 +524,13 @@ namespace Microsoft.Boogie {
       Contract.Requires(opName != null);Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out actualTypeParams)));

       actualTypeParams = new List<Type/*!*/>();

 

-      if (formalIns.Length != actualIns.Length) {

+      if (formalIns.Count != actualIns.Length) {

         tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1}",

                  opName, actualIns.Length);

         // if there are no type parameters, we can still return the result

         // type and hope that the type checking proceeds

         return typeParams.Length == 0 ? formalOuts : null;

-      } else if (actualOuts != null && formalOuts.Length != actualOuts.Length) {

+      } else if (actualOuts != null && formalOuts.Count != actualOuts.Length) {

         tc.Error(typeCheckingSubject, "wrong number of result variables in {0}: {1}",

                  opName, actualOuts.Length);

         // if there are no type parameters, we can still return the result

@@ -638,7 +638,7 @@ namespace Microsoft.Boogie {
                                       TypeSeq/*!*/ actualArgs) {

       Contract.Requires(typeParams != null);

       Contract.Requires(formalArgs != null);

-      Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Length == actualArgs.Length);

+      Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Count == actualArgs.Count);

       Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));

 

       

@@ -651,7 +651,7 @@ namespace Microsoft.Boogie {
         subst.Add(tv, proxy);

       }

 

-      for (int i = 0; i < formalArgs.Length; i++) {

+      for (int i = 0; i < formalArgs.Count; i++) {

         Type formal = formalArgs[i].Substitute(subst);

         Type actual = actualArgs[i];

         // if the type variables to be matched occur in the actual

@@ -1296,7 +1296,7 @@ Contract.Requires(that != null);
           }

         }

         if (is_bv) {

-          if (Arguments.Length > 0) {

+          if (Arguments.Count > 0) {

             rc.Error(this,

                      "bitvector types must not be applied to arguments: {0}",

                      Name);

@@ -1308,7 +1308,7 @@ Contract.Requires(that != null);
       // second case: the identifier is resolved to a type variable

       TypeVariable var = rc.LookUpTypeBinder(Name);

       if (var != null) {

-        if (Arguments.Length > 0) {

+        if (Arguments.Count > 0) {

           rc.Error(this,

                    "type variables must not be applied to arguments: {0}",

                    var);

@@ -1320,7 +1320,7 @@ Contract.Requires(that != null);
       // recursively resolve the arguments

       TypeCtorDecl ctorDecl = rc.LookUpType(Name);

       if (ctorDecl != null) {

-        if (Arguments.Length != ctorDecl.Arity) {

+        if (Arguments.Count != ctorDecl.Arity) {

           rc.Error(this,

                    "type constructor received wrong number of arguments: {0}",

                    ctorDecl);

@@ -1332,7 +1332,7 @@ Contract.Requires(that != null);
       // fourth case: the identifier denotes a type synonym

       TypeSynonymDecl synDecl = rc.LookUpTypeSynonym(Name);

       if (synDecl != null) {

-        if (Arguments.Length != synDecl.TypeParameters.Length) {

+        if (Arguments.Count != synDecl.TypeParameters.Length) {

           rc.Error(this,

                    "type synonym received wrong number of arguments: {0}",

                    synDecl);

@@ -2304,7 +2304,7 @@ Contract.Requires(that != null);
         Contract.Requires(unifiableVariables != null);

         Contract.Requires(cce.NonNullDictionaryAndValues(result));

         Contract.Requires(that != null);

-        Contract.Requires(Arguments.Length == that.Arguments.Length);

+        Contract.Requires(Arguments.Count == that.Arguments.Count);

         Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();

         foreach (TypeVariable/*!*/ tv in that.TypeParameters) {

           Contract.Assert(tv != null);

@@ -2313,7 +2313,7 @@ Contract.Requires(that != null);
         }

 

         bool good = true;

-        for (int i = 0; i < that.Arguments.Length; i++) {

+        for (int i = 0; i < that.Arguments.Count; i++) {

           Type t0 = that.Arguments[i].Substitute(subst);

           Type t1 = this.Arguments[i];

           good &= t0.Unify(t1, unifiableVariables, result);

@@ -2332,7 +2332,7 @@ Contract.Requires(that != null);
     }

 

     private void AddConstraint(Constraint c) {

-      Contract.Requires(c.Arguments.Length == Arity);

+      Contract.Requires(c.Arguments.Count == Arity);

 

       Type f = ProxyFor;

       MapType mf = f as MapType;

@@ -2462,7 +2462,7 @@ Contract.Requires(that != null);
         return true;

       } else if (that is MapType) {

         MapType mapType = (MapType)that;

-        if (mapType.Arguments.Length == Arity) {

+        if (mapType.Arguments.Count == Arity) {

           bool good = true;

           foreach (Constraint c in constraints)

             good &= c.Unify(mapType, unifiableVariables, result);

@@ -2500,7 +2500,7 @@ Contract.Requires(that != null);
         // of the substituted variables (otherwise, we are in big trouble)

         Contract.Assert(Contract.ForAll(constraints, c =>

                Contract.ForAll(subst.Keys, var =>

-               Contract.ForAll(0, c.Arguments.Length, t => !c.Arguments[t].FreeVariables.Has(var)) &&

+               Contract.ForAll(0, c.Arguments.Count, t => !c.Arguments[t].FreeVariables.Has(var)) &&

                      !c.Result.FreeVariables.Has(var))));

       }

       return base.Substitute(subst);

@@ -2566,7 +2566,7 @@ Contract.Requires(that != null);
       Contract.Requires(token != null);

       Contract.Requires(decl != null);

       Contract.Requires(arguments != null);

-      Contract.Requires(arguments.Length == decl.TypeParameters.Length);

+      Contract.Requires(arguments.Count == decl.TypeParameters.Length);

       this.Decl = decl;

       this.Arguments = arguments;

 

@@ -2574,7 +2574,7 @@ Contract.Requires(that != null);
       // the type synonym

       IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst =

         new Dictionary<TypeVariable/*!*/, Type/*!*/>();

-      for (int i = 0; i < arguments.Length; ++i)

+      for (int i = 0; i < arguments.Count; ++i)

         subst.Add(decl.TypeParameters[i], arguments[i]);

 

       ExpandedType = decl.Body.Substitute(subst);

@@ -2830,7 +2830,7 @@ Contract.Requires(that != null);
       Contract.Requires(token != null);

       Contract.Requires(decl != null);

       Contract.Requires(arguments != null);

-      Contract.Requires(arguments.Length == decl.Arity);

+      Contract.Requires(arguments.Count == decl.Arity);

       this.Decl = decl;

       this.Arguments = arguments;

     }

@@ -2878,7 +2878,7 @@ Contract.Requires(that != null);
       CtorType thatCtorType = thatType as CtorType;

       if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl))

         return false;

-      if (Arguments.Length == 0)

+      if (Arguments.Count == 0)

         return true;

       return base.Equals(thatType);

     }

@@ -2891,7 +2891,7 @@ Contract.Requires(that != null);
       CtorType thatCtorType = that as CtorType;

       if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl))

         return false;

-      for (int i = 0; i < Arguments.Length; ++i) {

+      for (int i = 0; i < Arguments.Count; ++i) {

         if (!Arguments[i].Equals(thatCtorType.Arguments[i],

                                  thisBoundVariables, thatBoundVariables))

           return false;

@@ -2913,7 +2913,7 @@ Contract.Requires(that != null);
         return false;

       } else {

         bool good = true;

-        for (int i = 0; i < Arguments.Length; ++i)

+        for (int i = 0; i < Arguments.Count; ++i)

           good &= Arguments[i].Unify(thatCtorType.Arguments[i], unifiableVariables, result);

         return good;

       }

@@ -2982,12 +2982,12 @@ Contract.Requires(that != null);
       Contract.Requires(stream != null);

       Contract.Requires(args != null);

       Contract.Requires(name != null);

-      int opBindingStrength = args.Length > 0 ? 0 : 2;

+      int opBindingStrength = args.Count > 0 ? 0 : 2;

       if (opBindingStrength < contextBindingStrength)

         stream.Write("(");

 

       stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(name));

-      int i = args.Length;

+      int i = args.Count;

       foreach (Type/*!*/ t in args) {

         Contract.Assert(t != null);

         stream.Write(" ");

@@ -3151,7 +3151,7 @@ Contract.Requires(that != null);
       MapType thatMapType = that as MapType;

       if (thatMapType == null ||

           this.TypeParameters.Length != thatMapType.TypeParameters.Length ||

-          this.Arguments.Length != thatMapType.Arguments.Length)

+          this.Arguments.Count != thatMapType.Arguments.Count)

         return false;

 

       foreach (TypeVariable/*!*/ var in this.TypeParameters) {

@@ -3165,7 +3165,7 @@ Contract.Requires(that != null);
 

       try {

 

-        for (int i = 0; i < Arguments.Length; ++i) {

+        for (int i = 0; i < Arguments.Count; ++i) {

           if (!Arguments[i].Equals(thatMapType.Arguments[i],

                                    thisBoundVariables, thatBoundVariables))

             return false;

@@ -3197,7 +3197,7 @@ Contract.Requires(that != null);
       MapType thatMapType = that as MapType;

       if (thatMapType == null ||

           this.TypeParameters.Length != thatMapType.TypeParameters.Length ||

-          this.Arguments.Length != thatMapType.Arguments.Length)

+          this.Arguments.Count != thatMapType.Arguments.Count)

         return false;

 

       // treat the bound variables of the two map types as equal...

@@ -3216,7 +3216,7 @@ Contract.Requires(that != null);
       }

       // ... and then unify the domain and range types

       bool good = true;

-      for (int i = 0; i < this.Arguments.Length; i++) {

+      for (int i = 0; i < this.Arguments.Count; i++) {

         Type t0 = this.Arguments[i].Substitute(subst0);

         Type t1 = thatMapType.Arguments[i].Substitute(subst1);

         good &= t0.Unify(t1, unifiableVariables, result);

@@ -3357,7 +3357,7 @@ Contract.Assert(var != null);
     [Pure]

     public override int GetHashCode(TypeVariableSeq boundVariables) {

       //Contract.Requires(boundVariables != null);

-      int res = 7643761 * TypeParameters.Length + 65121 * Arguments.Length;

+      int res = 7643761 * TypeParameters.Length + 65121 * Arguments.Count;

 

       foreach (TypeVariable/*!*/ var in this.TypeParameters) {

         Contract.Assert(var != null);

@@ -3470,7 +3470,7 @@ Contract.Assert(var != null);
     }

     public override int MapArity {

       get {

-        return Arguments.Length;

+        return Arguments.Count;

       }

     }

 

@@ -3498,7 +3498,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
         tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

         return null;

       } else {

-        Contract.Assert(actualResult.Length == 1);

+        Contract.Assert(actualResult.Count == 1);

         tpInstantiation = SimpleTypeParamInstantiation.From(TypeParameters, actualTypeParams);

         return actualResult[0];

       }

diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs
index 30ca85ba..cac5068a 100644
--- a/Source/Core/BitvectorAnalysis.cs
+++ b/Source/Core/BitvectorAnalysis.cs
@@ -128,7 +128,7 @@ namespace Microsoft.Boogie {
         TypeSeq newArguments = new TypeSeq();

         Type result = NewType(mapType.Result, mapDisjointSet.Result);

         bool newTypeNeeded = (result != mapType.Result);

-        for (int i = 0; i < mapType.Arguments.Length; i++) {

+        for (int i = 0; i < mapType.Arguments.Count; i++) {

           if (mapDisjointSet.Args(i).Find() == uniqueBv32Set.Find()) {

             newArguments.Add(new BvType(32));

             newTypeNeeded = true;

@@ -151,7 +151,7 @@ namespace Microsoft.Boogie {
       if (mapType == null) {

         return new DisjointSet();

       }

-      DisjointSet[] args = new DisjointSet[mapType.Arguments.Length];

+      DisjointSet[] args = new DisjointSet[mapType.Arguments.Count];

       for (int i = 0; i < args.Length; i++) {

         args[i] = MakeDisjointSet(mapType.Arguments[i]);

       }

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 64ddbb50..9cd7d524 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -588,9 +588,9 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>
 = (. Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;

      TypeVariableSeq/*!*/ typeParams;

      VariableSeq/*!*/ ins, outs;

-     RequiresSeq/*!*/ pre = new RequiresSeq();

+     List<Requires>/*!*/ pre = new List<Requires>();

      IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();

-     EnsuresSeq/*!*/ post = new EnsuresSeq();

+     List<Ensures>/*!*/ post = new List<Ensures>();

 

      VariableSeq/*!*/ locals = new VariableSeq();

      StmtList/*!*/ stmtList;

@@ -642,7 +642,7 @@ ProcSignature<bool allowWhereClausesOnFormals, out IToken/*!*/ name, out TypeVar
   .

 

 

-Spec<RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post>

+Spec<List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post>

 = (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; .)

   ( "modifies"

     [ Idents<out ms>        (. foreach(IToken/*!*/ m in ms){

@@ -656,7 +656,7 @@ Spec<RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post>
   )

   .

 

-SpecPrePost<bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post>

+SpecPrePost<bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post>

 = (. Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; .)

   ( "requires"              (. tok = t; .)

     { Attribute<ref kv> }

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index fe189f83..1bea5880 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -353,27 +353,30 @@ namespace Microsoft.Boogie {
   public delegate Expr/*?*/ Substitution(Variable/*!*/ v);

 

   public static class Substituter {

-    public static Substitution SubstitutionFromHashtable(Hashtable/*Variable!->Expr!*/ map) {

+    public static Substitution SubstitutionFromHashtable(Dictionary<Variable, Expr> map) {

       Contract.Requires(map != null);

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

       // TODO: With Whidbey, could use anonymous functions.

       return new Substitution(new CreateSubstitutionClosure(map).Method);

     }

     private sealed class CreateSubstitutionClosure {

-      Hashtable/*Variable!->Expr!*//*!*/ map;

+      Dictionary<Variable /*!*/, Expr /*!*/>/*!*/ map;

       [ContractInvariantMethod]

       void ObjectInvariant() {

         Contract.Invariant(map != null);

       }

 

-      public CreateSubstitutionClosure(Hashtable/*Variable!->Expr!*/ map)

+      public CreateSubstitutionClosure(Dictionary<Variable, Expr> map)

         : base() {

         Contract.Requires(map != null);

         this.map = map;

       }

       public Expr/*?*/ Method(Variable v) {

         Contract.Requires(v != null);

-        return (Expr)map[v];

+        if(map.ContainsKey(v)) {

+          return map[v];

+        }

+        return null;

       }

     }

 

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 57910775..26d57f68 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -328,7 +328,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(newModifies != null);

       Contract.Requires(newLocalVars != null);

       

-      Hashtable substMap = new Hashtable();

+      Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();

       Procedure proc = impl.Proc;

 

       foreach (Variable/*!*/ locVar in cce.NonNull(impl.OriginalLocVars)) {

@@ -365,7 +365,7 @@ namespace Microsoft.Boogie {
         }

       }

 

-      Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/();

+      Dictionary<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>();

 

       foreach (IdentifierExpr/*!*/ mie in proc.Modifies) {

         Contract.Assert(mie != null);

@@ -453,7 +453,7 @@ namespace Microsoft.Boogie {
       }

 

       // inject requires

-      for (int i = 0; i < proc.Requires.Length; i++) {

+      for (int i = 0; i < proc.Requires.Count; i++) {

         Requires/*!*/ req = cce.NonNull(proc.Requires[i]);

         inCmds.Add(InlinedRequires(callCmd, req));

       }

@@ -529,7 +529,7 @@ namespace Microsoft.Boogie {
       CmdSeq outCmds = new CmdSeq();

 

       // inject ensures

-      for (int i = 0; i < proc.Ensures.Length; i++) {

+      for (int i = 0; i < proc.Ensures.Count; i++) {

         Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);

         outCmds.Add(InlinedEnsures(callCmd, ens));

       }

@@ -588,12 +588,12 @@ namespace Microsoft.Boogie {
     public Substitution Subst;

     public Substitution OldSubst;

 

-    public CodeCopier(Hashtable substMap) {

+    public CodeCopier(Dictionary<Variable, Expr> substMap) {

       Contract.Requires(substMap != null);

       Subst = Substituter.SubstitutionFromHashtable(substMap);

     }

 

-    public CodeCopier(Hashtable substMap, Hashtable oldSubstMap) {

+    public CodeCopier(Dictionary<Variable, Expr> substMap, Dictionary<Variable, Expr> oldSubstMap) {

       Contract.Requires(oldSubstMap != null);

       Contract.Requires(substMap != null);

       Subst = Substituter.SubstitutionFromHashtable(substMap);

diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
index b3b02724..6874f1c9 100644
--- a/Source/Core/LambdaHelper.cs
+++ b/Source/Core/LambdaHelper.cs
@@ -95,7 +95,7 @@ namespace Microsoft.Boogie {
           Set freeVars = new Set();

           lambda.ComputeFreeVariables(freeVars);

           // this is ugly, the output will depend on hashing order

-          Hashtable subst = new Hashtable();

+          Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();

           VariableSeq formals = new VariableSeq();

           ExprSeq callArgs = new ExprSeq();

           ExprSeq axCallArgs = new ExprSeq();

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 27312f38..1d541183 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -216,7 +216,7 @@ namespace Microsoft.Boogie
                 MapType mapType = type as MapType;

                 if (mapType != null)

                 {

-                    if (mapType.Arguments.Length == 1 && mapType.Result.Equals(Type.Bool))

+                    if (mapType.Arguments.Count == 1 && mapType.Result.Equals(Type.Bool))

                     {

                         type = mapType.Arguments[0];

                         if (type is MapType)

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index e353700f..bd6b1da3 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -176,7 +176,7 @@ namespace Microsoft.Boogie
                 Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);

                 inputs.Add(f);

             }

-            yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

+            yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new VariableSeq(), new List<Requires>(), new IdentifierExprSeq(), new List<Ensures>());

             yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

         }

 

@@ -275,13 +275,13 @@ namespace Microsoft.Boogie
 

             VariableSeq inParams = new VariableSeq();

             VariableSeq outParams = new VariableSeq();

-            RequiresSeq requiresSeq = new RequiresSeq();

-            EnsuresSeq ensuresSeq = new EnsuresSeq();

+            List<Requires> requiresSeq = new List<Requires>();

+            List<Ensures> ensuresSeq = new List<Ensures>();

             IdentifierExprSeq ieSeq = new IdentifierExprSeq();

             int count = 0;

             while (callCmd != null)

             {

-                Hashtable map = new Hashtable();

+                Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

                 foreach (Variable x in callCmd.Proc.InParams)

                 {

                     Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true);

@@ -317,7 +317,7 @@ namespace Microsoft.Boogie
             return proc;

         }

 

-        private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, Hashtable map)

+        private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, Dictionary<Variable, Expr> map)

         {

             if (yields.Count == 0) return;

 

@@ -354,8 +354,8 @@ namespace Microsoft.Boogie
                 locals.Add(copy);

                 map[decl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy);

             }

-            Hashtable ogOldLocalMap = new Hashtable();

-            Hashtable assumeMap = new Hashtable(map);

+            Dictionary<Variable, Expr> ogOldLocalMap = new Dictionary<Variable, Expr>();

+            Dictionary<Variable, Expr> assumeMap = new Dictionary<Variable, Expr>(map);

             foreach (IdentifierExpr ie in globalMods)

             {

                 Variable g = ie.Decl;

@@ -406,7 +406,7 @@ namespace Microsoft.Boogie
 

             // Create the yield checker procedure

             var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name);

-            var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

+            var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), new List<Requires>(), new IdentifierExprSeq(), new List<Ensures>());

             yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

             yieldCheckerProcs.Add(yieldCheckerProc);

 

@@ -422,7 +422,7 @@ namespace Microsoft.Boogie
             Program program = linearTypechecker.program;

             ProcedureInfo info = procNameToInfo[impl.Name];

 

-            Hashtable map = new Hashtable();

+            Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

             foreach (Variable local in impl.LocVars)

             {

                 var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type));

@@ -504,7 +504,7 @@ namespace Microsoft.Boogie
                         {

                             if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))

                             {

-                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new IdentifierExprSeq(), new EnsuresSeq());

+                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new IdentifierExprSeq(), new List<Ensures>());

                             }

                             var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];

                             CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);

@@ -639,7 +639,7 @@ namespace Microsoft.Boogie
             // Collect the yield predicates and desugar yields

             List<CmdSeq> yields = new List<CmdSeq>();

             CmdSeq cmds = new CmdSeq();

-            if (proc.Requires.Length > 0)

+            if (proc.Requires.Count > 0)

             {

                 Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();

                 foreach (var domainName in linearTypechecker.linearDomains.Keys)

@@ -678,7 +678,7 @@ namespace Microsoft.Boogie
                 yields.Add(cmds);

                 cmds = new CmdSeq();

             }

-            if (info.inParallelCall && proc.Ensures.Length > 0)

+            if (info.inParallelCall && proc.Ensures.Count > 0)

             {

                 Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();

                 foreach (var domainName in linearTypechecker.linearDomains.Keys)

@@ -717,7 +717,7 @@ namespace Microsoft.Boogie
                 yields.Add(cmds);

                 cmds = new CmdSeq();

             }

-            CreateYieldCheckerImpl(proc, yields, new Hashtable());

+            CreateYieldCheckerImpl(proc, yields, new Dictionary<Variable, Expr>());

         }

 

         private void AddYieldProcAndImpl() 

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 95c46934..7bd21d02 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -403,7 +403,7 @@ private class BvBounds : Expr {
 		     }

 		     Bpl.Type ty = curr.Type;

 		     var uti = ty as UnresolvedTypeIdentifier;

-		     if (uti != null && uti.Arguments.Length == 0) {

+		     if (uti != null && uti.Arguments.Count == 0) {

 		       // the given "thing" was just an identifier, so let's use it as the name of the parameter

 		       curr.Name = uti.Name;

 		       curr.Type = prevType;

@@ -470,9 +470,9 @@ private class BvBounds : Expr {
 		Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;

 		TypeVariableSeq/*!*/ typeParams;

 		VariableSeq/*!*/ ins, outs;

-		RequiresSeq/*!*/ pre = new RequiresSeq();

+		List<Requires>/*!*/ pre = new List<Requires>();

 		IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();

-		EnsuresSeq/*!*/ post = new EnsuresSeq();

+		List<Ensures>/*!*/ post = new List<Ensures>();

 		

 		VariableSeq/*!*/ locals = new VariableSeq();

 		StmtList/*!*/ stmtList;

@@ -798,7 +798,7 @@ private class BvBounds : Expr {
 		if (la.kind == 11) {

 			Get();

 			var uti = ty as UnresolvedTypeIdentifier;

-			if (uti != null && uti.Arguments.Length == 0) {

+			if (uti != null && uti.Arguments.Count == 0) {

 			 varName = uti.Name;

 			} else {

 			 this.SemErr("expected identifier before ':'");

@@ -867,7 +867,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		}

 	}

 

-	void Spec(RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post) {

+	void Spec(List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post) {

 		Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; 

 		if (la.kind == 34) {

 			Get();

@@ -897,7 +897,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		StmtList(out stmtList);

 	}

 

-	void SpecPrePost(bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post) {

+	void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {

 		Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; 

 		if (la.kind == 36) {

 			Get();

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index ee873bd4..927b73fe 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -194,7 +194,7 @@ namespace Microsoft.Boogie {
     public virtual CtorType VisitCtorType(CtorType node) {

       Contract.Requires(node != null);

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

-      for (int i = 0; i < node.Arguments.Length; ++i)

+      for (int i = 0; i < node.Arguments.Count; ++i)

         node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));

       return node;

     }

@@ -248,10 +248,10 @@ namespace Microsoft.Boogie {
       @requires.Condition = this.VisitExpr(@requires.Condition);

       return @requires;

     }

-    public virtual RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) {

+    public virtual List<Requires> VisitRequiresSeq(List<Requires> requiresSeq) {

       Contract.Requires(requiresSeq != null);

-      Contract.Ensures(Contract.Result<RequiresSeq>() != null);

-      for (int i = 0, n = requiresSeq.Length; i < n; i++)

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

+      for (int i = 0, n = requiresSeq.Count; i < n; i++)

         requiresSeq[i] = this.VisitRequires(requiresSeq[i]);

       return requiresSeq;

     }

@@ -261,10 +261,10 @@ namespace Microsoft.Boogie {
       @ensures.Condition = this.VisitExpr(@ensures.Condition);

       return @ensures;

     }

-    public virtual EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) {

+    public virtual List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq) {

       Contract.Requires(ensuresSeq != null);

-      Contract.Ensures(Contract.Result<EnsuresSeq>() != null);

-      for (int i = 0, n = ensuresSeq.Length; i < n; i++)

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

+      for (int i = 0, n = ensuresSeq.Count; i < n; i++)

         ensuresSeq[i] = this.VisitEnsures(ensuresSeq[i]);

       return ensuresSeq;

     }

@@ -362,7 +362,7 @@ namespace Microsoft.Boogie {
       //

       // NOTE: when overriding this method, you have to make sure that

       // the bound variables of the map type are updated correctly

-      for (int i = 0; i < node.Arguments.Length; ++i)

+      for (int i = 0; i < node.Arguments.Count; ++i)

         node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));

       node.Result = cce.NonNull((Type/*!*/)this.Visit(node.Result));

       return node;

@@ -512,7 +512,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(node != null);

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

       node.ExpandedType = cce.NonNull((Type/*!*/)this.Visit(node.ExpandedType));

-      for (int i = 0; i < node.Arguments.Length; ++i)

+      for (int i = 0; i < node.Arguments.Count; ++i)

         node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));

       return node;

     }