diff options
| author |  tabarbe <unknown> | 2010-08-20 22:32:24 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-20 22:32:24 +0000 |
| commit | 72b39a6962d7f6c7ca1aab9919791238c7baba3f (patch) | |
| tree | 75bb9c1b956d1b368f4cf2983a20a913211dd350 /Source/Core/AbsyType.cs | |
| parent | 96d9624e9e22dbe9090e0bd7d538cafbf0a16463 (diff) | |
Boogie: Committing changed source files
Diffstat (limited to 'Source/Core/AbsyType.cs')
| -rw-r--r-- | Source/Core/AbsyType.cs | 2539 |
1 files changed, 1678 insertions, 861 deletions
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 55b8913f..7f3baa67 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -7,24 +7,23 @@ // BoogiePL - Absy.cs
//---------------------------------------------------------------------------------------------
-namespace Microsoft.Boogie
-{
+namespace Microsoft.Boogie {
using System;
using System.Collections;
using System.Diagnostics;
using System.Collections.Generic;
using Microsoft.Boogie.AbstractInterpretation;
using AI = Microsoft.AbstractInterpretationFramework;
- using Microsoft.Contracts;
+ using System.Diagnostics.Contracts;
//=====================================================================
//---------------------------------------------------------------------
// Types
-
+ [ContractClass(typeof(TypeContracts))]
public abstract class Type : Absy {
- public Type(IToken! token)
- : base(token)
- {
+ public Type(IToken/*!*/ token)
+ : base(token) {
+ Contract.Requires(token != null);
}
//----------- Cloning ----------------------------------
@@ -34,59 +33,65 @@ namespace Microsoft.Boogie // a type in which all bound variables have been replaced with new
// variables, whereas free variables have not changed
- public override Absy! Clone() {
- return this.Clone(new Dictionary<TypeVariable!, TypeVariable!> ());
+ public override Absy Clone() {
+ Contract.Ensures(Contract.Result<Absy>() != null);
+ return this.Clone(new Dictionary<TypeVariable/*!*/, TypeVariable/*!*/>());
}
- public abstract Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap);
+ public abstract Type/*!*/ Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap);
/// <summary>
/// Clones the type, but only syntactically. Anything resolved in the source
/// type is left unresolved (that is, with just the name) in the destination type.
/// </summary>
- public abstract Type! CloneUnresolved();
-
+ public abstract Type/*!*/ CloneUnresolved();
+
//----------- Linearisation ----------------------------------
- public void Emit(TokenTextWriter! stream) {
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
this.Emit(stream, 0);
}
- public abstract void Emit(TokenTextWriter! stream, int contextBindingStrength);
+ public abstract void Emit(TokenTextWriter/*!*/ stream, int contextBindingStrength);
[Pure]
- public override string! ToString() {
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
System.IO.StringWriter buffer = new System.IO.StringWriter();
- using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false))
- {
+ using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
this.Emit(stream);
}
return buffer.ToString();
}
-
+
//----------- Equality ----------------------------------
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object that)
- {
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
if (ReferenceEquals(this, that))
return true;
Type thatType = that as Type;
return thatType != null && this.Equals(thatType,
- new TypeVariableSeq (),
- new TypeVariableSeq ());
+ new TypeVariableSeq(),
+ new TypeVariableSeq());
}
[Pure]
- public abstract bool Equals(Type! that,
- TypeVariableSeq! thisBoundVariables,
- TypeVariableSeq! thatBoundVariables);
+ public abstract bool Equals(Type/*!*/ that,
+ TypeVariableSeq/*!*/ thisBoundVariables,
+ TypeVariableSeq/*!*/ thatBoundVariables);
// used to skip leading type annotations (subexpressions of the
// resulting type might still contain annotations)
- internal virtual Type! Expanded { get {
- return this;
- } }
+ internal virtual Type/*!*/ Expanded {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ return this;
+ }
+ }
//----------- Unification of types -----------
@@ -95,23 +100,23 @@ namespace Microsoft.Boogie /// If not possible, return false (which may have added some partial constraints).
/// No error is printed.
/// </summary>
- public bool Unify(Type! that) {
- return Unify(that, new TypeVariableSeq(), new Dictionary<TypeVariable!, Type!> ());
+ public bool Unify(Type that) {
+ Contract.Requires(that != null);
+ return Unify(that, new TypeVariableSeq(), new Dictionary<TypeVariable/*!*/, Type/*!*/>());
}
- public abstract bool Unify(Type! that,
- TypeVariableSeq! unifiableVariables,
- // an idempotent substitution that describes the
- // unification result up to a certain point
- IDictionary<TypeVariable!, Type!>! unifier);
- requires forall{TypeVariable key in unifier.Keys; unifiableVariables.Has(key)};
- requires IsIdempotent(unifier);
+ public abstract bool Unify(Type/*!*/ that,
+ TypeVariableSeq/*!*/ unifiableVariables,
+ // an idempotent substitution that describes the
+ // unification result up to a certain point
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier);
+
[Pure]
- public static bool IsIdempotent(IDictionary<TypeVariable!, Type!>! unifier) {
- return forall{Type! t in unifier.Values;
- forall{TypeVariable! var in t.FreeVariables;
- !unifier.ContainsKey(var)}};
+ public static bool IsIdempotent(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {
+ Contract.Requires(cce.NonNullElements(unifier));
+ return Contract.ForAll(unifier.Values, t => Contract.ForAll(0, t.FreeVariables.Length, var =>
+ !unifier.ContainsKey(t.FreeVariables[var])));
}
@@ -138,16 +143,16 @@ namespace Microsoft.Boogie // given mappings that need to be taken into account
// the old unifier has to be idempotent as well
IDictionary<TypeVariable!, Type!>! unifier)
- requires forall{TypeVariable key in unifier.Keys; unifiableVariables.Has(key)};
- requires IsIdempotent(unifier);
- {
+ {
+ Contract.Requires(Contract.ForAll(unifier.Keys , key=> unifiableVariables.Has(key)));
+ Contract.Requires(IsIdempotent(unifier));
try {
this.Unify(that, unifiableVariables,
new TypeVariableSeq (), new TypeVariableSeq (), unifier);
} catch (UnificationFailedException) {
return false;
}
- return true; + return true;
}
public abstract void Unify(Type! that,
@@ -161,8 +166,8 @@ namespace Microsoft.Boogie //----------- Substitution of free variables with types not containing bound variables -----------------
- public abstract Type! Substitute(IDictionary<TypeVariable!, Type!>! subst);
-
+ public abstract Type/*!*/ Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst);
+
//----------- Hashcodes ----------------------------------
// Hack to be able to access the hashcode of superclasses further up
@@ -173,44 +178,51 @@ namespace Microsoft.Boogie }
[Pure]
- public override int GetHashCode()
- {
- return this.GetHashCode(new TypeVariableSeq ());
+ public override int GetHashCode() {
+ return this.GetHashCode(new TypeVariableSeq());
}
[Pure]
- public abstract int GetHashCode(TypeVariableSeq! boundVariables);
+ public abstract int GetHashCode(TypeVariableSeq/*!*/ boundVariables);
//----------- Resolution ----------------------------------
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
System.Diagnostics.Debug.Fail("Type.Resolve should never be called." +
" Use Type.ResolveType instead");
}
- public abstract Type! ResolveType(ResolutionContext! rc);
+ public abstract Type/*!*/ ResolveType(ResolutionContext/*!*/ rc);
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
System.Diagnostics.Debug.Fail("Type.Typecheck should never be called");
}
// determine the free variables in a type, in the order in which the variables occur
- public abstract TypeVariableSeq! FreeVariables { get; }
+ public abstract TypeVariableSeq/*!*/ FreeVariables {
+ get;
+ }
// determine the free type proxies in a type, in the order in which they occur
- public abstract List<TypeProxy!>! FreeProxies { get; }
+ public abstract List<TypeProxy/*!*/>/*!*/ FreeProxies {
+ get;
+ }
- protected static void AppendWithoutDups<A>(List<A>! a, List<A>! b) {
+ protected static void AppendWithoutDups<A>(List<A> a, List<A> b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
foreach (A x in b)
if (!a.Contains(x))
a.Add(x);
}
- public bool IsClosed { get {
- return FreeVariables.Length == 0;
- } }
+ public bool IsClosed {
+ get {
+ return FreeVariables.Length == 0;
+ }
+ }
//----------- Getters/Issers ----------------------------------
@@ -218,42 +230,114 @@ namespace Microsoft.Boogie // C# "is" operator, because they handle type synonym annotations and
// type proxies correctly
- public virtual bool IsBasic { get { return false; } }
- public virtual bool IsInt { get { return false; } }
- public virtual bool IsBool { get { return false; } }
-
- public virtual bool IsVariable { get { return false; } }
- public virtual TypeVariable! AsVariable { get {
- assert false; // Type.AsVariable should never be called
- } }
- public virtual bool IsCtor { get { return false; } }
- public virtual CtorType! AsCtor { get {
- assert false; // Type.AsCtor should never be called
- } }
- public virtual bool IsMap { get { return false; } }
- public virtual MapType! AsMap { get {
- assert false; // Type.AsMap should never be called
- } }
- public virtual int MapArity { get {
- assert false; // Type.MapArity should never be called
- } }
- public virtual bool IsUnresolved { get { return false; } }
- public virtual UnresolvedTypeIdentifier! AsUnresolved { get {
- assert false; // Type.AsUnresolved should never be called
- } }
-
- public virtual bool IsBv { get { return false; } }
- public virtual int BvBits { get {
- assert false; // Type.BvBits should never be called
- } }
-
- public static readonly Type! Int = new BasicType(SimpleType.Int);
- public static readonly Type! Bool = new BasicType(SimpleType.Bool);
+ public virtual bool IsBasic {
+ get {
+ return false;
+ }
+ }
+ public virtual bool IsInt {
+ get {
+ return false;
+ }
+ }
+ public virtual bool IsBool {
+ get {
+ return false;
+ }
+ }
+
+ public virtual bool IsVariable {
+ get {
+ return false;
+ }
+ }
+ public virtual TypeVariable/*!*/ AsVariable {
+ get {
+ Contract.Ensures(Contract.Result<TypeVariable>() != null);
+
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // Type.AsVariable should never be called
+ }
+ }
+ public virtual bool IsCtor {
+ get {
+ return false;
+ }
+ }
+ public virtual CtorType/*!*/ AsCtor {
+ get {
+ Contract.Ensures(Contract.Result<CtorType>() != null);
+
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // Type.AsCtor should never be called
+ }
+ }
+ public virtual bool IsMap {
+ get {
+ return false;
+ }
+ }
+ public virtual MapType/*!*/ AsMap {
+ get {
+ Contract.Ensures(Contract.Result<MapType>() != null);
+
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // Type.AsMap should never be called
+ }
+ }
+ public virtual int MapArity {
+ get {
+
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // Type.MapArity should never be called
+ }
+ }
+ public virtual bool IsUnresolved {
+ get {
+ return false;
+ }
+ }
+ public virtual UnresolvedTypeIdentifier/*!*/ AsUnresolved {
+ get {
+ Contract.Ensures(Contract.Result<UnresolvedTypeIdentifier>() != null);
+
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // Type.AsUnresolved should never be called
+ }
+ }
+
+ public virtual bool IsBv {
+ get {
+ return false;
+ }
+ }
+ public virtual int BvBits {
+ get {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // Type.BvBits should never be called
+ }
+ }
+
+ public static readonly Type/*!*/ Int = new BasicType(SimpleType.Int);
+ public static readonly Type/*!*/ Bool = new BasicType(SimpleType.Bool);
private static BvType[] bvtypeCache;
-
- static public BvType! GetBvType(int sz)
- requires 0 <= sz;
- {
+
+ static public BvType GetBvType(int sz) {
+ Contract.Requires(0 <= sz);
+ Contract.Ensures(Contract.Result<BvType>() != null);
+
if (bvtypeCache == null) {
bvtypeCache = new BvType[128];
}
@@ -281,20 +365,20 @@ namespace Microsoft.Boogie IdentifierExprSeq actualOuts,
string! opName,
TypecheckingContext! tc)
- requires formalArgs.Length == actualArgs.Length;
- requires formalOuts == null <==> actualOuts == null;
- requires formalOuts != null ==> formalOuts.Length == actualOuts.Length;
- {
+ {
+ Contract.Requires(formalArgs.Length == actualArgs.Length);
+ Contract.Requires(formalOuts == null <==> actualOuts == null);
+ Contract.Requires(formalOuts != null ==> formalOuts.Length == actualOuts.Length);
TypeVariableSeq! boundVarSeq0 = new TypeVariableSeq ();
TypeVariableSeq! boundVarSeq1 = new TypeVariableSeq ();
Dictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!>();
for (int i = 0; i < formalArgs.Length; ++i) {
try {
- Type! actualType = (!)((!)actualArgs[i]).Type;
+ Type! actualType = cce.NonNull((!)actualArgs[i]).Type;
// if the type variables to be matched occur in the actual
// argument types, something has gone very wrong
- assert forall{TypeVariable! var in typeParams;
+ Contract.Assert(forall{TypeVariable! var in typeParams);
!actualType.FreeVariables.Has(var)};
formalArgs[i].Unify(actualType,
typeParams,
@@ -309,17 +393,17 @@ namespace Microsoft.Boogie formalArgs[i].Substitute(subst));
// the bound variable sequences should be empty ...
// so that we can continue with the unification
- assert boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0;
+ Contract.Assert(boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0);
}
}
if (formalOuts != null) {
for (int i = 0; i < formalOuts.Length; ++i) {
try {
- Type! actualType = (!)((!)actualOuts[i]).Type;
+ Type! actualType = cce.NonNull((!)actualOuts[i]).Type;
// if the type variables to be matched occur in the actual
// argument types, something has gone very wrong
- assert forall{TypeVariable! var in typeParams;
+ Contract.Assert(forall{TypeVariable! var in typeParams);
!actualType.FreeVariables.Has(var)};
formalOuts[i].Unify(actualType,
typeParams,
@@ -334,71 +418,79 @@ namespace Microsoft.Boogie formalOuts[i].Substitute(subst));
// the bound variable sequences should be empty ...
// so that we can continue with the unification
- assert boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0;
+ Contract.Assert(boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0);
}
}
}
// we only allow type parameters to be substituted
- assert forall{TypeVariable! var in subst.Keys; typeParams.Has(var)};
+ Contract.Assert(Contract.ForAll(subst.Keys , var=> typeParams.Has(var)));
return subst;
}
#else
- public static IDictionary<TypeVariable!, Type!>!
- MatchArgumentTypes(TypeVariableSeq! typeParams,
- TypeSeq! formalArgs,
- ExprSeq! actualArgs,
+ public static IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/
+ MatchArgumentTypes(TypeVariableSeq/*!*/ typeParams,
+ TypeSeq/*!*/ formalArgs,
+ ExprSeq/*!*/ actualArgs,
TypeSeq formalOuts,
IdentifierExprSeq actualOuts,
- string! opName,
- TypecheckingContext! tc)
- requires formalArgs.Length == actualArgs.Length;
- requires formalOuts == null <==> actualOuts == null;
- requires formalOuts != null ==> formalOuts.Length == ((!)actualOuts).Length;
- requires tc != null ==> opName != null;
+ string/*!*/ opName,
+ TypecheckingContext/*!*/ tc) {
+ Contract.Requires(typeParams != null);
+ Contract.Requires(formalArgs != null);
+ Contract.Requires(actualArgs != null);
+ Contract.Requires(opName != null);
+ Contract.Requires(tc != null);
+ Contract.Requires(formalArgs.Length == actualArgs.Length);
+ Contract.Requires((formalOuts == null) == (actualOuts == null));
+ Contract.Requires(formalOuts == null || formalOuts.Length == cce.NonNull(actualOuts).Length);
+ Contract.Requires(tc == null || opName != null);//Redundant
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IDictionary<TypeVariable, Type>>()));
+
// requires "actualArgs" and "actualOuts" to have been type checked
- {
- Dictionary<TypeVariable!, Type!> subst = new Dictionary<TypeVariable!, Type!>();
- foreach (TypeVariable! tv in typeParams) {
+
+ Dictionary<TypeVariable/*!*/, Type/*!*/> subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
+ foreach (TypeVariable/*!*/ tv in typeParams) {
+ Contract.Assert(tv != null);
TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name);
subst.Add(tv, proxy);
}
-
+
for (int i = 0; i < formalArgs.Length; i++) {
Type formal = formalArgs[i].Substitute(subst);
- Type actual = (!)((!)actualArgs[i]).Type;
+ Type actual = cce.NonNull(cce.NonNull(actualArgs[i]).Type);
// if the type variables to be matched occur in the actual
// argument types, something has gone very wrong
- assert forall{TypeVariable! var in typeParams; !actual.FreeVariables.Has(var)};
+ Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !actual.FreeVariables.Has(typeParams[index])));
if (!formal.Unify(actual)) {
- assume tc != null; // caller expected no errors
- assert opName != null; // follows from precondition
- tc.Error((!)actualArgs[i],
+ Contract.Assume(tc != null); // caller expected no errors
+ Contract.Assert(opName != null); // follows from precondition
+ tc.Error(cce.NonNull(actualArgs[i]),
"invalid type for argument {0} in {1}: {2} (expected: {3})",
i, opName, actual, formalArgs[i]);
}
}
-
+
if (formalOuts != null) {
for (int i = 0; i < formalOuts.Length; ++i) {
Type formal = formalOuts[i].Substitute(subst);
- Type actual = (!)((!)actualOuts)[i].Type;
+ Type actual = cce.NonNull(cce.NonNull(actualOuts)[i].Type);
// if the type variables to be matched occur in the actual
// argument types, something has gone very wrong
- assert forall{TypeVariable! var in typeParams; !actual.FreeVariables.Has(var)};
+ Contract.Assert(Contract.ForAll(0, typeParams.Length, var => !actual.FreeVariables.Has(typeParams[var])));
if (!formal.Unify(actual)) {
- assume tc != null; // caller expected no errors
- assert opName != null; // follows from precondition
+ Contract.Assume(tc != null); // caller expected no errors
+ Contract.Assert(opName != null); // follows from precondition
tc.Error(actualOuts[i],
"invalid type for out-parameter {0} in {1}: {2} (expected: {3})",
i, opName, actual, formal);
}
}
}
-
+
return subst;
}
#endif
@@ -407,18 +499,26 @@ namespace Microsoft.Boogie //------------ on concrete types, substitute the result into the
//------------ result type. Null is returned for type errors
- public static TypeSeq CheckArgumentTypes(TypeVariableSeq! typeParams,
- out List<Type!>! actualTypeParams,
- TypeSeq! formalIns,
- ExprSeq! actualIns,
- TypeSeq! formalOuts,
+ public static TypeSeq CheckArgumentTypes(TypeVariableSeq/*!*/ typeParams,
+ out List<Type/*!*/>/*!*/ actualTypeParams,
+ TypeSeq/*!*/ formalIns,
+ ExprSeq/*!*/ actualIns,
+ TypeSeq/*!*/ formalOuts,
IdentifierExprSeq actualOuts,
- IToken! typeCheckingSubject,
- string! opName,
- TypecheckingContext! tc)
+ IToken/*!*/ typeCheckingSubject,
+ string/*!*/ opName,
+ TypecheckingContext/*!*/ tc)
// requires "actualIns" and "actualOuts" to have been type checked
{
- actualTypeParams = new List<Type!> ();
+ Contract.Requires(typeParams != null);
+
+ Contract.Requires(formalIns != null);
+ Contract.Requires(formalOuts != null);
+ Contract.Requires(actualIns != null);
+ Contract.Requires(actualOuts != null);
+ Contract.Requires(typeCheckingSubject != null);
+ Contract.Requires(opName != null);Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out actualTypeParams)));
+ actualTypeParams = new List<Type/*!*/>();
if (formalIns.Length != actualIns.Length) {
tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1}",
@@ -431,20 +531,23 @@ namespace Microsoft.Boogie opName, actualOuts.Length);
// if there are no type parameters, we can still return the result
// type and hope that the type checking proceeds
- actualTypeParams = new List<Type!> ();
+ actualTypeParams = new List<Type>();
return typeParams.Length == 0 ? formalOuts : null;
}
int previousErrorCount = tc.ErrorCount;
- IDictionary<TypeVariable!, Type!> subst =
+ IDictionary<TypeVariable/*!*/, Type/*!*/> subst =
MatchArgumentTypes(typeParams, formalIns, actualIns,
actualOuts != null ? formalOuts : null, actualOuts, opName, tc);
-
- foreach (TypeVariable! var in typeParams)
+ Contract.Assert(cce.NonNullElements(subst));
+ foreach (TypeVariable/*!*/ var in typeParams) {
+ Contract.Assert(var != null);
actualTypeParams.Add(subst[var]);
+ }
- TypeSeq! actualResults = new TypeSeq ();
- foreach (Type! t in formalOuts) {
+ TypeSeq/*!*/ actualResults = new TypeSeq();
+ foreach (Type/*!*/ t in formalOuts) {
+ Contract.Assert(t != null);
actualResults.Add(t.Substitute(subst));
}
TypeVariableSeq resultFreeVars = FreeVariablesIn(actualResults);
@@ -453,7 +556,7 @@ namespace Microsoft.Boogie // in case we have been able to substitute all type parameters,
// we can still return the result type and hope that the
// type checking proceeds in a meaningful manner
- if (forall{TypeVariable! var in typeParams; !resultFreeVars.Has(var)})
+ if (Contract.ForAll(0, typeParams.Length, index => !resultFreeVars.Has(typeParams[index])))
return actualResults;
else
// otherwise there is no point in returning the result type,
@@ -461,7 +564,7 @@ namespace Microsoft.Boogie return null;
}
- assert forall{TypeVariable! var in typeParams; !resultFreeVars.Has(var)};
+ Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !resultFreeVars.Has(typeParams[index])));
return actualResults;
}
@@ -469,17 +572,26 @@ namespace Microsoft.Boogie // about the same as Type.CheckArgumentTypes, but without
// detailed error reports
- public static Type! InferValueType(TypeVariableSeq! typeParams,
- TypeSeq! formalArgs,
- Type! formalResult,
- TypeSeq! actualArgs) {
- IDictionary<TypeVariable!, Type!>! subst =
+ public static Type/*!*/ InferValueType(TypeVariableSeq/*!*/ typeParams,
+ TypeSeq/*!*/ formalArgs,
+ Type/*!*/ formalResult,
+ TypeSeq/*!*/ actualArgs) {
+ Contract.Requires(typeParams != null);
+ Contract.Requires(formalArgs != null);
+ Contract.Requires(formalResult != null);
+ Contract.Requires(actualArgs != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst =
InferTypeParameters(typeParams, formalArgs, actualArgs);
+ Contract.Assert(cce.NonNullElements(subst));
- Type! res = formalResult.Substitute(subst);
+ Type/*!*/ res = formalResult.Substitute(subst);
+ Contract.Assert(res != null);
// all type parameters have to be substituted with concrete types
- TypeVariableSeq! resFreeVars = res.FreeVariables;
- assert forall{TypeVariable! var in typeParams; !resFreeVars.Has(var)};
+ TypeVariableSeq/*!*/ resFreeVars = res.FreeVariables;
+ Contract.Assert(resFreeVars != null);
+ Contract.Assert(Contract.ForAll(0, typeParams.Length, var => !resFreeVars.Has(typeParams[var])));
return res;
}
@@ -488,7 +600,8 @@ namespace Microsoft.Boogie InferTypeParameters(TypeVariableSeq! typeParams,
TypeSeq! formalArgs,
TypeSeq! actualArgs)
- requires formalArgs.Length == actualArgs.Length; {
+ {
+ Contract.Requires(formalArgs.Length == actualArgs.Length);
TypeVariableSeq! boundVarSeq0 = new TypeVariableSeq ();
TypeVariableSeq! boundVarSeq1 = new TypeVariableSeq ();
@@ -496,7 +609,7 @@ namespace Microsoft.Boogie for (int i = 0; i < formalArgs.Length; ++i) {
try {
- assert forall{TypeVariable! var in typeParams;
+ Contract.Assert(forall{TypeVariable! var in typeParams);
!actualArgs[i].FreeVariables.Has(var)};
formalArgs[i].Unify(actualArgs[i], typeParams,
boundVarSeq0, boundVarSeq1, subst);
@@ -507,47 +620,54 @@ namespace Microsoft.Boogie }
// we only allow type parameters to be substituted
- assert forall{TypeVariable! var in subst.Keys; typeParams.Has(var)};
- return subst; + Contract.Assert(Contract.ForAll(subst.Keys , var=> typeParams.Has(var)));
+ return subst;
}
#else
/// <summary>
/// like Type.CheckArgumentTypes, but assumes no errors
/// (and only does arguments, not results; and takes actuals as TypeSeq, not ExprSeq)
/// </summary>
- public static IDictionary<TypeVariable!, Type!>!
- InferTypeParameters(TypeVariableSeq! typeParams,
- TypeSeq! formalArgs,
- TypeSeq! actualArgs)
- requires formalArgs.Length == actualArgs.Length;
- {
+ public static IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/
+ InferTypeParameters(TypeVariableSeq/*!*/ typeParams,
+ TypeSeq/*!*/ formalArgs,
+ TypeSeq/*!*/ actualArgs) {
+ Contract.Requires(typeParams != null);
+ Contract.Requires(formalArgs != null);
+ Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Length == actualArgs.Length);
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IDictionary<TypeVariable, Type>>()));
+
+
TypeSeq proxies = new TypeSeq();
- Dictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!>();
- foreach (TypeVariable! tv in typeParams) {
+ Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
+ foreach (TypeVariable/*!*/ tv in typeParams) {
+ Contract.Assert(tv != null);
TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name);
proxies.Add(proxy);
subst.Add(tv, proxy);
}
-
+
for (int i = 0; i < formalArgs.Length; i++) {
Type formal = formalArgs[i].Substitute(subst);
Type actual = actualArgs[i];
// if the type variables to be matched occur in the actual
// argument types, something has gone very wrong
- assert forall{TypeVariable! var in typeParams; !actual.FreeVariables.Has(var)};
+ Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !actual.FreeVariables.Has(typeParams[index])));
if (!formal.Unify(actual)) {
- assume false; // caller expected no errors
+ Contract.Assume(false); // caller expected no errors
}
}
-
+
return subst;
}
#endif
-
+
//----------- Helper methods to deal with bound type variables ---------------
- public static void EmitOptionalTypeParams(TokenTextWriter! stream, TypeVariableSeq! typeParams) {
+ public static void EmitOptionalTypeParams(TokenTextWriter stream, TypeVariableSeq typeParams) {
+ Contract.Requires(typeParams != null);
+ Contract.Requires(stream != null);
if (typeParams.Length > 0) {
stream.Write("<");
typeParams.Emit(stream, ","); // default binding strength of 0 is ok
@@ -556,9 +676,13 @@ namespace Microsoft.Boogie }
// Sort the type parameters according to the order of occurrence in the argument types
- public static TypeVariableSeq! SortTypeParams(TypeVariableSeq! typeParams,
- TypeSeq! argumentTypes, Type resultType)
- ensures result.Length == typeParams.Length; {
+ public static TypeVariableSeq/*!*/ SortTypeParams(TypeVariableSeq/*!*/ typeParams, TypeSeq/*!*/ argumentTypes, Type resultType) {
+ Contract.Requires(typeParams != null);
+ Contract.Requires(argumentTypes != null);
+ Contract.Requires(resultType != null);
+ Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
+
+ Contract.Ensures(Contract.Result<TypeVariableSeq>().Length == typeParams.Length);
if (typeParams.Length == 0) {
return typeParams;
}
@@ -569,13 +693,14 @@ namespace Microsoft.Boogie }
// "freeVarsInUse" is already sorted, but it may contain type variables not in "typeParams".
// So, project "freeVarsInUse" onto "typeParams":
- TypeVariableSeq! sortedTypeParams = new TypeVariableSeq ();
- foreach (TypeVariable! var in freeVarsInUse) {
+ TypeVariableSeq sortedTypeParams = new TypeVariableSeq();
+ foreach (TypeVariable/*!*/ var in freeVarsInUse) {
+ Contract.Assert(var != null);
if (typeParams.Has(var)) {
sortedTypeParams.Add(var);
}
}
-
+
if (sortedTypeParams.Length < typeParams.Length)
// add the type parameters not mentioned in "argumentTypes" in
// the end of the list (this can happen for quantifiers)
@@ -588,16 +713,22 @@ namespace Microsoft.Boogie // Return true if some type parameters appear only among "moreArgumentTypes" and
// not in "argumentTypes".
[Pure]
- public static bool CheckBoundVariableOccurrences(TypeVariableSeq! typeParams,
- TypeSeq! argumentTypes,
+ public static bool CheckBoundVariableOccurrences(TypeVariableSeq/*!*/ typeParams,
+ TypeSeq/*!*/ argumentTypes,
TypeSeq moreArgumentTypes,
- IToken! resolutionSubject,
- string! subjectName,
- ResolutionContext! rc) {
+ IToken/*!*/ resolutionSubject,
+ string/*!*/ subjectName,
+ ResolutionContext/*!*/ rc) {
+ Contract.Requires(typeParams != null);
+ Contract.Requires(argumentTypes != null);
+ Contract.Requires(resolutionSubject != null);
+ Contract.Requires(subjectName != null);
+ Contract.Requires(rc != null);
TypeVariableSeq freeVarsInArgs = FreeVariablesIn(argumentTypes);
TypeVariableSeq moFreeVarsInArgs = moreArgumentTypes == null ? null : FreeVariablesIn(moreArgumentTypes);
bool someTypeParamsAppearOnlyAmongMo = false;
- foreach (TypeVariable! var in typeParams) {
+ foreach (TypeVariable/*!*/ var in typeParams) {
+ Contract.Assert(var != null);
if (rc.LookUpTypeBinder(var.Name) == var) // avoid to complain twice about variables that are bound multiple times
{
if (freeVarsInArgs.Has(var)) {
@@ -615,28 +746,92 @@ namespace Microsoft.Boogie }
[Pure]
- public static TypeVariableSeq! FreeVariablesIn(TypeSeq! arguments) {
- TypeVariableSeq! res = new TypeVariableSeq ();
- foreach (Type! t in arguments)
+ public static TypeVariableSeq FreeVariablesIn(TypeSeq arguments) {
+ Contract.Requires(arguments != null);
+ Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
+ TypeVariableSeq/*!*/ res = new TypeVariableSeq();
+ foreach (Type/*!*/ t in arguments) {
+ Contract.Assert(t != null);
res.AppendWithoutDups(t.FreeVariables);
+ }
return res;
}
}
+ [ContractClassFor(typeof(Type))]
+ public abstract class TypeContracts : Type {
+ public TypeContracts() :base(null){
+
+ }
+ public override List<TypeProxy> FreeProxies {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
+ throw new NotImplementedException();
+ }
+ }
+ public override TypeVariableSeq FreeVariables {
+ get {
+ Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
+ throw new NotImplementedException();
+ }
+ }
+ public override Type Clone(IDictionary<TypeVariable, TypeVariable> varMap) {
+ Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ throw new NotImplementedException();
+ }
+ public override Type CloneUnresolved() {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ throw new NotImplementedException();
+ }
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
+ Contract.Requires(stream != null);
+ throw new NotImplementedException();
+ }
+ public override bool Equals(Type that, TypeVariableSeq thisBoundVariables, TypeVariableSeq thatBoundVariables) {
+ Contract.Requires(that != null);
+ Contract.Requires(thisBoundVariables != null);
+ Contract.Requires(thatBoundVariables != null);
+ throw new NotImplementedException();
+ }
+ public override bool Unify(Type that, TypeVariableSeq unifiableVariables, IDictionary<TypeVariable, Type> unifier) {
+ Contract.Requires(that != null);
+ Contract.Requires(unifiableVariables != null);
+ Contract.Requires(cce.NonNullElements(unifier));
+ Contract.Requires(Contract.ForAll(unifier.Keys, key => unifiableVariables.Has(key)));
+ Contract.Requires(IsIdempotent(unifier));
+ throw new NotImplementedException();
+ }
+ public override Type Substitute(IDictionary<TypeVariable, Type> subst) {
+ Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ throw new NotImplementedException();
+ }
+ public override Type ResolveType(ResolutionContext rc) {
+ Contract.Requires(rc != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ throw new NotImplementedException();
+ }
+ public override int GetHashCode(TypeVariableSeq boundVariables) {
+ Contract.Requires(boundVariables != null);
+ throw new NotImplementedException();
+ }
+ }
//=====================================================================
- public class BasicType : Type
- {
+ public class BasicType : Type {
public readonly SimpleType T;
- public BasicType(IToken! token, SimpleType t)
- : base(token)
- {
+ public BasicType(IToken/*!*/ token, SimpleType t)
+ : base(token) {
+ Contract.Requires(token != null);
T = t;
// base(token);
}
public BasicType(SimpleType t)
- : base(Token.NoToken)
- {
+ : base(Token.NoToken) {
T = t;
// base(Token.NoToken);
}
@@ -646,39 +841,47 @@ namespace Microsoft.Boogie // have to be created in the right way. It is /not/ ok to just clone
// everything recursively.
- public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
// BasicTypes are immutable anyway, we do not clone
return this;
}
- public override Type! CloneUnresolved() {
+ public override Type CloneUnresolved() {
+ Contract.Ensures(Contract.Result<Type>() != null);
return this;
}
//----------- Linearisation ----------------------------------
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
+ //Contract.Requires(stream != null);
// no parentheses are necessary for basic types
stream.SetToken(this);
stream.Write("{0}", this);
}
[Pure]
- public override string! ToString()
- {
- switch (T)
- {
- case SimpleType.Int: return "int";
- case SimpleType.Bool: return "bool";
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ switch (T) {
+ case SimpleType.Int:
+ return "int";
+ case SimpleType.Bool:
+ return "bool";
}
Debug.Assert(false, "bad type " + T);
- assert false; // make compiler happy
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // make compiler happy
}
//----------- Equality ----------------------------------
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
// shortcut
Type thatType = that as Type;
@@ -689,19 +892,22 @@ namespace Microsoft.Boogie }
[Pure]
- public override bool Equals(Type! that,
- TypeVariableSeq! thisBoundVariables,
- TypeVariableSeq! thatBoundVariables) {
+ public override bool Equals(Type that, TypeVariableSeq thisBoundVariables, TypeVariableSeq thatBoundVariables) {
+ //Contract.Requires(thatBoundVariables != null);
+ //Contract.Requires(thisBoundVariables != null);
+ //Contract.Requires(that != null);
return this.Equals(that);
}
//----------- Unification of types -----------
- public override bool Unify(Type! that,
- TypeVariableSeq! unifiableVariables,
- // an idempotent substitution that describes the
- // unification result up to a certain point
- IDictionary<TypeVariable!, Type!>! unifier) {
+ public override bool Unify(Type that, TypeVariableSeq unifiableVariables, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {
+ //Contract.Requires(unifiableVariables != null);
+ //Contract.Requires(that != null);
+ Contract.Requires(cce.NonNullElements(unifier));
+ // an idempotent substitution that describes the
+ // unification result up to a certain point
+
that = that.Expanded;
if (that is TypeProxy || that is TypeVariable) {
return that.Unify(this, unifiableVariables, unifier);
@@ -728,64 +934,84 @@ namespace Microsoft.Boogie //----------- Substitution of free variables with types not containing bound variables -----------------
- public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
+ //Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
return this;
}
//----------- Hashcodes ----------------------------------
[Pure]
- public override int GetHashCode(TypeVariableSeq! boundVariables)
- {
+ public override int GetHashCode(TypeVariableSeq boundVariables) {
+ //Contract.Requires(boundVariables != null);
return this.T.GetHashCode();
}
//----------- Resolution ----------------------------------
- public override Type! ResolveType(ResolutionContext! rc) {
+ public override Type ResolveType(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
// nothing to resolve
return this;
}
// determine the free variables in a type, in the order in which the variables occur
- public override TypeVariableSeq! FreeVariables {
+ public override TypeVariableSeq/*!*/ FreeVariables {
get {
- return new TypeVariableSeq (); // basic type are closed
+ Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
+
+ return new TypeVariableSeq(); // basic type are closed
}
}
- public override List<TypeProxy!>! FreeProxies { get {
- return new List<TypeProxy!> ();
- } }
+ public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
+ return new List<TypeProxy/*!*/>();
+ }
+ }
//----------- Getters/Issers ----------------------------------
- public override bool IsBasic { get { return true; } }
- public override bool IsInt { get { return this.T == SimpleType.Int; } }
- public override bool IsBool { get { return this.T == SimpleType.Bool; } }
+ public override bool IsBasic {
+ get {
+ return true;
+ }
+ }
+ public override bool IsInt {
+ get {
+ return this.T == SimpleType.Int;
+ }
+ }
+ public override bool IsBool {
+ get {
+ return this.T == SimpleType.Bool;
+ }
+ }
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitBasicType(this);
}
}
-
+
//=====================================================================
- public class BvType : Type
- {
+ public class BvType : Type {
public readonly int Bits;
-
- public BvType(IToken! token, int bits)
- : base(token)
- {
+
+ public BvType(IToken token, int bits)
+ : base(token) {
+ Contract.Requires(token != null);
Bits = bits;
}
-
+
public BvType(int bits)
- : base(Token.NoToken)
- {
- Bits = bits; + : base(Token.NoToken) {
+ Bits = bits;
}
//----------- Cloning ----------------------------------
@@ -793,47 +1019,56 @@ namespace Microsoft.Boogie // have to be created in the right way. It is /not/ ok to just clone
// everything recursively.
- public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
// BvTypes are immutable anyway, we do not clone
return this;
}
- public override Type! CloneUnresolved() {
+ public override Type CloneUnresolved() {
+ Contract.Ensures(Contract.Result<Type>() != null);
return this;
}
//----------- Linearisation ----------------------------------
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
+ //Contract.Requires(stream != null);
// no parentheses are necessary for bitvector-types
stream.SetToken(this);
stream.Write("{0}", this);
}
[Pure]
- public override string! ToString()
- {
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
return "bv" + Bits;
}
//----------- Equality ----------------------------------
[Pure]
- public override bool Equals(Type! that,
- TypeVariableSeq! thisBoundVariables,
- TypeVariableSeq! thatBoundVariables) {
+ public override bool Equals(Type/*!*/ that,
+ TypeVariableSeq/*!*/ thisBoundVariables,
+ TypeVariableSeq/*!*/ thatBoundVariables) {
+ //Contract.Requires(thisBoundVariables != null);
+ //Contract.Requires(thatBoundVariables != null);
+ //Contract.Requires(that != null);
BvType thatBvType = TypeProxy.FollowProxy(that.Expanded) as BvType;
return thatBvType != null && this.Bits == thatBvType.Bits;
}
//----------- Unification of types -----------
- public override bool Unify(Type! that,
- TypeVariableSeq! unifiableVariables,
- // an idempotent substitution that describes the
- // unification result up to a certain point
- IDictionary<TypeVariable!, Type!>! unifier) {
+ public override bool Unify(Type/*!*/ that,
+ TypeVariableSeq/*!*/ unifiableVariables,
+ // an idempotent substitution that describes the
+ // unification result up to a certain point
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {
+ //Contract.Requires(that != null);
+ //Contract.Requires(unifiableVariables != null);
+ Contract.Requires(cce.NonNullElements(unifier));
that = that.Expanded;
if (that is TypeProxy || that is TypeVariable) {
return that.Unify(this, unifiableVariables, unifier);
@@ -843,11 +1078,13 @@ namespace Microsoft.Boogie }
#if OLD_UNIFICATION
- public override void Unify(Type! that,
+ public override void Unify(Type that,
TypeVariableSeq! unifiableVariables,
TypeVariableSeq! thisBoundVariables,
TypeVariableSeq! thatBoundVariables,
- IDictionary<TypeVariable!, Type!>! result) {
+ IDictionary<TypeVariable!, Type!> result){
+Contract.Requires(result != null);
+Contract.Requires(that != null);
that = that.Expanded;
if (that is TypeVariable) {
that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result);
@@ -860,45 +1097,61 @@ namespace Microsoft.Boogie //----------- Substitution of free variables with types not containing bound variables -----------------
- public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
+ //Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
return this;
}
//----------- Hashcodes ----------------------------------
[Pure]
- public override int GetHashCode(TypeVariableSeq! boundVariables)
- {
+ public override int GetHashCode(TypeVariableSeq boundVariables) {
+ //Contract.Requires(boundVariables != null);
return this.Bits.GetHashCode();
}
//----------- Resolution ----------------------------------
- public override Type! ResolveType(ResolutionContext! rc) {
+ public override Type ResolveType(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
// nothing to resolve
return this;
}
// determine the free variables in a type, in the order in which the variables occur
- public override TypeVariableSeq! FreeVariables {
+ public override TypeVariableSeq/*!*/ FreeVariables {
get {
- return new TypeVariableSeq (); // bitvector-type are closed
+ Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
+
+ return new TypeVariableSeq(); // bitvector-type are closed
}
}
- public override List<TypeProxy!>! FreeProxies { get {
- return new List<TypeProxy!> ();
- } }
+ public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
+ return new List<TypeProxy/*!*/>();
+ }
+ }
//----------- Getters/Issers ----------------------------------
- public override bool IsBv { get { return true; } }
- public override int BvBits { get {
- return Bits;
- } }
+ public override bool IsBv {
+ get {
+ return true;
+ }
+ }
+ public override int BvBits {
+ get {
+ return Bits;
+ }
+ }
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitBvType(this);
}
}
@@ -909,16 +1162,26 @@ namespace Microsoft.Boogie // will be turned either into a TypeVariable, into a CtorType or into a BvType
// during the resolution phase
public class UnresolvedTypeIdentifier : Type {
- public readonly string! Name;
- public readonly TypeSeq! Arguments;
+ public readonly string/*!*/ Name;
+ public readonly TypeSeq/*!*/ Arguments;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Name != null);
+ Contract.Invariant(Arguments != null);
+ }
+
- public UnresolvedTypeIdentifier(IToken! token, string! name) {
- this(token, name, new TypeSeq ());
+ public UnresolvedTypeIdentifier(IToken token, string name)
+ : this(token, name, new TypeSeq()) {
+ Contract.Requires(name != null);
+ Contract.Requires(token != null);
}
- public UnresolvedTypeIdentifier(IToken! token, string! name, TypeSeq! arguments)
- : base(token)
- {
+ public UnresolvedTypeIdentifier(IToken token, string name, TypeSeq arguments)
+ : base(token) {
+ Contract.Requires(arguments != null);
+ Contract.Requires(name != null);
+ Contract.Requires(token != null);
this.Name = name;
this.Arguments = arguments;
}
@@ -928,64 +1191,93 @@ namespace Microsoft.Boogie // have to be created in the right way. It is /not/ ok to just clone
// everything recursively
- public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
- TypeSeq! newArgs = new TypeSeq ();
- foreach(Type! t in Arguments)
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
+ TypeSeq/*!*/ newArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
newArgs.Add(t.Clone(varMap));
+ }
return new UnresolvedTypeIdentifier(tok, Name, newArgs);
}
- public override Type! CloneUnresolved() {
- TypeSeq! newArgs = new TypeSeq ();
- foreach(Type! t in Arguments)
+ public override Type CloneUnresolved() {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ TypeSeq/*!*/ newArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
newArgs.Add(t.CloneUnresolved());
+ }
return new UnresolvedTypeIdentifier(tok, Name, newArgs);
}
//----------- Equality ----------------------------------
[Pure]
- public override bool Equals(Type! that,
- TypeVariableSeq! thisBoundVariables,
- TypeVariableSeq! thatBoundVariables) {
+ public override bool Equals(Type that,
+ TypeVariableSeq/*!*/ thisBoundVariables,
+ TypeVariableSeq/*!*/ thatBoundVariables) {
+ Contract.Requires(thisBoundVariables != null);
+ Contract.Requires(thatBoundVariables != null);
+ Contract.Requires(that != null);
System.Diagnostics.Debug.Fail("UnresolvedTypeIdentifier.Equals should never be called");
return false; // to make the compiler happy
}
//----------- Unification of types -----------
- public override bool Unify(Type! that,
- TypeVariableSeq! unifiableVariables,
- IDictionary<TypeVariable!, Type!>! result) {
- assert false; // UnresolvedTypeIdentifier.Unify should never be called
+ public override bool Unify(Type that,
+ TypeVariableSeq/*!*/ unifiableVariables,
+ IDictionary<TypeVariable/*!*/, Type/*!*/> result) {
+ Contract.Requires(unifiableVariables != null);
+ Contract.Requires(cce.NonNullElements(result));
+ Contract.Requires(that != null);
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // UnresolvedTypeIdentifier.Unify should never be called
}
#if OLD_UNIFICATION
- public override void Unify(Type! that,
+ public override void Unify(Type that,
TypeVariableSeq! unifiableVariables,
TypeVariableSeq! thisBoundVariables,
TypeVariableSeq! thatBoundVariables,
- IDictionary<TypeVariable!, Type!>! result) {
+ IDictionary<TypeVariable!, Type!> result){
+Contract.Requires(result != null);
+Contract.Requires(that != null);
System.Diagnostics.Debug.Fail("UnresolvedTypeIdentifier.Unify should never be called");
}
#endif
//----------- Substitution of free variables with types not containing bound variables -----------------
- public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
- assert false; // UnresolvedTypeIdentifier.Substitute should never be called
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
+ Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // UnresolvedTypeIdentifier.Substitute should never be called
}
//----------- Hashcodes ----------------------------------
[Pure]
- public override int GetHashCode(TypeVariableSeq! boundVariables) {
- assert false; // UnresolvedTypeIdentifier.GetHashCode should never be called
+ public override int GetHashCode(TypeVariableSeq boundVariables) {
+ Contract.Requires(boundVariables != null);
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // UnresolvedTypeIdentifier.GetHashCode should never be called
}
//----------- Resolution ----------------------------------
- public override Type! ResolveType(ResolutionContext! rc) {
+ public override Type ResolveType(ResolutionContext rc) {
+ Contract.Requires(rc != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
// first case: the type name denotes a bitvector-type
if (Name.StartsWith("bv") && Name.Length > 2) {
bool is_bv = true;
@@ -1026,7 +1318,7 @@ namespace Microsoft.Boogie ctorDecl);
return this;
}
- return new CtorType (tok, ctorDecl, ResolveArguments(rc));
+ return new CtorType(tok, ctorDecl, ResolveArguments(rc));
}
// fourth case: the identifier denotes a type synonym
@@ -1038,8 +1330,8 @@ namespace Microsoft.Boogie synDecl);
return this;
}
- TypeSeq! resolvedArgs = ResolveArguments(rc);
-
+ TypeSeq/*!*/ resolvedArgs = ResolveArguments(rc);
+ Contract.Assert(resolvedArgs != null);
return new TypeSynonymAnnotation(this.tok, synDecl, resolvedArgs);
@@ -1050,27 +1342,36 @@ namespace Microsoft.Boogie return this;
}
- private TypeSeq! ResolveArguments(ResolutionContext! rc) {
- TypeSeq! resolvedArgs = new TypeSeq ();
- foreach (Type! t in Arguments)
+ private TypeSeq ResolveArguments(ResolutionContext rc) {
+ Contract.Requires(rc != null);
+ Contract.Ensures(Contract.Result<TypeSeq>() != null);
+ TypeSeq/*!*/ resolvedArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
resolvedArgs.Add(t.ResolveType(rc));
+ }
return resolvedArgs;
}
- public override TypeVariableSeq! FreeVariables {
+ public override TypeVariableSeq/*!*/ FreeVariables {
get {
- return new TypeVariableSeq ();
- }
+ Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
+
+ return new TypeVariableSeq();
+ }
}
- public override List<TypeProxy!>! FreeProxies { get {
- return new List<TypeProxy!> ();
- } }
+ public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
+ return new List<TypeProxy/*!*/>();
+ }
+ }
//----------- Linearisation ----------------------------------
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
+ //Contract.Requires(stream != null);
stream.SetToken(this);
// PR: should unresolved types be syntactically distinguished from resolved types?
CtorType.EmitCtorType(this.Name, Arguments, stream, contextBindingStrength);
@@ -1078,11 +1379,21 @@ namespace Microsoft.Boogie //----------- Getters/Issers ----------------------------------
- public override bool IsUnresolved { get { return true; } }
- public override UnresolvedTypeIdentifier! AsUnresolved { get { return this; } }
+ public override bool IsUnresolved {
+ get {
+ return true;
+ }
+ }
+ public override UnresolvedTypeIdentifier/*!*/ AsUnresolved {
+ get {
+ Contract.Ensures(Contract.Result<UnresolvedTypeIdentifier>() != null);
+ return this;
+ }
+ }
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitUnresolvedTypeIdentifier(this);
}
}
@@ -1090,11 +1401,17 @@ namespace Microsoft.Boogie //=====================================================================
public class TypeVariable : Type {
- public readonly string! Name;
+ public readonly string/*!*/ Name;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Name != null);
+ }
- public TypeVariable(IToken! token, string! name)
- : base(token)
- {
+
+ public TypeVariable(IToken token, string name)
+ : base(token) {
+ Contract.Requires(name != null);
+ Contract.Requires(token != null);
this.Name = name;
}
@@ -1103,7 +1420,9 @@ namespace Microsoft.Boogie // have to be created in the right way. It is /not/ ok to just clone
// everything recursively
- public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
// if this variable is mapped to some new variable, we take the new one
// otherwise, return this
TypeVariable res;
@@ -1114,18 +1433,22 @@ namespace Microsoft.Boogie return res;
}
- public override Type! CloneUnresolved() {
+ public override Type CloneUnresolved() {
+ Contract.Ensures(Contract.Result<Type>() != null);
return this;
}
//----------- Equality ----------------------------------
[Pure]
- public override bool Equals(Type! that,
- TypeVariableSeq! thisBoundVariables,
- TypeVariableSeq! thatBoundVariables) {
+ public override bool Equals(Type that,
+ TypeVariableSeq/*!*/ thisBoundVariables,
+ TypeVariableSeq/*!*/ thatBoundVariables) {
+ //Contract.Requires(thisBoundVariables != null);
+ //Contract.Requires(thatBoundVariables != null);
+ //Contract.Requires(that != null);
TypeVariable thatAsTypeVar = TypeProxy.FollowProxy(that.Expanded) as TypeVariable;
-
+
if (thatAsTypeVar == null)
return false;
@@ -1138,11 +1461,14 @@ namespace Microsoft.Boogie //----------- Unification of types -----------
- public override bool Unify(Type! that,
- TypeVariableSeq! unifiableVariables,
- // an idempotent substitution that describes the
- // unification result up to a certain point
- IDictionary<TypeVariable!, Type!>! unifier) {
+ public override bool Unify(Type/*!*/ that,
+ TypeVariableSeq/*!*/ unifiableVariables,
+ // an idempotent substitution that describes the
+ // unification result up to a certain point
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {
+ //Contract.Requires(that != null);
+ //Contract.Requires(unifiableVariables != null);
+ //Contract.Requires(cce.NonNullElements(unifier));
that = that.Expanded;
if (that is TypeProxy && !(that is ConstrainedProxy))
return that.Unify(this, unifiableVariables, unifier);
@@ -1163,9 +1489,9 @@ namespace Microsoft.Boogie // this cannot be instantiated with anything
// but that possibly can ...
-
+
TypeVariable tv = that as TypeVariable;
-
+
return tv != null &&
unifiableVariables.Has(tv) &&
that.Unify(this, unifiableVariables, unifier);
@@ -1174,43 +1500,50 @@ namespace Microsoft.Boogie // TODO: the following might cause problems, because when applying substitutions
// to type proxies the substitutions are not propagated to the proxy
// constraints (right now at least)
- private bool addSubstitution(IDictionary<TypeVariable!, Type!>! oldSolution,
- // the type that "this" is instantiated with
- Type! newSubst)
- requires !oldSolution.ContainsKey(this); {
-
- Dictionary<TypeVariable!, Type!>! newMapping = new Dictionary<TypeVariable!, Type!> ();
+ private bool addSubstitution(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ oldSolution,
+ // the type that "this" is instantiated with
+ Type/*!*/ newSubst) {
+ Contract.Requires(cce.NonNullElements(oldSolution));
+ Contract.Requires(newSubst != null);
+ Contract.Requires(!oldSolution.ContainsKey(this));
+
+ Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ newMapping = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
// apply the old (idempotent) substitution to the new instantiation
- Type! substSubst = newSubst.Substitute(oldSolution);
+ Type/*!*/ substSubst = newSubst.Substitute(oldSolution);
+ Contract.Assert(substSubst != null);
// occurs check
if (substSubst.FreeVariables.Has(this))
return false;
newMapping.Add(this, substSubst);
// apply the new substitution to the old ones to ensure idempotence
- List<TypeVariable!>! keys = new List<TypeVariable!> ();
+ List<TypeVariable/*!*/>/*!*/ keys = new List<TypeVariable/*!*/>();
keys.AddRange(oldSolution.Keys);
- foreach (TypeVariable! var in keys)
+ foreach (TypeVariable/*!*/ var in keys) {
+ Contract.Assert(var != null);
oldSolution[var] = oldSolution[var].Substitute(newMapping);
+ }
oldSolution.Add(this, substSubst);
- assert IsIdempotent(oldSolution);
+ Contract.Assert(IsIdempotent(oldSolution));
return true;
}
#if OLD_UNIFICATION
- public override void Unify(Type! that,
+ public override void Unify(Type that,
TypeVariableSeq! unifiableVariables,
TypeVariableSeq! thisBoundVariables,
TypeVariableSeq! thatBoundVariables,
- IDictionary<TypeVariable!, Type!>! result) {
+ IDictionary<TypeVariable!, Type!> result){
+Contract.Requires(result != null);
+Contract.Requires(that != null);
that = that.Expanded;
int thisIndex = thisBoundVariables.LastIndexOf(this);
if (thisIndex == -1) {
// this is not a bound variable and can possibly be matched on that
// that must not contain any bound variables
TypeVariableSeq! thatFreeVars = that.FreeVariables;
- if (exists{TypeVariable! var in thatBoundVariables; thatFreeVars.Has(var)})
+ if (Contract.Exists(thatBoundVariables, var=> thatFreeVars.Has(var)))
throw UNIFICATION_FAILED;
// otherwise, in case that is a typevariable it cannot be bound and
@@ -1250,10 +1583,12 @@ namespace Microsoft.Boogie //----------- Substitution of free variables with types not containing bound variables -----------------
- public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
+ //Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
Type res;
if (subst.TryGetValue(this, out res)) {
- assert res != null;
+ Contract.Assert(res != null);
return res;
} else {
return this;
@@ -1263,7 +1598,8 @@ namespace Microsoft.Boogie //----------- Hashcodes ----------------------------------
[Pure]
- public override int GetHashCode(TypeVariableSeq! boundVariables) {
+ public override int GetHashCode(TypeVariableSeq boundVariables) {
+ //Contract.Requires(boundVariables != null);
int thisIndex = boundVariables.LastIndexOf(this);
if (thisIndex == -1)
return GetBaseHashCode();
@@ -1272,8 +1608,8 @@ namespace Microsoft.Boogie //----------- Linearisation ----------------------------------
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
+ //Contract.Requires(stream != null);
// never put parentheses around variables
stream.SetToken(this);
stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
@@ -1281,26 +1617,44 @@ namespace Microsoft.Boogie //----------- Resolution ----------------------------------
- public override Type! ResolveType(ResolutionContext! rc) {
+ public override Type ResolveType(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ //Contract.Ensures(Contract.Result<Type>() != null);
// nothing to resolve
return this;
}
- public override TypeVariableSeq! FreeVariables {
- get { return new TypeVariableSeq(this); }
+ public override TypeVariableSeq/*!*/ FreeVariables {
+ get {
+ Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
+ return new TypeVariableSeq(this);
+ }
}
- public override List<TypeProxy!>! FreeProxies { get {
- return new List<TypeProxy!> ();
- } }
+ public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
+ return new List<TypeProxy/*!*/>();
+ }
+ }
//----------- Getters/Issers ----------------------------------
- public override bool IsVariable { get { return true; } }
- public override TypeVariable! AsVariable { get { return this; } }
+ public override bool IsVariable {
+ get {
+ return true;
+ }
+ }
+ public override TypeVariable/*!*/ AsVariable {
+ get {
+ Contract.Ensures(Contract.Result<TypeVariable>() != null);
+ return this;
+ }
+ }
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ //Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitTypeVariable(this);
}
}
@@ -1309,18 +1663,27 @@ namespace Microsoft.Boogie public class TypeProxy : Type {
static int proxies = 0;
- protected readonly string! Name;
-
- public TypeProxy(IToken! token, string! givenName)
- {
- this(token, givenName, "proxy");
+ protected readonly string/*!*/ Name;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Name != null);
}
-
- protected TypeProxy(IToken! token, string! givenName, string! kind)
- {
+
+
+ public TypeProxy(IToken token, string givenName)
+ : this(token, givenName, "proxy") {
+ Contract.Requires(givenName != null);
+ Contract.Requires(token != null);
+ }
+
+ protected TypeProxy(IToken token, string givenName, string kind)
+ : base(token) {//BASEMOVE DANGER
+ Contract.Requires(kind != null);
+ Contract.Requires(givenName != null);
+ Contract.Requires(token != null);
Name = givenName + "$" + kind + "#" + proxies;
proxies++;
- base(token);
+ //:base(token);
}
private Type proxyFor;
@@ -1331,16 +1694,18 @@ namespace Microsoft.Boogie if (anotherProxy != null && anotherProxy.proxyFor != null) {
// apply path shortening by bypassing "anotherProxy" (and possibly others)
proxyFor = anotherProxy.ProxyFor;
- assert proxyFor != null;
+ Contract.Assert(proxyFor != null);
}
return proxyFor;
}
}
-
- [Pure][Reads(ReadsAttribute.Reads.Everything)]
- public static Type! FollowProxy(Type! t)
- ensures result is TypeProxy ==> ((TypeProxy)result).proxyFor == null;
- {
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Everything)]
+ public static Type FollowProxy(Type t) {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ Contract.Ensures(!(Contract.Result<Type>() is TypeProxy) || ((TypeProxy)Contract.Result<Type>()).proxyFor == null);
if (t is TypeProxy) {
Type p = ((TypeProxy)t).ProxyFor;
if (p != null) {
@@ -1349,20 +1714,22 @@ namespace Microsoft.Boogie }
return t;
}
-
- protected void DefineProxy(Type! ty)
- requires ProxyFor == null;
- {
+
+ protected void DefineProxy(Type ty) {
+ Contract.Requires(ty != null);
+ Contract.Requires(ProxyFor == null);
// follow ty down to the leaf level, so that we can avoid creating a cycle
ty = FollowProxy(ty);
if (!object.ReferenceEquals(this, ty)) {
proxyFor = ty;
}
}
-
+
//----------- Cloning ----------------------------------
- public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
Type p = ProxyFor;
if (p != null) {
return p.Clone(varMap);
@@ -1371,16 +1738,20 @@ namespace Microsoft.Boogie }
}
- public override Type! CloneUnresolved() {
+ public override Type CloneUnresolved() {
+ Contract.Ensures(Contract.Result<Type>() != null);
return new TypeProxy(this.tok, this.Name); // the clone will have a name that ends with $proxy<n>$proxy<m>
}
//----------- Equality ----------------------------------
[Pure]
- public override bool Equals(Type! that,
- TypeVariableSeq! thisBoundVariables,
- TypeVariableSeq! thatBoundVariables) {
+ public override bool Equals(Type that,
+ TypeVariableSeq/*!*/ thisBoundVariables,
+ TypeVariableSeq/*!*/ thatBoundVariables) {
+ //Contract.Requires(thisBoundVariables != null);
+ //Contract.Requires(thatBoundVariables != null);
+ //Contract.Requires(that != null);
if (object.ReferenceEquals(this, that)) {
return true;
}
@@ -1396,15 +1767,19 @@ namespace Microsoft.Boogie //----------- Unification of types -----------
// determine whether the occurs check fails: this is a strict subtype of that
- protected bool ReallyOccursIn(Type! that) {
+ protected bool ReallyOccursIn(Type that) {
+ Contract.Requires(that != null);
that = FollowProxy(that.Expanded);
return that.FreeProxies.Contains(this) &&
(that.IsCtor || that.IsMap && this != that && this.ProxyFor != that);
}
- public override bool Unify(Type! that,
- TypeVariableSeq! unifiableVariables,
- IDictionary<TypeVariable!, Type!>! result) {
+ public override bool Unify(Type that,
+ TypeVariableSeq/*!*/ unifiableVariables,
+ IDictionary<TypeVariable/*!*/, Type/*!*/> result) {
+ //Contract.Requires(cce.NonNullElements(result));
+ //Contract.Requires(unifiableVariables != null);
+ //Contract.Requires(that != null);
Type p = ProxyFor;
if (p != null) {
return p.Unify(that, unifiableVariables, result);
@@ -1419,7 +1794,9 @@ namespace Microsoft.Boogie //----------- Substitution of free variables with types not containing bound variables -----------------
- public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
+ //Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
Type p = ProxyFor;
if (p != null) {
return p.Substitute(subst);
@@ -1431,7 +1808,8 @@ namespace Microsoft.Boogie //----------- Hashcodes ----------------------------------
[Pure]
- public override int GetHashCode(TypeVariableSeq! boundVariables) {
+ public override int GetHashCode(TypeVariableSeq boundVariables) {
+ //Contract.Requires(boundVariables != null);
Type p = ProxyFor;
if (p != null) {
return p.GetHashCode(boundVariables);
@@ -1442,8 +1820,8 @@ namespace Microsoft.Boogie //----------- Linearisation ----------------------------------
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
+ //Contract.Requires(stream != null);
Type p = ProxyFor;
if (p != null) {
p.Emit(stream, contextBindingStrength);
@@ -1456,7 +1834,9 @@ namespace Microsoft.Boogie //----------- Resolution ----------------------------------
- public override Type! ResolveType(ResolutionContext! rc) {
+ public override Type ResolveType(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
Type p = ProxyFor;
if (p != null) {
return p.ResolveType(rc);
@@ -1465,108 +1845,153 @@ namespace Microsoft.Boogie }
}
- public override TypeVariableSeq! FreeVariables {
- get {
- Type p = ProxyFor;
- if (p != null) {
- return p.FreeVariables;
- } else {
- return new TypeVariableSeq();
- }
- }
+ public override TypeVariableSeq/*!*/ FreeVariables {
+ get {
+ Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
+
+ Type p = ProxyFor;
+ if (p != null) {
+ return p.FreeVariables;
+ } else {
+ return new TypeVariableSeq();
+ }
+ }
}
- public override List<TypeProxy!>! FreeProxies { get {
- Type p = ProxyFor;
- if (p != null) {
- return p.FreeProxies;
- } else {
- List<TypeProxy!>! res = new List<TypeProxy!> ();
- res.Add(this);
- return res;
- }
- } }
+ public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
+ Type p = ProxyFor;
+ if (p != null) {
+ return p.FreeProxies;
+ } else {
+ List<TypeProxy/*!*/>/*!*/ res = new List<TypeProxy/*!*/>();
+ res.Add(this);
+ return res;
+ }
+ }
+ }
//----------- Getters/Issers ----------------------------------
- public override bool IsBasic { get {
- Type p = ProxyFor;
- return p != null && p.IsBasic;
- } }
- public override bool IsInt { get {
- Type p = ProxyFor;
- return p != null && p.IsInt;
- } }
- public override bool IsBool { get {
- Type p = ProxyFor;
- return p != null && p.IsBool;
- } }
+ public override bool IsBasic {
+ get {
+ Type p = ProxyFor;
+ return p != null && p.IsBasic;
+ }
+ }
+ public override bool IsInt {
+ get {
+ Type p = ProxyFor;
+ return p != null && p.IsInt;
+ }
+ }
+ public override bool IsBool {
+ get {
+ Type p = ProxyFor;
+ return p != null && p.IsBool;
+ }
+ }
- public override bool IsVariable { get {
- Type p = ProxyFor;
- return p != null && p.IsVariable;
- } }
- public override TypeVariable! AsVariable { get {
- Type p = ProxyFor;
- assume p != null;
- return p.AsVariable;
- } }
+ public override bool IsVariable {
+ get {
+ Type p = ProxyFor;
+ return p != null && p.IsVariable;
+ }
+ }
+ public override TypeVariable/*!*/ AsVariable {
+ get {
+ Contract.Ensures(Contract.Result<TypeVariable>() != null);
- public override bool IsCtor { get {
- Type p = ProxyFor;
- return p != null && p.IsCtor;
- } }
- public override CtorType! AsCtor { get {
- Type p = ProxyFor;
- assume p != null;
- return p.AsCtor;
- } }
- public override bool IsMap { get {
- Type p = ProxyFor;
- return p != null && p.IsMap;
- } }
- public override MapType! AsMap { get {
- Type p = ProxyFor;
- assume p != null;
- return p.AsMap;
- } }
- public override int MapArity { get {
- Type p = ProxyFor;
- assume p != null;
- return p.MapArity;
- } }
- public override bool IsUnresolved { get {
- Type p = ProxyFor;
- return p != null && p.IsUnresolved;
- } }
- public override UnresolvedTypeIdentifier! AsUnresolved { get {
- Type p = ProxyFor;
- assume p != null;
- return p.AsUnresolved;
- } }
+ Type p = ProxyFor;
+ Contract.Assume(p != null);
+ return p.AsVariable;
+ }
+ }
- public override bool IsBv { get {
- Type p = ProxyFor;
- return p != null && p.IsBv;
- } }
- public override int BvBits { get {
- Type p = ProxyFor;
- assume p != null;
- return p.BvBits;
- } }
+ public override bool IsCtor {
+ get {
+ Type p = ProxyFor;
+ return p != null && p.IsCtor;
+ }
+ }
+ public override CtorType/*!*/ AsCtor {
+ get {
+ Contract.Ensures(Contract.Result<CtorType>() != null);
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ Type p = ProxyFor;
+ Contract.Assume(p != null);
+ return p.AsCtor;
+ }
+ }
+ public override bool IsMap {
+ get {
+ Type p = ProxyFor;
+ return p != null && p.IsMap;
+ }
+ }
+ public override MapType/*!*/ AsMap {
+ get {
+ Contract.Ensures(Contract.Result<MapType>() != null);
+
+ Type p = ProxyFor;
+ Contract.Assume(p != null);
+ return p.AsMap;
+ }
+ }
+ public override int MapArity {
+ get {
+ Type p = ProxyFor;
+ Contract.Assume(p != null);
+ return p.MapArity;
+ }
+ }
+ public override bool IsUnresolved {
+ get {
+ Type p = ProxyFor;
+ return p != null && p.IsUnresolved;
+ }
+ }
+ public override UnresolvedTypeIdentifier/*!*/ AsUnresolved {
+ get {
+ Contract.Ensures(Contract.Result<UnresolvedTypeIdentifier>() != null);
+
+ Type p = ProxyFor;
+ Contract.Assume(p != null);
+ return p.AsUnresolved;
+ }
+ }
+
+ public override bool IsBv {
+ get {
+ Type p = ProxyFor;
+ return p != null && p.IsBv;
+ }
+ }
+ public override int BvBits {
+ get {
+ Type p = ProxyFor;
+ Contract.Assume(p != null);
+ return p.BvBits;
+ }
+ }
+
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitTypeProxy(this);
}
}
public abstract class ConstrainedProxy : TypeProxy {
- protected ConstrainedProxy(IToken! token, string! givenName, string! kind) {
- base(token, givenName, kind);
+ protected ConstrainedProxy(IToken token, string givenName, string kind)
+ : base(token, givenName, kind) {
+ Contract.Requires(kind != null);
+ Contract.Requires(givenName != null);
+ Contract.Requires(token != null);
}
}
-
+
/// <summary>
/// Each instance of this class represents a set of bitvector types. In particular, it represents
/// a bitvector type bvN iff
@@ -1587,21 +2012,29 @@ namespace Microsoft.Boogie /// </summary>
public class BvTypeProxy : ConstrainedProxy {
public int MinBits;
- List<BvTypeConstraint!> constraints;
+ List<BvTypeConstraint/*!*/> constraints;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(constraints, true));
+ }
+
class BvTypeConstraint {
- public Type! T0;
- public Type! T1;
- public BvTypeConstraint(Type! t0, Type! t1)
- requires t0.IsBv && t1.IsBv;
- {
+ public Type/*!*/ T0;
+ public Type/*!*/ T1;
+ public BvTypeConstraint(Type t0, Type t1) {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t0 != null);
+ Contract.Requires(t0.IsBv && t1.IsBv);
T0 = t0;
T1 = t1;
}
}
-
- public BvTypeProxy(IToken! token, string! name, int minBits)
- {
- base(token, name, "bv" + minBits + "proxy");
+
+ public BvTypeProxy(IToken token, string name, int minBits)
+ : base(token, name, "bv" + minBits + "proxy") {//BASEMOVEA
+ Contract.Requires(name != null);
+ Contract.Requires(token != null);
+ //base(token, name, "bv" + minBits + "proxy");
this.MinBits = minBits;
}
@@ -1609,39 +2042,49 @@ namespace Microsoft.Boogie /// Requires that any further constraints to be placed on t0 and t1 go via the object to
/// be constructed.
/// </summary>
- public BvTypeProxy(IToken! token, string! name, Type! t0, Type! t1)
- requires t0.IsBv && t1.IsBv;
- {
- base(token, name, "bvproxy");
+ public BvTypeProxy(IToken token, string name, Type t0, Type t1)
+ : base(token, name, "bvproxy") {//BASEMOVEA
+ Contract.Requires(t1 != null);
+ Contract.Requires(t0 != null);
+ Contract.Requires(name != null);
+ Contract.Requires(token != null);
+ Contract.Requires(t0.IsBv && t1.IsBv);
+ //:base(token, name, "bvproxy");
t0 = FollowProxy(t0);
t1 = FollowProxy(t1);
this.MinBits = MinBitsFor(t0) + MinBitsFor(t1);
- List<BvTypeConstraint!> list = new List<BvTypeConstraint!>();
+ List<BvTypeConstraint/*!*/> list = new List<BvTypeConstraint/*!*/>();
list.Add(new BvTypeConstraint(t0, t1));
this.constraints = list;
}
-
+
/// <summary>
/// Construct a BvTypeProxy like p, but with minBits.
/// </summary>
- private BvTypeProxy(BvTypeProxy! p, int minBits)
- {
- base(p.tok, p.Name, "");
+ private BvTypeProxy(BvTypeProxy p, int minBits)
+ : base(p.tok, p.Name, "") {//BASEMOVEA
+ Contract.Requires(p != null);
+ //:base(p.tok, p.Name, "");
this.MinBits = minBits;
this.constraints = p.constraints;
}
-
- private BvTypeProxy(IToken! token, string! name, int minBits, List<BvTypeConstraint!> constraints) {
- base(token, name, "");
+
+ private BvTypeProxy(IToken token, string name, int minBits, List<BvTypeConstraint/*!*/> constraints)
+ : base(token, name, "") {//BASEMOVEA
+ Contract.Requires(cce.NonNullElements(constraints, true));
+ Contract.Requires(name != null);
+ Contract.Requires(token != null);
+ //:base(token, name, "");
this.MinBits = minBits;
this.constraints = constraints;
}
-
- [Pure][Reads(ReadsAttribute.Reads.Everything)]
- private static int MinBitsFor(Type! t)
- requires t.IsBv;
- ensures 0 <= result;
- {
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Everything)]
+ private static int MinBitsFor(Type t) {
+ Contract.Requires(t != null);
+ Contract.Requires(t.IsBv);
+ Contract.Ensures(0 <= Contract.Result<int>());
if (t is BvType) {
return t.BvBits;
} else {
@@ -1651,7 +2094,9 @@ namespace Microsoft.Boogie //----------- Cloning ----------------------------------
- public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
Type p = ProxyFor;
if (p != null) {
return p.Clone(varMap);
@@ -1660,15 +2105,19 @@ namespace Microsoft.Boogie }
}
- public override Type! CloneUnresolved() {
+ public override Type CloneUnresolved() {
+ Contract.Ensures(Contract.Result<Type>() != null);
return new BvTypeProxy(this.tok, this.Name, this.MinBits, this.constraints); // the clone will have a name that ends with $bvproxy<n>$bvproxy<m>
}
//----------- Unification of types -----------
- public override bool Unify(Type! that,
- TypeVariableSeq! unifiableVariables,
- IDictionary<TypeVariable!, Type!>! result) {
+ public override bool Unify(Type that,
+ TypeVariableSeq unifiableVariables,
+ IDictionary<TypeVariable, Type> result) {
+ //Contract.Requires(cce.NonNullElements(result));
+ //Contract.Requires(unifiableVariables != null);
+ //Contract.Requires(that != null);
Type p = ProxyFor;
if (p != null) {
return p.Unify(that, unifiableVariables, result);
@@ -1695,7 +2144,7 @@ namespace Microsoft.Boogie int minT1 = MinBitsFor(btc.T1);
int left = IncreaseBits(btc.T0, that.BvBits - minT1);
left = IncreaseBits(btc.T1, minT1 + left);
- assert left == 0; // because it should always be possible to increase the total size of a BvTypeConstraint pair (t0,t1) arbitrarily
+ Contract.Assert(left == 0); // because it should always be possible to increase the total size of a BvTypeConstraint pair (t0,t1) arbitrarily
}
}
DefineProxy(that);
@@ -1707,10 +2156,14 @@ namespace Microsoft.Boogie // has a constraints list, then concatenate both constraints lists and define the previous
// proxies to the new one
if (this.constraints != null || bt.constraints != null) {
- List<BvTypeConstraint!> list = new List<BvTypeConstraint!>();
- if (this.constraints != null) { list.AddRange(this.constraints); }
- if (bt.constraints != null) { list.AddRange(bt.constraints); }
- BvTypeProxy np = new BvTypeProxy(this.tok, this.Name, max{this.MinBits, bt.MinBits}, list);
+ List<BvTypeConstraint/*!*/> list = new List<BvTypeConstraint/*!*/>();
+ if (this.constraints != null) {
+ list.AddRange(this.constraints);
+ }
+ if (bt.constraints != null) {
+ list.AddRange(bt.constraints);
+ }
+ BvTypeProxy np = new BvTypeProxy(this.tok, this.Name, Math.Max(this.MinBits, bt.MinBits), list);
this.DefineProxy(np);
bt.DefineProxy(np);
} else if (this.MinBits <= bt.MinBits) {
@@ -1729,16 +2182,16 @@ namespace Microsoft.Boogie return false;
}
- private static int IncreaseBits(Type! t, int to)
- requires t.IsBv && 0 <= to && MinBitsFor(t) <= to;
- ensures 0 <= result && result <= to;
- {
+ private static int IncreaseBits(Type t, int to) {
+ Contract.Requires(t != null);
+ Contract.Requires(t.IsBv && 0 <= to && MinBitsFor(t) <= to);
+ Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= to);
t = FollowProxy(t);
if (t is BvType) {
return to - t.BvBits;
} else {
BvTypeProxy p = (BvTypeProxy)t;
- assert p.MinBits <= to;
+ Contract.Assert(p.MinBits <= to);
if (p.MinBits < to) {
BvTypeProxy q = new BvTypeProxy(p, to);
p.DefineProxy(q);
@@ -1749,36 +2202,43 @@ namespace Microsoft.Boogie //----------- Substitution of free variables with types not containing bound variables -----------------
- public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
+ //Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
if (this.ProxyFor == null) {
// check that the constraints are clean and do not contain any
// of the substituted variables (otherwise, we are in big trouble)
- assert forall{BvTypeConstraint! c in constraints;
- forall{TypeVariable! var in subst.Keys;
- !c.T0.FreeVariables.Has(var) && !c.T1.FreeVariables.Has(var)}};
+ Contract.Assert(Contract.ForAll(constraints, c =>
+ Contract.ForAll(subst.Keys, var =>
+ !c.T0.FreeVariables.Has(var) && !c.T1.FreeVariables.Has(var))));
}
return base.Substitute(subst);
}
-
+
//----------- Getters/Issers ----------------------------------
- public override bool IsBv { get {
- return true;
- } }
- public override int BvBits { get {
- // This method is supposed to return the number of bits supplied, but unless the proxy has been resolved,
- // we only have a lower bound on the number of bits supplied. But this method is not supposed to be
- // called until type checking has finished, at which time the minBits is stable.
- Type p = ProxyFor;
- if (p != null) {
- return p.BvBits;
- } else {
- return MinBits;
+ public override bool IsBv {
+ get {
+ return true;
+ }
+ }
+ public override int BvBits {
+ get {
+ // This method is supposed to return the number of bits supplied, but unless the proxy has been resolved,
+ // we only have a lower bound on the number of bits supplied. But this method is not supposed to be
+ // called until type checking has finished, at which time the minBits is stable.
+ Type p = ProxyFor;
+ if (p != null) {
+ return p.BvBits;
+ } else {
+ return MinBits;
+ }
}
- } }
+ }
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitBvTypeProxy(this);
}
}
@@ -1791,37 +2251,58 @@ namespace Microsoft.Boogie // constraints can be satisfied.
public class MapTypeProxy : ConstrainedProxy {
public readonly int Arity;
- private readonly List<Constraint>! constraints = new List<Constraint> ();
+ private readonly List<Constraint>/*!*/ constraints = new List<Constraint>();
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(constraints != null);
+ }
+
// each constraint specifies that the given combination of argument/result
// types must be a possible instance of the formal map argument/result types
private struct Constraint {
- public readonly TypeSeq! Arguments;
- public readonly Type! Result;
+ public readonly TypeSeq/*!*/ Arguments;
+ public readonly Type/*!*/ Result;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Arguments != null);
+ Contract.Invariant(Result != null);
+ }
+
- public Constraint(TypeSeq! arguments, Type! result) {
+ public Constraint(TypeSeq arguments, Type result) {
+ Contract.Requires(result != null);
+ Contract.Requires(arguments != null);
Arguments = arguments;
Result = result;
}
- public Constraint Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
- TypeSeq! args = new TypeSeq ();
- foreach (Type! t in Arguments)
+ public Constraint Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
+ Contract.Requires(cce.NonNullElements(varMap));
+ TypeSeq/*!*/ args = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
args.Add(t.Clone(varMap));
- Type! res = Result.Clone(varMap);
+ }
+ Type/*!*/ res = Result.Clone(varMap);
+ Contract.Assert(res != null);
return new Constraint(args, res);
}
- public bool Unify(MapType! that,
- TypeVariableSeq! unifiableVariables,
- IDictionary<TypeVariable!, Type!>! result)
- requires Arguments.Length == that.Arguments.Length; {
- Dictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!>();
- foreach (TypeVariable! tv in that.TypeParameters) {
+ public bool Unify(MapType that,
+ TypeVariableSeq/*!*/ unifiableVariables,
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {
+ Contract.Requires(unifiableVariables != null);
+ Contract.Requires(cce.NonNullElements(result));
+ Contract.Requires(that != null);
+ Contract.Requires(Arguments.Length == that.Arguments.Length);
+ Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
+ foreach (TypeVariable/*!*/ tv in that.TypeParameters) {
+ Contract.Assert(tv != null);
TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name);
subst.Add(tv, proxy);
}
-
+
bool good = true;
for (int i = 0; i < that.Arguments.Length; i++) {
Type t0 = that.Arguments[i].Substitute(subst);
@@ -1833,20 +2314,23 @@ namespace Microsoft.Boogie }
}
- public MapTypeProxy(IToken! token, string! name, int arity)
- requires 0 <= arity; {
- base(token, name, "mapproxy");
+ public MapTypeProxy(IToken token, string name, int arity)
+ : base(token, name, "mapproxy") {//BASEMOVEA
+ Contract.Requires(name != null);
+ Contract.Requires(token != null);
+ Contract.Requires(0 <= arity);
+ //:base(token, name, "mapproxy");
this.Arity = arity;
}
- private void AddConstraint(Constraint c)
- requires c.Arguments.Length == Arity; {
+ private void AddConstraint(Constraint c) {
+ Contract.Requires(c.Arguments.Length == Arity);
Type f = ProxyFor;
MapType mf = f as MapType;
if (mf != null) {
- bool success = c.Unify(mf, new TypeVariableSeq(), new Dictionary<TypeVariable!, Type!> ());
- assert success;
+ bool success = c.Unify(mf, new TypeVariableSeq(), new Dictionary<TypeVariable/*!*/, Type/*!*/>());
+ Contract.Assert(success);
return;
}
@@ -1855,18 +2339,25 @@ namespace Microsoft.Boogie mpf.AddConstraint(c);
return;
}
-
- assert f == null; // no other types should occur as specialisations of this proxy
+
+ Contract.Assert(f == null); // no other types should occur as specialisations of this proxy
constraints.Add(c);
}
- public Type CheckArgumentTypes(ExprSeq! actualArgs,
- out TypeParamInstantiation! tpInstantiation,
- IToken! typeCheckingSubject,
- string! opName,
- TypecheckingContext! tc)
- {
+ public Type CheckArgumentTypes(ExprSeq/*!*/ actualArgs,
+ out TypeParamInstantiation/*!*/ tpInstantiation,
+ IToken/*!*/ typeCheckingSubject,
+ string/*!*/ opName,
+ TypecheckingContext/*!*/ tc) {
+ Contract.Requires(actualArgs != null);
+ Contract.Requires(typeCheckingSubject != null);
+ Contract.Requires(opName != null);
+ Contract.Requires(tc != null);
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+
+
+
Type f = ProxyFor;
MapType mf = f as MapType;
if (mf != null)
@@ -1876,27 +2367,34 @@ namespace Microsoft.Boogie if (mpf != null)
return mpf.CheckArgumentTypes(actualArgs, out tpInstantiation, typeCheckingSubject, opName, tc);
- assert f == null; // no other types should occur as specialisations of this proxy
+ Contract.Assert(f == null); // no other types should occur as specialisations of this proxy
// otherwise, we just record the constraints given by this usage of the map type
- TypeSeq! arguments = new TypeSeq ();
- foreach (Expr! e in actualArgs)
+ TypeSeq/*!*/ arguments = new TypeSeq();
+ foreach (Expr/*!*/ e in actualArgs) {
+ Contract.Assert(e != null);
arguments.Add(e.Type);
- Type! result = new TypeProxy (tok, "result");
- AddConstraint(new Constraint (arguments, result));
+ }
+ Type/*!*/ result = new TypeProxy(tok, "result");
+ Contract.Assert(result != null);
+ AddConstraint(new Constraint(arguments, result));
- TypeSeq! argumentsResult = new TypeSeq ();
- foreach (Expr! e in actualArgs)
+ TypeSeq/*!*/ argumentsResult = new TypeSeq();
+ foreach (Expr/*!*/ e in actualArgs) {
+ Contract.Assert(e != null);
argumentsResult.Add(e.Type);
+ }
argumentsResult.Add(result);
-
+
tpInstantiation = new MapTypeProxyParamInstantiation(this, argumentsResult);
return result;
}
//----------- Cloning ----------------------------------
- public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
Type p = ProxyFor;
if (p != null) {
return p.Clone(varMap);
@@ -1910,14 +2408,14 @@ namespace Microsoft.Boogie //----------- Linearisation ----------------------------------
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
+ //Contract.Requires(stream != null);
Type p = ProxyFor;
if (p != null) {
p.Emit(stream, contextBindingStrength);
} else {
stream.Write("[");
- string! sep = "";
+ string/*!*/ sep = "";
for (int i = 0; i < Arity; ++i) {
stream.Write(sep);
sep = ", ";
@@ -1929,9 +2427,12 @@ namespace Microsoft.Boogie //----------- Unification of types -----------
- public override bool Unify(Type! that,
- TypeVariableSeq! unifiableVariables,
- IDictionary<TypeVariable!, Type!>! result) {
+ public override bool Unify(Type/*!*/ that,
+ TypeVariableSeq/*!*/ unifiableVariables,
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {
+ //Contract.Requires(that != null);
+ //Contract.Requires(unifiableVariables != null);
+ //Contract.Requires(cce.NonNullElements(result));
Type p = ProxyFor;
if (p != null) {
return p.Unify(that, unifiableVariables, result);
@@ -1946,7 +2447,7 @@ namespace Microsoft.Boogie TypeVariable tv = that as TypeVariable;
- if (tv != null && unifiableVariables.Has(tv))
+ if (tv != null && unifiableVariables.Has(tv))
return that.Unify(this, unifiableVariables, result);
if (object.ReferenceEquals(this, that)) {
@@ -1983,35 +2484,51 @@ namespace Microsoft.Boogie //----------- Substitution of free variables with types not containing bound variables -----------------
- public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
+ //Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
if (this.ProxyFor == null) {
// check that the constraints are clean and do not contain any
// of the substituted variables (otherwise, we are in big trouble)
- assert forall{Constraint c in constraints;
- forall{TypeVariable! var in subst.Keys;
- forall{Type! t in c.Arguments; !t.FreeVariables.Has(var)} &&
- !c.Result.FreeVariables.Has(var)}};
+ Contract.Assert(Contract.ForAll(constraints, c =>
+ Contract.ForAll(subst.Keys, var =>
+ Contract.ForAll(0, c.Arguments.Length, t => !c.Arguments[t].FreeVariables.Has(var)) &&
+ !c.Result.FreeVariables.Has(var))));
}
return base.Substitute(subst);
}
//----------- Getters/Issers ----------------------------------
- public override bool IsMap { get { return true; } }
- public override MapType! AsMap { get {
- Type p = ProxyFor;
- if (p != null) {
- return p.AsMap;
- } else {
- assert false; // what to do now?
+ public override bool IsMap {
+ get {
+ return true;
}
- } }
- public override int MapArity { get {
- return Arity;
- } }
+ }
+ public override MapType/*!*/ AsMap {
+ get {
+ Contract.Ensures(Contract.Result<MapType>() != null);
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ Type p = ProxyFor;
+ if (p != null) {
+ return p.AsMap;
+ } else {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // what to do now?
+ }
+ }
+ }
+ public override int MapArity {
+ get {
+ return Arity;
+ }
+ }
+
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitMapTypeProxy(this);
}
}
@@ -2023,35 +2540,49 @@ namespace Microsoft.Boogie // equivalent to ExpandedType, the annotations are only used to enable
// better pretty-printing
public class TypeSynonymAnnotation : Type {
- public Type! ExpandedType;
+ public Type/*!*/ ExpandedType;
- public readonly TypeSeq! Arguments;
+ public readonly TypeSeq/*!*/ Arguments;
// is set during resolution and determines whether the right number of arguments is given
- public readonly TypeSynonymDecl! Decl;
+ public readonly TypeSynonymDecl/*!*/ Decl;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(ExpandedType != null);
+ Contract.Invariant(Arguments != null);
+ Contract.Invariant(Decl != null);
+ }
- public TypeSynonymAnnotation(IToken! token, TypeSynonymDecl! decl, TypeSeq! arguments)
- : base(token)
- requires arguments.Length == decl.TypeParameters.Length;
- {
+
+ public TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, TypeSeq/*!*/ arguments)
+ : base(token) {
+ Contract.Requires(token != null);
+ Contract.Requires(decl != null);
+ Contract.Requires(arguments != null);
+ Contract.Requires(arguments.Length == decl.TypeParameters.Length);
this.Decl = decl;
this.Arguments = arguments;
// build a substitution that can be applied to the definition of
// the type synonym
- IDictionary<TypeVariable!, Type!>! subst =
- new Dictionary<TypeVariable!, Type!> ();
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst =
+ new Dictionary<TypeVariable/*!*/, Type/*!*/>();
for (int i = 0; i < arguments.Length; ++i)
subst.Add(decl.TypeParameters[i], arguments[i]);
ExpandedType = decl.Body.Substitute(subst);
}
- private TypeSynonymAnnotation(IToken! token, TypeSynonymDecl! decl, TypeSeq! arguments,
- Type! expandedType)
+ private TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, TypeSeq/*!*/ arguments,
+ Type/*!*/ expandedType)
: base(token) {
+ Contract.Requires(token != null);
+ Contract.Requires(decl != null);
+ Contract.Requires(arguments != null);
+ Contract.Requires(expandedType != null);
+
this.Decl = decl;
this.Arguments = arguments;
- this.ExpandedType = expandedType; + this.ExpandedType = expandedType;
}
//----------- Cloning ----------------------------------
@@ -2059,40 +2590,58 @@ namespace Microsoft.Boogie // have to be created in the right way. It is /not/ ok to just clone
// everything recursively
- public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
- TypeSeq! newArgs = new TypeSeq ();
- foreach(Type! t in Arguments)
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
+ TypeSeq/*!*/ newArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
newArgs.Add(t.Clone(varMap));
- Type! newExpandedType = ExpandedType.Clone(varMap);
+ }
+ Type/*!*/ newExpandedType = ExpandedType.Clone(varMap);
+ Contract.Assert(newExpandedType != null);
return new TypeSynonymAnnotation(tok, Decl, newArgs, newExpandedType);
}
- public override Type! CloneUnresolved() {
- TypeSeq! newArgs = new TypeSeq ();
- foreach(Type! t in Arguments)
+ public override Type CloneUnresolved() {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ TypeSeq/*!*/ newArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
newArgs.Add(t.CloneUnresolved());
+ }
return new TypeSynonymAnnotation(tok, Decl, newArgs);
}
//----------- Equality ----------------------------------
[Pure]
- public override bool Equals(Type! that,
- TypeVariableSeq! thisBoundVariables,
- TypeVariableSeq! thatBoundVariables) {
+ public override bool Equals(Type/*!*/ that,
+ TypeVariableSeq/*!*/ thisBoundVariables,
+ TypeVariableSeq/*!*/ thatBoundVariables) {
+ //Contract.Requires(that != null);
+ //Contract.Requires(thisBoundVariables != null);
+ //Contract.Requires(thatBoundVariables != null);
return ExpandedType.Equals(that, thisBoundVariables, thatBoundVariables);
}
// used to skip leading type annotations
- internal override Type! Expanded { get {
- return ExpandedType.Expanded;
- } }
+ internal override Type/*!*/ Expanded {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ return ExpandedType.Expanded;
+ }
+ }
//----------- Unification of types -----------
- public override bool Unify(Type! that,
- TypeVariableSeq! unifiableVariables,
- IDictionary<TypeVariable!, Type!>! result) {
+ public override bool Unify(Type/*!*/ that,
+ TypeVariableSeq/*!*/ unifiableVariables,
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {
+ //Contract.Requires(that != null);
+ //Contract.Requires(unifiableVariables != null);
+ //Contract.Requires(cce.NonNullElements(result));
return ExpandedType.Unify(that, unifiableVariables, result);
}
@@ -2109,69 +2658,143 @@ namespace Microsoft.Boogie //----------- Substitution of free variables with types not containing bound variables -----------------
- public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
+ //Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
if (subst.Count == 0)
return this;
- TypeSeq newArgs = new TypeSeq ();
- foreach (Type! t in Arguments)
+ TypeSeq newArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
newArgs.Add(t.Substitute(subst));
- Type! newExpandedType = ExpandedType.Substitute(subst);
+ }
+ Type/*!*/ newExpandedType = ExpandedType.Substitute(subst);
+ Contract.Assert(newExpandedType != null);
return new TypeSynonymAnnotation(tok, Decl, newArgs, newExpandedType);
}
//----------- Hashcodes ----------------------------------
[Pure]
- public override int GetHashCode(TypeVariableSeq! boundVariables) {
+ public override int GetHashCode(TypeVariableSeq boundVariables) {
+ //Contract.Requires(boundVariables != null);
return ExpandedType.GetHashCode(boundVariables);
}
//----------- Linearisation ----------------------------------
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
+ //Contract.Requires(stream != null);
stream.SetToken(this);
CtorType.EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength);
}
//----------- Resolution ----------------------------------
- public override Type! ResolveType(ResolutionContext! rc) {
- TypeSeq resolvedArgs = new TypeSeq ();
- foreach (Type! t in Arguments)
+ public override Type ResolveType(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ TypeSeq resolvedArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
resolvedArgs.Add(t.ResolveType(rc));
+ }
return new TypeSynonymAnnotation(tok, Decl, resolvedArgs);
}
- public override TypeVariableSeq! FreeVariables { get {
- return ExpandedType.FreeVariables;
- } }
+ public override TypeVariableSeq/*!*/ FreeVariables {
+ get {
+ Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
- public override List<TypeProxy!>! FreeProxies { get {
- return ExpandedType.FreeProxies;
- } }
+ return ExpandedType.FreeVariables;
+ }
+ }
+
+ public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
+ return ExpandedType.FreeProxies;
+ }
+ }
//----------- Getters/Issers ----------------------------------
- public override bool IsBasic { get { return ExpandedType.IsBasic; } }
- public override bool IsInt { get { return ExpandedType.IsInt; } }
- public override bool IsBool { get { return ExpandedType.IsBool; } }
+ public override bool IsBasic {
+ get {
+ return ExpandedType.IsBasic;
+ }
+ }
+ public override bool IsInt {
+ get {
+ return ExpandedType.IsInt;
+ }
+ }
+ public override bool IsBool {
+ get {
+ return ExpandedType.IsBool;
+ }
+ }
- public override bool IsVariable { get { return ExpandedType.IsVariable; } }
- public override TypeVariable! AsVariable { get { return ExpandedType.AsVariable; } }
- public override bool IsCtor { get { return ExpandedType.IsCtor; } }
- public override CtorType! AsCtor { get { return ExpandedType.AsCtor; } }
- public override bool IsMap { get { return ExpandedType.IsMap; } }
- public override MapType! AsMap { get { return ExpandedType.AsMap; } }
- public override bool IsUnresolved { get { return ExpandedType.IsUnresolved; } }
- public override UnresolvedTypeIdentifier! AsUnresolved { get {
- return ExpandedType.AsUnresolved; } }
+ public override bool IsVariable {
+ get {
+ return ExpandedType.IsVariable;
+ }
+ }
+ public override TypeVariable/*!*/ AsVariable {
+ get {
+ Contract.Ensures(Contract.Result<TypeVariable>() != null);
+ return ExpandedType.AsVariable;
+ }
+ }
+ public override bool IsCtor {
+ get {
+ return ExpandedType.IsCtor;
+ }
+ }
+ public override CtorType/*!*/ AsCtor {
+ get {
+ Contract.Ensures(Contract.Result<CtorType>() != null);
+ return ExpandedType.AsCtor;
+ }
+ }
+ public override bool IsMap {
+ get {
+ return ExpandedType.IsMap;
+ }
+ }
+ public override MapType/*!*/ AsMap {
+ get {
+ Contract.Ensures(Contract.Result<MapType>() != null);
+ return ExpandedType.AsMap;
+ }
+ }
+ public override bool IsUnresolved {
+ get {
+ return ExpandedType.IsUnresolved;
+ }
+ }
+ public override UnresolvedTypeIdentifier/*!*/ AsUnresolved {
+ get {
+ Contract.Ensures(Contract.Result<UnresolvedTypeIdentifier>() != null);
- public override bool IsBv { get { return ExpandedType.IsBv; } }
- public override int BvBits { get { return ExpandedType.BvBits; } }
+ return ExpandedType.AsUnresolved;
+ }
+ }
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override bool IsBv {
+ get {
+ return ExpandedType.IsBv;
+ }
+ }
+ public override int BvBits {
+ get {
+ return ExpandedType.BvBits;
+ }
+ }
+
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitTypeSynonymAnnotation(this);
}
}
@@ -2179,14 +2802,22 @@ namespace Microsoft.Boogie //=====================================================================
public class CtorType : Type {
- public readonly TypeSeq! Arguments;
+ public readonly TypeSeq/*!*/ Arguments;
// is set during resolution and determines whether the right number of arguments is given
- public readonly TypeCtorDecl! Decl;
+ public readonly TypeCtorDecl/*!*/ Decl;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Arguments != null);
+ Contract.Invariant(Decl != null);
+ }
- public CtorType(IToken! token, TypeCtorDecl! decl, TypeSeq! arguments)
- : base(token)
- requires arguments.Length == decl.Arity;
- {
+
+ public CtorType(IToken/*!*/ token, TypeCtorDecl/*!*/ decl, TypeSeq/*!*/ arguments)
+ : base(token) {
+ Contract.Requires(token != null);
+ Contract.Requires(decl != null);
+ Contract.Requires(arguments != null);
+ Contract.Requires(arguments.Length == decl.Arity);
this.Decl = decl;
this.Arguments = arguments;
}
@@ -2196,23 +2827,31 @@ namespace Microsoft.Boogie // have to be created in the right way. It is /not/ ok to just clone
// everything recursively
- public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
- TypeSeq! newArgs = new TypeSeq ();
- foreach(Type! t in Arguments)
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
+ TypeSeq/*!*/ newArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
newArgs.Add(t.Clone(varMap));
+ }
return new CtorType(tok, Decl, newArgs);
}
- public override Type! CloneUnresolved() {
- TypeSeq! newArgs = new TypeSeq ();
- foreach(Type! t in Arguments)
+ public override Type CloneUnresolved() {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ TypeSeq/*!*/ newArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
newArgs.Add(t.CloneUnresolved());
+ }
return new CtorType(tok, Decl, newArgs);
}
//----------- Equality ----------------------------------
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
Type thatType = that as Type;
if (thatType == null)
@@ -2228,9 +2867,9 @@ namespace Microsoft.Boogie }
[Pure]
- public override bool Equals(Type! that,
- TypeVariableSeq! thisBoundVariables,
- TypeVariableSeq! thatBoundVariables) {
+ public override bool Equals(Type/*!*/ that,
+ TypeVariableSeq/*!*/ thisBoundVariables,
+ TypeVariableSeq/*!*/ thatBoundVariables) {
that = TypeProxy.FollowProxy(that.Expanded);
CtorType thatCtorType = that as CtorType;
if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl))
@@ -2245,9 +2884,9 @@ namespace Microsoft.Boogie //----------- Unification of types -----------
- public override bool Unify(Type! that,
- TypeVariableSeq! unifiableVariables,
- IDictionary<TypeVariable!, Type!>! result) {
+ public override bool Unify(Type/*!*/ that,
+ TypeVariableSeq/*!*/ unifiableVariables,
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {
that = that.Expanded;
if (that is TypeProxy || that is TypeVariable)
return that.Unify(this, unifiableVariables, result);
@@ -2288,41 +2927,52 @@ namespace Microsoft.Boogie //----------- Substitution of free variables with types not containing bound variables -----------------
- public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
+ //Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
if (subst.Count == 0)
return this;
- TypeSeq newArgs = new TypeSeq ();
- foreach (Type! t in Arguments)
+ TypeSeq newArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
newArgs.Add(t.Substitute(subst));
+ }
return new CtorType(tok, Decl, newArgs);
}
//----------- Hashcodes ----------------------------------
[Pure]
- public override int GetHashCode(TypeVariableSeq! boundVariables) {
+ public override int GetHashCode(TypeVariableSeq boundVariables) {
+ //Contract.Requires(boundVariables != null);
int res = 1637643879 * Decl.GetHashCode();
- foreach (Type! t in Arguments)
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
res = res * 3 + t.GetHashCode(boundVariables);
+ }
return res;
}
//----------- Linearisation ----------------------------------
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
+ //Contract.Requires(stream != null);
stream.SetToken(this);
EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength);
}
-
- internal static void EmitCtorType(string! name, TypeSeq! args, TokenTextWriter! stream, int contextBindingStrength) {
+
+ internal static void EmitCtorType(string name, TypeSeq args, TokenTextWriter stream, int contextBindingStrength) {
+ Contract.Requires(stream != null);
+ Contract.Requires(args != null);
+ Contract.Requires(name != null);
int opBindingStrength = args.Length > 0 ? 0 : 2;
if (opBindingStrength < contextBindingStrength)
stream.Write("(");
stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(name));
int i = args.Length;
- foreach (Type! t in args) {
+ foreach (Type/*!*/ t in args) {
+ Contract.Assert(t != null);
stream.Write(" ");
// use a lower binding strength for the last argument
// to allow map-types without parentheses
@@ -2336,36 +2986,55 @@ namespace Microsoft.Boogie //----------- Resolution ----------------------------------
- public override Type! ResolveType(ResolutionContext! rc) {
- TypeSeq resolvedArgs = new TypeSeq ();
- foreach (Type! t in Arguments)
+ public override Type ResolveType(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ TypeSeq resolvedArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
resolvedArgs.Add(t.ResolveType(rc));
+ }
return new CtorType(tok, Decl, resolvedArgs);
}
- public override TypeVariableSeq! FreeVariables {
- get {
- TypeVariableSeq! res = new TypeVariableSeq ();
- foreach (Type! t in Arguments)
- res.AppendWithoutDups(t.FreeVariables);
- return res;
- }
+ public override TypeVariableSeq/*!*/ FreeVariables {
+ get {
+ TypeVariableSeq/*!*/ res = new TypeVariableSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
+ res.AppendWithoutDups(t.FreeVariables);
+ }
+ return res;
+ }
}
- public override List<TypeProxy!>! FreeProxies { get {
- List<TypeProxy!>! res = new List<TypeProxy!> ();
- foreach (Type! t in Arguments)
- AppendWithoutDups(res, t.FreeProxies);
- return res;
- } }
+ public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
+ get {
+ List<TypeProxy/*!*/>/*!*/ res = new List<TypeProxy/*!*/>();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
+ AppendWithoutDups(res, t.FreeProxies);
+ }
+ return res;
+ }
+ }
//----------- Getters/Issers ----------------------------------
- public override bool IsCtor { get { return true; } }
- public override CtorType! AsCtor { get { return this; } }
+ public override bool IsCtor {
+ get {
+ return true;
+ }
+ }
+ public override CtorType/*!*/ AsCtor {
+ get {
+ return this;
+ }
+ }
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitCtorType(this);
}
}
@@ -2375,13 +3044,24 @@ namespace Microsoft.Boogie public class MapType : Type {
// an invariant is that each of the type parameters has to occur as
// free variable in at least one of the arguments
- public readonly TypeVariableSeq! TypeParameters;
- public readonly TypeSeq! Arguments;
- public Type! Result;
+ public readonly TypeVariableSeq/*!*/ TypeParameters;
+ public readonly TypeSeq/*!*/ Arguments;
+ public Type/*!*/ Result;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(TypeParameters != null);
+ Contract.Invariant(Arguments != null);
+ Contract.Invariant(Result != null);
+ }
+
+
+ public MapType(IToken/*!*/ token, TypeVariableSeq/*!*/ typeParameters, TypeSeq/*!*/ arguments, Type/*!*/ result)
+ : base(token) {
+ Contract.Requires(token != null);
+ Contract.Requires(typeParameters != null);
+ Contract.Requires(arguments != null);
+ Contract.Requires(result != null);
- public MapType(IToken! token, TypeVariableSeq! typeParameters, TypeSeq! arguments, Type! result)
- : base(token)
- {
this.TypeParameters = typeParameters;
this.Result = result;
this.Arguments = arguments;
@@ -2392,50 +3072,64 @@ namespace Microsoft.Boogie // have to be created in the right way. It is /not/ ok to just clone
// everything recursively
- public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
- IDictionary<TypeVariable!, TypeVariable!>! newVarMap =
- new Dictionary<TypeVariable!, TypeVariable!>();
- foreach (KeyValuePair<TypeVariable!, TypeVariable!> p in varMap) {
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
+ IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ newVarMap =
+ new Dictionary<TypeVariable/*!*/, TypeVariable/*!*/>();
+ foreach (KeyValuePair<TypeVariable/*!*/, TypeVariable/*!*/> p in varMap) {
+ Contract.Assert(cce.NonNullElements(p));
if (!TypeParameters.Has(p.Key))
newVarMap.Add(p);
}
- TypeVariableSeq! newTypeParams = new TypeVariableSeq ();
- foreach (TypeVariable! var in TypeParameters) {
- TypeVariable! newVar = new TypeVariable (var.tok, var.Name);
+ TypeVariableSeq/*!*/ newTypeParams = new TypeVariableSeq();
+ foreach (TypeVariable/*!*/ var in TypeParameters) {
+ Contract.Assert(var != null);
+ TypeVariable/*!*/ newVar = new TypeVariable(var.tok, var.Name);
+ Contract.Assert(newVar != null);
newVarMap.Add(var, newVar);
newTypeParams.Add(newVar);
}
- TypeSeq! newArgs = new TypeSeq ();
- foreach(Type! t in Arguments)
+ TypeSeq/*!*/ newArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
newArgs.Add(t.Clone(newVarMap));
- Type! newResult = Result.Clone(newVarMap);
+ }
+ Type/*!*/ newResult = Result.Clone(newVarMap);
+ Contract.Assert(newResult != null);
- return new MapType (this.tok, newTypeParams, newArgs, newResult);
+ return new MapType(this.tok, newTypeParams, newArgs, newResult);
}
- public override Type! CloneUnresolved() {
- TypeVariableSeq! newTypeParams = new TypeVariableSeq ();
- foreach (TypeVariable! var in TypeParameters) {
- TypeVariable! newVar = new TypeVariable (var.tok, var.Name);
+ public override Type CloneUnresolved() {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ TypeVariableSeq/*!*/ newTypeParams = new TypeVariableSeq();
+ foreach (TypeVariable/*!*/ var in TypeParameters) {
+ Contract.Assert(var != null);
+ TypeVariable/*!*/ newVar = new TypeVariable(var.tok, var.Name);
+ Contract.Assert(newVar != null);
newTypeParams.Add(newVar);
}
- TypeSeq! newArgs = new TypeSeq ();
- foreach(Type! t in Arguments)
+ TypeSeq/*!*/ newArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
newArgs.Add(t.CloneUnresolved());
- Type! newResult = Result.CloneUnresolved();
+ }
+ Type/*!*/ newResult = Result.CloneUnresolved();
+ Contract.Assert(newResult != null);
- return new MapType (this.tok, newTypeParams, newArgs, newResult);
+ return new MapType(this.tok, newTypeParams, newArgs, newResult);
}
//----------- Equality ----------------------------------
[Pure]
- public override bool Equals(Type! that,
- TypeVariableSeq! thisBoundVariables,
- TypeVariableSeq! thatBoundVariables) {
+ public override bool Equals(Type/*!*/ that,
+ TypeVariableSeq/*!*/ thisBoundVariables,
+ TypeVariableSeq/*!*/ thatBoundVariables) {
that = TypeProxy.FollowProxy(that.Expanded);
MapType thatMapType = that as MapType;
if (thatMapType == null ||
@@ -2443,10 +3137,14 @@ namespace Microsoft.Boogie this.Arguments.Length != thatMapType.Arguments.Length)
return false;
- foreach (TypeVariable! var in this.TypeParameters)
+ foreach (TypeVariable/*!*/ var in this.TypeParameters) {
+ Contract.Assert(var != null);
thisBoundVariables.Add(var);
- foreach (TypeVariable! var in thatMapType.TypeParameters)
+ }
+ foreach (TypeVariable/*!*/ var in thatMapType.TypeParameters) {
+ Contract.Assert(var != null);
thatBoundVariables.Add(var);
+ }
try {
@@ -2466,15 +3164,15 @@ namespace Microsoft.Boogie thatBoundVariables.Remove();
}
}
-
+
return true;
}
//----------- Unification of types -----------
- public override bool Unify(Type! that,
- TypeVariableSeq! unifiableVariables,
- IDictionary<TypeVariable!, Type!>! result) {
+ public override bool Unify(Type/*!*/ that,
+ TypeVariableSeq/*!*/ unifiableVariables,
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {
that = that.Expanded;
if (that is TypeProxy || that is TypeVariable)
return that.Unify(this, unifiableVariables, result);
@@ -2486,8 +3184,10 @@ namespace Microsoft.Boogie return false;
// treat the bound variables of the two map types as equal...
- Dictionary<TypeVariable!, Type!>! subst0 = new Dictionary<TypeVariable!, Type!>();
- Dictionary<TypeVariable!, Type!>! subst1 = new Dictionary<TypeVariable!, Type!>();
+ Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst0 =
+ new Dictionary<TypeVariable/*!*/, Type/*!*/>();
+ Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst1 =
+ new Dictionary<TypeVariable/*!*/, Type/*!*/>();
TypeVariableSeq freshies = new TypeVariableSeq();
for (int i = 0; i < this.TypeParameters.Length; i++) {
TypeVariable tp0 = this.TypeParameters[i];
@@ -2514,16 +3214,23 @@ namespace Microsoft.Boogie // non-substituted types ...
TypeVariableSeq freeVars = this.FreeVariables;
foreach (TypeVariable fr in freshies)
- if (freeVars.Has(fr)) { return false; } // fresh variable escaped
+ if (freeVars.Has(fr)) {
+ return false;
+ } // fresh variable escaped
freeVars = thatMapType.FreeVariables;
foreach (TypeVariable fr in freshies)
- if (freeVars.Has(fr)) { return false; } // fresh variable escaped
+ if (freeVars.Has(fr)) {
+ return false;
+ } // fresh variable escaped
// ... and in the resulting unifier of type variables
- foreach (KeyValuePair<TypeVariable!, Type!> pair in result) {
+ foreach (KeyValuePair<TypeVariable/*!*/, Type/*!*/> pair in result) {
+ Contract.Assert(cce.NonNullElements(pair));
freeVars = pair.Value.FreeVariables;
foreach (TypeVariable fr in freshies)
- if (freeVars.Has(fr)) { return false; } // fresh variable escaped
+ if (freeVars.Has(fr)) {
+ return false;
+ } // fresh variable escaped
}
}
@@ -2558,10 +3265,12 @@ namespace Microsoft.Boogie if (thatMapType.collisionsPossible(result))
thatMapType = (MapType)that.Clone();
- foreach (TypeVariable! var in this.TypeParameters)
- thisBoundVariables.Add(var);
- foreach (TypeVariable! var in thatMapType.TypeParameters)
- thatBoundVariables.Add(var);
+ foreach(TypeVariable/*!*/ var in this.TypeParameters){
+Contract.Assert(var != null);
+ thisBoundVariables.Add(var);}
+ foreach(TypeVariable/*!*/ var in thatMapType.TypeParameters){
+Contract.Assert(var != null);
+ thatBoundVariables.Add(var);}
try {
@@ -2588,14 +3297,15 @@ namespace Microsoft.Boogie //----------- Substitution of free variables with types not containing bound variables -----------------
[Pure]
- private bool collisionsPossible(IDictionary<TypeVariable!, Type!>! subst) {
+ private bool collisionsPossible(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
+ Contract.Requires(cce.NonNullElements(subst));
// PR: could be written more efficiently
- return exists{TypeVariable! var in TypeParameters;
- subst.ContainsKey(var) ||
- exists{Type! t in subst.Values; t.FreeVariables.Has(var)}};
+ return Contract.Exists(0, TypeParameters.Length, i => subst.ContainsKey(TypeParameters[i]) || Contract.Exists(subst.Values, t => t.FreeVariables.Has(TypeParameters[i])));
}
- public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
+ //Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
if (subst.Count == 0)
return this;
@@ -2608,15 +3318,19 @@ namespace Microsoft.Boogie // variables are fresh
if (collisionsPossible(subst)) {
- MapType! newType = (MapType)this.Clone();
- assert newType.Equals(this) && !newType.collisionsPossible(subst);
+ MapType/*!*/ newType = (MapType)this.Clone();
+ Contract.Assert(newType != null);
+ Contract.Assert(newType.Equals(this) && !newType.collisionsPossible(subst));
return newType.Substitute(subst);
}
- TypeSeq newArgs = new TypeSeq ();
- foreach (Type! t in Arguments)
+ TypeSeq newArgs = new TypeSeq();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
newArgs.Add(t.Substitute(subst));
- Type! newResult = Result.Substitute(subst);
+ }
+ Type/*!*/ newResult = Result.Substitute(subst);
+ Contract.Assert(newResult != null);
return new MapType(tok, TypeParameters, newArgs, newResult);
}
@@ -2624,14 +3338,19 @@ namespace Microsoft.Boogie //----------- Hashcodes ----------------------------------
[Pure]
- public override int GetHashCode(TypeVariableSeq! boundVariables) {
+ public override int GetHashCode(TypeVariableSeq boundVariables) {
+ //Contract.Requires(boundVariables != null);
int res = 7643761 * TypeParameters.Length + 65121 * Arguments.Length;
- foreach (TypeVariable! var in this.TypeParameters)
+ foreach (TypeVariable/*!*/ var in this.TypeParameters) {
+ Contract.Assert(var != null);
boundVariables.Add(var);
+ }
- foreach (Type! t in Arguments)
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
res = res * 5 + t.GetHashCode(boundVariables);
+ }
res = res * 7 + Result.GetHashCode(boundVariables);
for (int i = 0; i < this.TypeParameters.Length; ++i)
@@ -2642,8 +3361,8 @@ namespace Microsoft.Boogie //----------- Linearisation ----------------------------------
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
+ //Contract.Requires(stream != null);
stream.SetToken(this);
const int opBindingStrength = 1;
@@ -2663,15 +3382,19 @@ namespace Microsoft.Boogie //----------- Resolution ----------------------------------
- public override Type! ResolveType(ResolutionContext! rc) {
+ public override Type ResolveType(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
int previousState = rc.TypeBinderState;
try {
- foreach (TypeVariable! v in TypeParameters) {
+ foreach (TypeVariable/*!*/ v in TypeParameters) {
+ Contract.Assert(v != null);
rc.AddTypeBinder(v);
}
- TypeSeq resolvedArgs = new TypeSeq ();
- foreach (Type! ty in Arguments) {
+ TypeSeq resolvedArgs = new TypeSeq();
+ foreach (Type/*!*/ ty in Arguments) {
+ Contract.Assert(ty != null);
resolvedArgs.Add(ty.ResolveType(rc));
}
@@ -2683,72 +3406,100 @@ namespace Microsoft.Boogie rc);
// sort the type parameters so that they are bound in the order of occurrence
- TypeVariableSeq! sortedTypeParams = SortTypeParams(TypeParameters, resolvedArgs, resolvedResult);
+ TypeVariableSeq/*!*/ sortedTypeParams = SortTypeParams(TypeParameters, resolvedArgs, resolvedResult);
+ Contract.Assert(sortedTypeParams != null);
return new MapType(tok, sortedTypeParams, resolvedArgs, resolvedResult);
} finally {
rc.TypeBinderState = previousState;
}
}
- public override TypeVariableSeq! FreeVariables {
+ public override TypeVariableSeq/*!*/ FreeVariables {
get {
- TypeVariableSeq! res = FreeVariablesIn(Arguments);
+ TypeVariableSeq/*!*/ res = FreeVariablesIn(Arguments);
+ Contract.Assert(res != null);
res.AppendWithoutDups(Result.FreeVariables);
- foreach (TypeVariable! v in TypeParameters)
+ foreach (TypeVariable/*!*/ v in TypeParameters) {
+ Contract.Assert(v != null);
res.Remove(v);
+ }
return res;
}
}
- public override List<TypeProxy!>! FreeProxies { get {
- List<TypeProxy!>! res = new List<TypeProxy!> ();
- foreach (Type! t in Arguments)
- AppendWithoutDups(res, t.FreeProxies);
- AppendWithoutDups(res, Result.FreeProxies);
- return res;
- } }
+ public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
+ get {
+ List<TypeProxy/*!*/>/*!*/ res = new List<TypeProxy/*!*//*!*/>();
+ foreach (Type/*!*/ t in Arguments) {
+ Contract.Assert(t != null);
+ AppendWithoutDups(res, t.FreeProxies);
+ }
+ AppendWithoutDups(res, Result.FreeProxies);
+ return res;
+ }
+ }
//----------- Getters/Issers ----------------------------------
- public override bool IsMap { get { return true; } }
- public override MapType! AsMap { get { return this; } }
- public override int MapArity { get {
- return Arguments.Length;
- } }
+ public override bool IsMap {
+ get {
+ return true;
+ }
+ }
+ public override MapType/*!*/ AsMap {
+ get {
+ return this;
+ }
+ }
+ public override int MapArity {
+ get {
+ return Arguments.Length;
+ }
+ }
//------------ Match formal argument types of the map
//------------ on concrete types, substitute the result into the
//------------ result type. Null is returned if so many type checking
//------------ errors occur that the situation is hopeless
- public Type CheckArgumentTypes(ExprSeq! actualArgs,
- out TypeParamInstantiation! tpInstantiation,
- IToken! typeCheckingSubject,
- string! opName,
- TypecheckingContext! tc) {
- List<Type!>! actualTypeParams;
+ public Type CheckArgumentTypes(ExprSeq/*!*/ actualArgs,
+ out TypeParamInstantiation/*!*/ tpInstantiation,
+ IToken/*!*/ typeCheckingSubject,
+ string/*!*/ opName,
+ TypecheckingContext/*!*/ tc) {
+ Contract.Requires(actualArgs != null);
+ Contract.Requires(typeCheckingSubject != null);
+
+ Contract.Requires(opName != null);
+ Contract.Requires(tc != null);
+Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+ List<Type/*!*/>/*!*/ actualTypeParams;
TypeSeq actualResult =
Type.CheckArgumentTypes(TypeParameters, out actualTypeParams, Arguments, actualArgs,
- new TypeSeq (Result), null, typeCheckingSubject, opName, tc);
+ new TypeSeq(Result), null, typeCheckingSubject, opName, tc);
if (actualResult == null) {
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
return null;
} else {
- assert actualResult.Length == 1;
+ Contract.Assert(actualResult.Length == 1);
tpInstantiation = SimpleTypeParamInstantiation.From(TypeParameters, actualTypeParams);
return actualResult[0];
}
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitMapType(this);
}
}
//---------------------------------------------------------------------
- public enum SimpleType { Int, Bool };
+ public enum SimpleType {
+ Int,
+ Bool
+ };
//=====================================================================
@@ -2758,31 +3509,73 @@ namespace Microsoft.Boogie // instead of using a simple list or dictionary, because in some cases
// (due to the type proxies for map types) the actual number and instantiation
// of type parameters can only be determined very late.
+ [ContractClass(typeof(TypeParamInstantiationContracts))]
public interface TypeParamInstantiation {
// return what formal type parameters there are
- List<TypeVariable!>! FormalTypeParams { get; }
+ List<TypeVariable/*!*/>/*!*/ FormalTypeParams {
+ get;
+ }
// given a formal type parameter, return the actual instantiation
- Type! this[TypeVariable! var] { get; }
+ Type/*!*/ this[TypeVariable/*!*/ var] {
+ get;
+ }
+ }
+ [ContractClassFor(typeof(TypeParamInstantiation))]
+ public abstract class TypeParamInstantiationContracts : TypeParamInstantiation {
+ #region TypeParamInstantiation Members
+
+ public List<TypeVariable> FormalTypeParams {
+
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
+ throw new NotImplementedException();
+ }
+ }
+
+ public Type this[TypeVariable var] {
+ get {
+ Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ throw new NotImplementedException();
+ }
+ }
+
+ #endregion
}
+
public class SimpleTypeParamInstantiation : TypeParamInstantiation {
- private readonly List<TypeVariable!>! TypeParams;
- private readonly IDictionary<TypeVariable!, Type!>! Instantiations;
+ private readonly List<TypeVariable/*!*/>/*!*/ TypeParams;
+ [ContractInvariantMethod]
+ void TypeParamsInvariantMethod() {
+ Contract.Invariant(cce.NonNullElements(TypeParams));
+ }
+ private readonly IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ Instantiations;
+ [ContractInvariantMethod]
+ void InstantiationsInvariantMethod() {
+ Contract.Invariant(cce.NonNullElements(Instantiations));
+ }
- public SimpleTypeParamInstantiation(List<TypeVariable!>! typeParams,
- IDictionary<TypeVariable!, Type!>! instantiations) {
+ public SimpleTypeParamInstantiation(List<TypeVariable/*!*/>/*!*/ typeParams,
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ instantiations) {
+ Contract.Requires(cce.NonNullElements(typeParams));
+ Contract.Requires(cce.NonNullElements(instantiations));
this.TypeParams = typeParams;
this.Instantiations = instantiations;
}
- public static TypeParamInstantiation!
- From(TypeVariableSeq! typeParams, List<Type!>! actualTypeParams)
- requires typeParams.Length == actualTypeParams.Count; {
+ public static TypeParamInstantiation/*!*/ From(TypeVariableSeq typeParams, List<Type/*!*/>/*!*/ actualTypeParams) {
+ Contract.Requires(cce.NonNullElements(actualTypeParams));
+ Contract.Requires(typeParams != null);
+ Contract.Requires(typeParams.Length == actualTypeParams.Count);
+ Contract.Ensures(Contract.Result<TypeParamInstantiation>() != null);
+
if (typeParams.Length == 0)
return EMPTY;
- List<TypeVariable!>! typeParamList = new List<TypeVariable!> ();
- IDictionary<TypeVariable!, Type!>! dict = new Dictionary<TypeVariable!, Type!> ();
+ List<TypeVariable/*!*/>/*!*/ typeParamList = new List<TypeVariable/*!*/>();
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
for (int i = 0; i < typeParams.Length; ++i) {
typeParamList.Add(typeParams[i]);
dict.Add(typeParams[i], actualTypeParams[i]);
@@ -2790,18 +3583,28 @@ namespace Microsoft.Boogie return new SimpleTypeParamInstantiation(typeParamList, dict);
}
- public static readonly TypeParamInstantiation! EMPTY =
- new SimpleTypeParamInstantiation (new List<TypeVariable!> (),
- new Dictionary<TypeVariable!, Type!> ());
+ public static readonly TypeParamInstantiation EMPTY =
+ new SimpleTypeParamInstantiation(new List<TypeVariable/*!*/>(),
+ new Dictionary<TypeVariable/*!*/, Type/*!*/>());
+ [ContractInvariantMethod]
+ void EMPTYInvariant() {
+ Contract.Invariant(EMPTY != null);
+ }
+
// return what formal type parameters there are
- public List<TypeVariable!>! FormalTypeParams { get {
- return TypeParams;
- } }
+ public List<TypeVariable/*!*/>/*!*/ FormalTypeParams {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
+ return TypeParams;
+ }
+ }
// given a formal type parameter, return the actual instantiation
- public Type! this[TypeVariable! var] { get {
- return Instantiations[var];
- } }
+ public Type/*!*/ this[TypeVariable/*!*/ var] {
+ get {
+ return Instantiations[var];
+ }
+ }
}
// Implementation of TypeParamInstantiation that refers to the current
@@ -2809,49 +3612,63 @@ namespace Microsoft.Boogie // methods of this implementation can change in case the MapTypeProxy
// receives further unifications.
class MapTypeProxyParamInstantiation : TypeParamInstantiation {
- private readonly MapTypeProxy! Proxy;
+ private readonly MapTypeProxy/*!*/ Proxy;
// the argument and result type of this particular usage of the map
// type. these are necessary to derive the values of the type parameters
- private readonly TypeSeq! ArgumentsResult;
+ private readonly TypeSeq/*!*/ ArgumentsResult;
// field that is initialised once all necessary information is available
// (the MapTypeProxy is instantiated to an actual type) and the instantiation
// of a type parameter is queried
- private IDictionary<TypeVariable!, Type!> Instantiations = null;
+ private IDictionary<TypeVariable/*!*/, Type/*!*/> Instantiations = null;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Proxy != null);
+ Contract.Invariant(ArgumentsResult != null);
+ Contract.Invariant(cce.NonNullElements(Instantiations));
+ }
- public MapTypeProxyParamInstantiation(MapTypeProxy! proxy,
- TypeSeq! argumentsResult) {
+
+ public MapTypeProxyParamInstantiation(MapTypeProxy/*!*/ proxy,
+ TypeSeq/*!*/ argumentsResult) {
+ Contract.Requires(proxy != null);
+ Contract.Requires(argumentsResult != null);
this.Proxy = proxy;
this.ArgumentsResult = argumentsResult;
}
// return what formal type parameters there are
- public List<TypeVariable!>! FormalTypeParams { get {
- MapType realType = Proxy.ProxyFor as MapType;
- if (realType == null)
- // no instantiation of the map type is known, which means
- // that the map type is assumed to be monomorphic
- return new List<TypeVariable!> ();
- else
- return realType.TypeParameters.ToList();
- } }
+ public List<TypeVariable/*!*/>/*!*/ FormalTypeParams {
+ get {
+ MapType realType = Proxy.ProxyFor as MapType;
+ if (realType == null)
+ // no instantiation of the map type is known, which means
+ // that the map type is assumed to be monomorphic
+ return new List<TypeVariable/*!*/>();
+ else
+ return realType.TypeParameters.ToList();
+ }
+ }
// given a formal type parameter, return the actual instantiation
- public Type! this[TypeVariable! var] { get {
- // then there has to be an instantiation that is a polymorphic map type
- if (Instantiations == null) {
- MapType realType = Proxy.ProxyFor as MapType;
- assert realType != null;
- TypeSeq! formalArgs = new TypeSeq ();
- foreach (Type! t in realType.Arguments)
- formalArgs.Add(t);
- formalArgs.Add(realType.Result);
- Instantiations =
- Type.InferTypeParameters(realType.TypeParameters, formalArgs, ArgumentsResult);
- }
- return Instantiations[var];
- } }
+ public Type/*!*/ this[TypeVariable/*!*/ var] {
+ get {
+ // then there has to be an instantiation that is a polymorphic map type
+ if (Instantiations == null) {
+ MapType realType = Proxy.ProxyFor as MapType;
+ Contract.Assert(realType != null);
+ TypeSeq/*!*/ formalArgs = new TypeSeq();
+ foreach (Type/*!*/ t in realType.Arguments) {
+ Contract.Assert(t != null);
+ formalArgs.Add(t);
+ }
+ formalArgs.Add(realType.Result);
+ Instantiations =
+ Type.InferTypeParameters(realType.TypeParameters, formalArgs, ArgumentsResult);
+ }
+ return Instantiations[var];
+ }
+ }
}
-
-}
+}
\ No newline at end of file |