diff options
| author |  tabarbe <unknown> | 2010-08-26 23:38:33 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-26 23:38:33 +0000 |
| commit | 1188039043117d026e6cdfe13d35aed03880fea7 (patch) | |
| tree | bff79efa62b4ce001422c62c525618c5f235e1b0 /Source/AIFramework/VariableMap/Intervals.cs | |
| parent | 47171ab9f9d31dab0d5e0a4c3c95c763452e9295 (diff) | |
Boogie: AIFramework port part 1/3: Committing new sources.
Diffstat (limited to 'Source/AIFramework/VariableMap/Intervals.cs')
| -rw-r--r-- | Source/AIFramework/VariableMap/Intervals.cs | 884 |
1 files changed, 487 insertions, 397 deletions
diff --git a/Source/AIFramework/VariableMap/Intervals.cs b/Source/AIFramework/VariableMap/Intervals.cs index f507e020..73a1352f 100644 --- a/Source/AIFramework/VariableMap/Intervals.cs +++ b/Source/AIFramework/VariableMap/Intervals.cs @@ -5,47 +5,48 @@ //-----------------------------------------------------------------------------
using System;
using System.Collections;
-using System.Compiler.Analysis;
+//using System.Compiler.Analysis;
using Microsoft.AbstractInterpretationFramework.Collections;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
/////////////////////////////////////////////////////////////////////////////////
// An implementation of the interval abstract domain
/////////////////////////////////////////////////////////////////////////////////
-namespace Microsoft.AbstractInterpretationFramework
-{
- public class IntervalLattice : MicroLattice
- {
- readonly ILinearExprFactory! factory;
-
- public IntervalLattice(ILinearExprFactory! factory)
- {
+namespace Microsoft.AbstractInterpretationFramework {
+ public class IntervalLattice : MicroLattice {
+ readonly ILinearExprFactory/*!*/ factory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(factory != null);
+ }
+
+
+ public IntervalLattice(ILinearExprFactory/*!*/ factory) {
+ Contract.Requires(factory != null);
this.factory = factory;
// base();
}
- public override bool UnderstandsBasicArithmetics
- {
- get
- {
+ public override bool UnderstandsBasicArithmetics {
+ get {
return true;
}
}
- public override Element! Top
- {
- get
- {
+ public override Element/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+
return IntervalElement.Top;
}
}
-
- public override Element! Bottom
- {
- get
- {
+
+ public override Element/*!*/ Bottom {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+
return IntervalElement.Bottom;
}
}
@@ -53,47 +54,51 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// The paramter is the top?
/// </summary>
- public override bool IsTop(Element! element)
- {
- IntervalElement interval = (IntervalElement) element;
-
- return interval.IsTop(); + public override bool IsTop(Element/*!*/ element) {
+ Contract.Requires(element != null);
+ IntervalElement interval = (IntervalElement)element;
+
+ return interval.IsTop();
}
/// <summary>
/// The parameter is the bottom?
/// </summary>
- public override bool IsBottom(Element! element)
- {
- IntervalElement interval = (IntervalElement) element;
-
- return interval.IsBottom(); + public override bool IsBottom(Element/*!*/ element) {
+ Contract.Requires(element != null);
+ IntervalElement interval = (IntervalElement)element;
+
+ return interval.IsBottom();
}
/// <summary>
/// The classic, pointwise, join of intervals
/// </summary>
- public override Element! NontrivialJoin(Element! left, Element! right)
- {
- IntervalElement! leftInterval = (IntervalElement!) left;
- IntervalElement! rightInterval = (IntervalElement) right;
-
+ public override Element/*!*/ NontrivialJoin(Element/*!*/ left, Element/*!*/ right) {
+ Contract.Requires(right != null);
+ Contract.Requires(left != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
+ IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
+
ExtendedInt inf = ExtendedInt.Inf(leftInterval.Inf, rightInterval.Inf);
ExtendedInt sup = ExtendedInt.Sup(leftInterval.Sup, rightInterval.Sup);
- IntervalElement! join = IntervalElement.Factory(inf, sup);
+ IntervalElement/*!*/ join = IntervalElement.Factory(inf, sup);
- return join; + return join;
}
/// <summary>
/// The classic, pointwise, meet of intervals
/// </summary>
- public override Element! NontrivialMeet(Element! left, Element! right)
- {
- IntervalElement! leftInterval = (IntervalElement!) left;
- IntervalElement! rightInterval = (IntervalElement) right;
-
+ public override Element/*!*/ NontrivialMeet(Element/*!*/ left, Element/*!*/ right) {
+ Contract.Requires(right != null);
+ Contract.Requires(left != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
+ IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
+
ExtendedInt inf = ExtendedInt.Sup(leftInterval.Inf, rightInterval.Inf);
ExtendedInt sup = ExtendedInt.Inf(leftInterval.Sup, rightInterval.Sup);
@@ -105,11 +110,13 @@ namespace Microsoft.AbstractInterpretationFramework /// The very simple widening of intervals, to be improved with thresholds
/// left is the PREVIOUS value in the iterations and right is the NEW one
/// </summary>
- public override Element! Widen(Element! left, Element! right)
- {
- IntervalElement! prevInterval = (IntervalElement!) left;
- IntervalElement! nextInterval = (IntervalElement!) right;
-
+ public override Element/*!*/ Widen(Element/*!*/ left, Element/*!*/ right) {
+ Contract.Requires(right != null);
+ Contract.Requires(left != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ IntervalElement/*!*/ prevInterval = (IntervalElement/*!*/)cce.NonNull(left);
+ IntervalElement/*!*/ nextInterval = (IntervalElement/*!*/)cce.NonNull(right);
+
ExtendedInt inf = nextInterval.Inf < prevInterval.Inf ? ExtendedInt.MinusInfinity : prevInterval.Inf;
ExtendedInt sup = nextInterval.Sup > prevInterval.Sup ? ExtendedInt.PlusInfinity : prevInterval.Sup;
@@ -122,12 +129,13 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Return true iff the interval left is containted in right
/// </summary>
- protected override bool AtMost(Element! left, Element! right)
- {
- IntervalElement! leftInterval = (IntervalElement!) left;
- IntervalElement! rightInterval = (IntervalElement!) right;
+ protected override bool AtMost(Element/*!*/ left, Element/*!*/ right) {
+ Contract.Requires(right != null);
+ Contract.Requires(left != null);
+ IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
+ IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
- if(leftInterval.IsBottom() || rightInterval.IsTop())
+ if (leftInterval.IsBottom() || rightInterval.IsTop())
return true;
return rightInterval.Inf <= leftInterval.Inf && leftInterval.Sup <= rightInterval.Sup;
@@ -136,17 +144,19 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Return just null
/// </summary>
- public override IExpr GetFoldExpr(Element! element)
- {
+ public override IExpr GetFoldExpr(Element/*!*/ element) {
+ Contract.Requires(element != null);
return null;
- }
+ }
/// <summary>
/// return a predicate inf "\leq x and x "\leq" sup (if inf [or sup] is not oo)
/// </summary>
- public override IExpr! ToPredicate(IVariable! var, Element! element)
- {
- IntervalElement! interval = (IntervalElement!) element; + public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element){
+Contract.Requires(element != null);
+Contract.Requires(var != null);
+Contract.Ensures(Contract.Result<IExpr>() != null);
+IntervalElement/*!*/ interval = (IntervalElement/*!*/)cce.NonNull(element); IExpr lowerBound = null;
IExpr upperBound = null; @@ -171,38 +181,41 @@ namespace Microsoft.AbstractInterpretationFramework return upperBound; else // If we reach this point, both lowerBound and upperBound are null, i.e. we have no bounds on var, so we return simply true...
return this.factory.True;
- }
+ }
/// <summary>
/// For the moment consider just equalities. Other case must be considered
/// </summary>
- public override bool Understands(IFunctionSymbol! f, IList /*<IExpr*/ ! args)
- {
- return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq); + public override bool Understands(IFunctionSymbol/*!*/ f, IList /*<IExpr*//*!*/ args) {
+ Contract.Requires(args != null);
+ Contract.Requires(f != null);
+ return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
}
/// <summary>
/// Evaluate the predicate passed as input according the semantics of intervals
/// </summary>
- public override Element! EvaluatePredicate(IExpr! pred)
- {
+ public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ pred) {
+ Contract.Requires(pred != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
return this.EvaluatePredicateWithState(pred, null);
}
-
+
/// <summary>
/// Evaluate the predicate passed as input according the semantics of intervals and the given state.
/// Right now just basic arithmetic operations are supported. A future extension may consider an implementation of boolean predicates
/// </summary>
- public override Element! EvaluatePredicateWithState(IExpr! pred, IFunctionalMap/* Var -> Element */ state)
- {
+ public override Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ pred, IFunctionalMap/* Var -> Element */ state){
+Contract.Requires(pred != null);
+Contract.Ensures(Contract.Result<Element>() != null);
if(pred is IFunApp)
{
IFunApp fun = (IFunApp) pred;
if(fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
{
- IExpr! leftArg = (IExpr!) fun.Arguments[0];
- IExpr! rightArg = (IExpr!) fun.Arguments[1];
+ IExpr/*!*/ leftArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
if (leftArg is IVariable) {
return Eval(rightArg, state);
} else if (rightArg is IVariable) {
@@ -217,10 +230,11 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Evaluate the expression (that is assured to be an arithmetic expression, in the state passed as a parameter
/// </summary>
- private IntervalElement! Eval(IExpr! exp, IFunctionalMap/* Var -> Element */ state)
- {
+ private IntervalElement/*!*/ Eval(IExpr/*!*/ exp, IFunctionalMap/* Var -> Element */ state) {
+Contract.Requires((exp != null));
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
- IntervalElement! retVal = (IntervalElement!) Top;
+ IntervalElement/*!*/ retVal = (IntervalElement/*!*/)cce.NonNull(Top);
// Eval the expression by structural induction
@@ -248,19 +262,23 @@ namespace Microsoft.AbstractInterpretationFramework }
else if(fun.FunctionSymbol.Equals(Int.Negate)) // An unary minus
{
- IExpr! arg = (IExpr!) fun.Arguments[0];
- IntervalElement! argEval = Eval(arg, state);
- IntervalElement! zero = IntervalElement.Factory(BigNum.ZERO);
+ IExpr/*!*/ arg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IntervalElement/*!*/ argEval = Eval(arg, state);
+ Contract.Assert(argEval != null);
+ IntervalElement/*!*/ zero = IntervalElement.Factory(BigNum.ZERO);
+ Contract.Assert(zero != null);
retVal = zero - argEval;
}
else if(fun.Arguments.Count == 2)
{
- IExpr! left = (IExpr!) fun.Arguments[0];
- IExpr! right = (IExpr!) fun.Arguments[1];
+ IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
- IntervalElement! leftVal = Eval(left, state);
- IntervalElement! rightVal = Eval(right, state);
+ IntervalElement/*!*/ leftVal = Eval(left, state);
+ Contract.Assert(leftVal != null);
+ IntervalElement/*!*/ rightVal = Eval(right, state);
+ Contract.Assert(rightVal != null);
if(fun.FunctionSymbol.Equals(Int.Add))
retVal = leftVal + rightVal;
@@ -281,165 +299,199 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Inner class standing for an interval on integers, possibly unbounded
/// </summary>
- private class IntervalElement : Element
- {
- protected static readonly IntervalElement! TopInterval = new IntervalElement(new MinusInfinity(), new PlusInfinity()); // Top = [-oo , +oo]
- protected static readonly IntervalElement! BottomInterval = new IntervalElement(new PlusInfinity(), new MinusInfinity()); // Bottom = [+oo, -oo]
+ private class IntervalElement : Element {
+ protected static readonly IntervalElement/*!*/ TopInterval = new IntervalElement(new MinusInfinity(), new PlusInfinity()); // Top = [-oo , +oo]
+ protected static readonly IntervalElement/*!*/ BottomInterval = new IntervalElement(new PlusInfinity(), new MinusInfinity()); // Bottom = [+oo, -oo]
+
+ private readonly ExtendedInt/*!*/ inf;
+ private readonly ExtendedInt/*!*/ sup;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(inf != null);
+ Contract.Invariant(sup != null);
+ }
- private readonly ExtendedInt! inf;
- private readonly ExtendedInt! sup;
-
- public ExtendedInt! Inf
- {
- get
- {
- return inf;
- }
- }
-
- public ExtendedInt! Sup
- {
- get
- {
- return sup;
- }
- }
-
- // Construct the inteval [val, val]
- protected IntervalElement(BigNum val)
- {
- this.inf = this.sup = ExtendedInt.Factory(val);
- // base();
- }
+ public ExtendedInt/*!*/ Inf {
+ get {
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- // Construct the interval [inf, sup]
- protected IntervalElement(BigNum infInt, BigNum supInt)
- {
- this.inf = ExtendedInt.Factory(infInt);
- this.sup = ExtendedInt.Factory(supInt);
- // base(); // to please the compiler...
- }
-
- protected IntervalElement(ExtendedInt! inf, ExtendedInt! sup)
- {
- this.inf = inf;
- this.sup = sup;
- // base();
+ return inf;
}
+ }
- // Construct an Interval
- public static IntervalElement! Factory(ExtendedInt! inf, ExtendedInt! sup)
- {
- if(inf is MinusInfinity && sup is PlusInfinity)
- return Top;
- if(inf > sup)
- return Bottom;
- // otherwise...
- return new IntervalElement(inf, sup);
- }
+ public ExtendedInt/*!*/ Sup {
+ get {
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- public static IntervalElement! Factory(BigNum i)
- {
- return new IntervalElement(i);
+ return sup;
}
+ }
- public static IntervalElement! Factory(BigNum inf, BigNum sup)
- {
- ExtendedInt! i = ExtendedInt.Factory(inf);
- ExtendedInt! s = ExtendedInt.Factory(sup);
+ // Construct the inteval [val, val]
+ protected IntervalElement(BigNum val) {
+ this.inf = this.sup = ExtendedInt.Factory(val);
+ // base();
+ }
+
+ // Construct the interval [inf, sup]
+ protected IntervalElement(BigNum infInt, BigNum supInt) {
+ this.inf = ExtendedInt.Factory(infInt);
+ this.sup = ExtendedInt.Factory(supInt);
+ // base(); // to please the compiler...
+ }
+
+ protected IntervalElement(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
+ this.inf = inf;
+ this.sup = sup;
+ // base();
+ }
+
+ // Construct an Interval
+ public static IntervalElement/*!*/ Factory(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires((sup != null));
+Contract.Requires((inf != null));
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ if (inf is MinusInfinity && sup is PlusInfinity)
+ return Top;
+ if (inf > sup)
+ return Bottom;
+ // otherwise...
+ return new IntervalElement(inf, sup);
+ }
+
+ public static IntervalElement/*!*/ Factory(BigNum i) {
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ return new IntervalElement(i);
+ }
+
+ public static IntervalElement/*!*/ Factory(BigNum inf, BigNum sup) {
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ i = ExtendedInt.Factory(inf);
+ ExtendedInt/*!*/ s = ExtendedInt.Factory(sup);
return Factory(i, s);
}
- static public IntervalElement! Top
- {
- get
- {
- return TopInterval;
- }
- }
+ static public IntervalElement/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
- static public IntervalElement! Bottom
- {
- get
- {
- return BottomInterval;
- }
+ return TopInterval;
}
+ }
- public bool IsTop()
- {
- return this.inf is MinusInfinity && this.sup is PlusInfinity;
- }
+ static public IntervalElement/*!*/ Bottom {
+ get {
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
- public bool IsBottom()
- {
- return this.inf > this.sup;
+ return BottomInterval;
}
+ }
- #region Below are the arithmetic operations lifted to intervals
+ public bool IsTop() {
+ return this.inf is MinusInfinity && this.sup is PlusInfinity;
+ }
- // Addition
- public static IntervalElement! operator+(IntervalElement! a, IntervalElement! b)
- {
- ExtendedInt! inf = a.inf + b.inf;
- ExtendedInt! sup = a.sup + b.sup;
+ public bool IsBottom() {
+ return this.inf > this.sup;
+ }
+
+ #region Below are the arithmetic operations lifted to intervals
+
+ // Addition
+ public static IntervalElement/*!*/ operator +(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ inf = a.inf + b.inf;
+ Contract.Assert(inf != null);
+ ExtendedInt/*!*/ sup = a.sup + b.sup;
+ Contract.Assert(sup != null);
return Factory(inf, sup); }
- // Subtraction
- public static IntervalElement! operator-(IntervalElement! a, IntervalElement! b)
- {
- ExtendedInt! inf = a.inf - b.sup;
- ExtendedInt! sup = a.sup - b.inf;
-
- IntervalElement! sub = Factory(inf, sup); + // Subtraction
+ public static IntervalElement/*!*/ operator -(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ inf = a.inf - b.sup;
+ Contract.Assert(inf != null);
+
+ ExtendedInt/*!*/ sup = a.sup - b.inf;
+Contract.Assert(sup != null);
+IntervalElement/*!*/ sub = Factory(inf, sup);
+Contract.Assert(sub != null); return sub;
- }
-
- // Multiplication
- public static IntervalElement! operator*(IntervalElement! a, IntervalElement! b)
- {
- ExtendedInt! infinf = a.inf * b.inf;
- ExtendedInt! infsup = a.inf * b.sup;
- ExtendedInt! supinf = a.sup * b.inf;
- ExtendedInt! supsup = a.sup * b.sup;
+ }
- ExtendedInt! inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
- ExtendedInt! sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+ // Multiplication
+ public static IntervalElement/*!*/ operator *(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ infinf = a.inf * b.inf;
+ Contract.Assert(infinf != null);
+ ExtendedInt/*!*/ infsup = a.inf * b.sup;
+ Contract.Assert(infsup != null);
+ ExtendedInt/*!*/ supinf = a.sup * b.inf;
+ Contract.Assert(supinf != null);
+ ExtendedInt/*!*/ supsup = a.sup * b.sup;
+ Contract.Assert(supsup != null);
+
+ ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+ Contract.Assert(inf != null);
+ ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+ Contract.Assert(sup != null);
return Factory(inf, sup);
}
- // Division
- public static IntervalElement! operator/(IntervalElement! a, IntervalElement! b)
- {
+ // Division
+ public static IntervalElement/*!*/ operator /(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
if(b.inf.IsZero && b.sup.IsZero) // Check division by zero
return IntervalElement.Top;
- ExtendedInt! infinf = a.inf / b.inf;
- ExtendedInt! infsup = a.inf / b.sup;
- ExtendedInt! supinf = a.sup / b.inf;
- ExtendedInt! supsup = a.sup / b.sup;
+ ExtendedInt/*!*/ infinf = a.inf / b.inf;
+ Contract.Assert(infinf != null);
+ ExtendedInt/*!*/ infsup = a.inf / b.sup;
+ Contract.Assert(infsup != null);
+ ExtendedInt/*!*/ supinf = a.sup / b.inf;
+ Contract.Assert(supinf != null);
+ ExtendedInt/*!*/ supsup = a.sup / b.sup;
+ Contract.Assert(supsup != null);
- ExtendedInt! inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
- ExtendedInt! sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+ ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+ Contract.Assert(inf != null);
+ ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+ Contract.Assert(sup != null);
return Factory(inf, sup);
}
- // Division
- public static IntervalElement! operator%(IntervalElement! a, IntervalElement! b)
- {
+ // Division
+ public static IntervalElement/*!*/ operator %(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
if(b.inf.IsZero && b.sup.IsZero) // Check division by zero
return IntervalElement.Top;
- ExtendedInt! infinf = a.inf % b.inf;
- ExtendedInt! infsup = a.inf % b.sup;
- ExtendedInt! supinf = a.sup % b.inf;
- ExtendedInt! supsup = a.sup % b.sup;
+ ExtendedInt/*!*/ infinf = a.inf % b.inf;
+ Contract.Assert(infinf != null);
+ ExtendedInt/*!*/ infsup = a.inf % b.sup;
+ Contract.Assert(infsup != null);
+ ExtendedInt/*!*/ supinf = a.sup % b.inf;
+ Contract.Assert(supinf != null);
+ ExtendedInt/*!*/ supsup = a.sup % b.sup;
+ Contract.Assert(supsup != null);
ExtendedInt inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
ExtendedInt sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
@@ -447,67 +499,72 @@ namespace Microsoft.AbstractInterpretationFramework return Factory(inf, sup);
}
- #endregion
+ #endregion
- #region Overriden methods
+ #region Overriden methods
- public override Element! Clone()
- {
- // Real copying should not be needed because intervals are immutable?
- return this;
- /*
- int valInf = this.inf.Value;
- int valSup = this.sup.Value;
+ public override Element/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ // Real copying should not be needed because intervals are immutable?
+ return this;
+ /*
+ int valInf = this.inf.Value;
+ int valSup = this.sup.Value;
- ExtendedInt clonedInf = ExtendedInt.Factory(valInf);
- ExtendedInt clonedSup = ExtendedInt.Factory(valSup);
+ ExtendedInt clonedInf = ExtendedInt.Factory(valInf);
+ ExtendedInt clonedSup = ExtendedInt.Factory(valSup);
- return Factory(clonedInf, clonedSup);
- */
- }
+ return Factory(clonedInf, clonedSup);
+ */
+ }
- [Pure]
- public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
- {
- return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
+ [Pure]
+ public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
+return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
}
- [Pure]
- public override string! ToString()
- {
- return "[" + this.inf + ", " + this.sup + "]";
- }
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return "[" + this.inf + ", " + this.sup + "]";
+ }
- #endregion
+ #endregion
}
-}
+ }
+
-
/// The interface for an extended integer
- abstract class ExtendedInt
- {
- private static readonly PlusInfinity! cachedPlusInf = new PlusInfinity();
- private static readonly MinusInfinity! cachedMinusInf = new MinusInfinity();
-
- static public ExtendedInt! PlusInfinity
- {
- get
- {
+ ///
+ [ContractClass(typeof(ExtendedIntContracts))]
+ abstract class ExtendedInt {
+ private static readonly PlusInfinity/*!*/ cachedPlusInf = new PlusInfinity();
+ private static readonly MinusInfinity/*!*/ cachedMinusInf = new MinusInfinity();
+
+ static public ExtendedInt/*!*/ PlusInfinity {
+ get {
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+
return cachedPlusInf;
}
}
- static public ExtendedInt! MinusInfinity
- {
- get
- {
+ static public ExtendedInt/*!*/ MinusInfinity {
+ get {
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+
return cachedMinusInf;
- }
+ }
}
- public abstract BigNum Value { get; }
+ public abstract BigNum Value {
+ get;
+ }
- public abstract int Signum { get; }
+ public abstract int Signum {
+ get;
+ }
public bool IsZero {
get {
@@ -531,158 +588,188 @@ namespace Microsoft.AbstractInterpretationFramework #region Below are the extensions of arithmetic operations on extended integers
// Addition
- public static ExtendedInt! operator+(ExtendedInt! a, ExtendedInt! b)
- {
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
- return b;
- } else {
- return ExtendedInt.Factory(a.Value + b.Value);
- }
+ public static ExtendedInt/*!*/ operator +(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return b;
+ } else {
+ return ExtendedInt.Factory(a.Value + b.Value);
+ }
}
// Subtraction
- public static ExtendedInt! operator-(ExtendedInt! a, ExtendedInt! b)
- {
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
- return UnaryMinus(b);
- } else {
- return ExtendedInt.Factory(a.Value - b.Value);
- }
- }
-
+ public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return UnaryMinus(b);
+ } else {
+ return ExtendedInt.Factory(a.Value - b.Value);
+ }
+ }
+
// Unary minus
- public static ExtendedInt! operator-(ExtendedInt! a)
- {
+ public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a) {
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
// BUGBUG: Some compiler error prevents the unary minus operator from being used
return UnaryMinus(a);
}
// Unary minus
- public static ExtendedInt! UnaryMinus(ExtendedInt! a)
- {
- if(a is PlusInfinity)
+ public static ExtendedInt/*!*/ UnaryMinus(ExtendedInt/*!*/ a) {
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (a is PlusInfinity)
return cachedMinusInf;
- if(a is MinusInfinity)
+ if (a is MinusInfinity)
return cachedPlusInf;
else // a is a PureInteger
return new PureInteger(-a.Value);
}
// Multiplication
- public static ExtendedInt! operator*(ExtendedInt! a, ExtendedInt! b)
- {
- if (a.IsZero) {
+ public static ExtendedInt/*!*/ operator *(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (a.IsZero) {
+ return a;
+ } else if (b.IsZero) {
+ return b;
+ } else if (a is InfinitaryInt) {
+ if (b.IsPositive) {
return a;
- } else if (b.IsZero) {
- return b;
- } else if (a is InfinitaryInt) {
- if (b.IsPositive) {
- return a;
- } else {
- return UnaryMinus(a);
- }
- } else if (b is InfinitaryInt) {
- if (a.IsPositive) {
- return b;
- } else {
- return UnaryMinus(b);
- }
} else {
- return ExtendedInt.Factory(a.Value * b.Value);
+ return UnaryMinus(a);
}
- }
-
- // Division
- public static ExtendedInt! operator/(ExtendedInt! a, ExtendedInt! b)
- {
- if(b.IsZero)
- {
- return a.IsPositive? (ExtendedInt) cachedPlusInf : cachedMinusInf;
- }
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
+ } else if (b is InfinitaryInt) {
+ if (a.IsPositive) {
return b;
} else {
- return ExtendedInt.Factory(a.Value / b.Value);
+ return UnaryMinus(b);
}
+ } else {
+ return ExtendedInt.Factory(a.Value * b.Value);
+ }
+ }
+
+ // Division
+ public static ExtendedInt/*!*/ operator /(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (b.IsZero) {
+ return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf;
+ }
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return b;
+ } else {
+ return ExtendedInt.Factory(a.Value / b.Value);
+ }
}
// Modulo
- public static ExtendedInt! operator%(ExtendedInt! a, ExtendedInt! b)
- {
- if(b.IsZero)
- {
- return a.IsPositive? (ExtendedInt) cachedPlusInf : cachedMinusInf;
- }
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
- return b;
- } else {
- return ExtendedInt.Factory(a.Value % b.Value);
- }
+ public static ExtendedInt/*!*/ operator %(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (b.IsZero) {
+ return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf;
+ }
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return b;
+ } else {
+ return ExtendedInt.Factory(a.Value % b.Value);
+ }
}
#endregion
#region Inf and Sup operations
- public abstract int CompareTo(ExtendedInt! that);
+ public abstract int CompareTo(ExtendedInt/*!*/ that);
- public static bool operator<(ExtendedInt! inf, ExtendedInt! sup)
- {
+ public static bool operator <(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
return inf.CompareTo(sup) < 0;
}
- public static bool operator>(ExtendedInt! inf, ExtendedInt! sup)
- {
+ public static bool operator >(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
return inf.CompareTo(sup) > 0;
}
- public static bool operator<=(ExtendedInt! inf, ExtendedInt! sup)
- {
+ public static bool operator <=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
return inf.CompareTo(sup) <= 0;
}
- public static bool operator>=(ExtendedInt! inf, ExtendedInt! sup)
- requires inf != null && sup != null;
- {
+ public static bool operator >=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
+ Contract.Requires(inf != null && sup != null);
return inf.CompareTo(sup) >= 0;
}
- public static ExtendedInt! Inf(ExtendedInt! inf, ExtendedInt! sup)
- {
- if(inf < sup)
+ public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (inf < sup)
return inf;
else
return sup;
}
- public static ExtendedInt! Inf(ExtendedInt! a, ExtendedInt! b, ExtendedInt! c, ExtendedInt! d)
- {
- ExtendedInt! infab = Inf(a,b);
- ExtendedInt! infcd = Inf(c,d);
+ public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d){
+Contract.Requires(d != null);
+Contract.Requires(c != null);
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ ExtendedInt/*!*/ infab = Inf(a,b);
+ Contract.Assert(infab != null);
+ ExtendedInt/*!*/ infcd = Inf(c, d);
+ Contract.Assert(infcd != null);
return Inf(infab, infcd);
}
-
- public static ExtendedInt! Sup(ExtendedInt! inf, ExtendedInt! sup)
- {
- if(inf > sup)
+
+ public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (inf > sup)
return inf;
else
return sup;
- }
+ }
- public static ExtendedInt! Sup(ExtendedInt! a, ExtendedInt! b, ExtendedInt! c, ExtendedInt! d)
- {
- ExtendedInt! supab = Sup(a,b);
- ExtendedInt! supcd = Sup(c,d);
+ public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d){
+Contract.Requires(d != null);
+Contract.Requires(c != null);
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ ExtendedInt/*!*/ supab = Sup(a,b);
+ Contract.Assert(supab != null);
+ ExtendedInt/*!*/ supcd = Sup(c, d);
+ Contract.Assert(supcd != null);
return Sup(supab, supcd);
}
@@ -690,101 +777,104 @@ namespace Microsoft.AbstractInterpretationFramework #endregion
// Return the ExtendedInt corresponding to the value
- public static ExtendedInt! Factory(BigNum val)
- {
+ public static ExtendedInt/*!*/ Factory(BigNum val) {
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
return new PureInteger(val);
}
- }
+ }
+ [ContractClassFor(typeof(ExtendedInt))]
+ abstract class ExtendedIntContracts : ExtendedInt {
+ public override int CompareTo(ExtendedInt that) {
+ Contract.Requires(that != null);
+ throw new NotImplementedException();
+ }
+ }
// Stands for a normal (finite) integer x
- class PureInteger : ExtendedInt
- {
- public PureInteger(BigNum i)
- {
+ class PureInteger : ExtendedInt {
+ public PureInteger(BigNum i) {
this.val = i;
}
[Pure]
- public override string! ToString()
- {
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
return this.Value.ToString();
}
private BigNum val;
public override BigNum Value {
- get
- {
+ get {
return this.val;
}
}
public override int Signum {
- get {
- return val.Signum;
- }
- }
-
- public override int CompareTo(ExtendedInt! that) {
- if (that is PlusInfinity)
- return -1;
- else if (that is PureInteger)
- return this.Value.CompareTo(that.Value);
- else // then that is a MinusInfinity
- return 1;
- }
+ get {
+ return val.Signum;
+ }
+ }
+
+ public override int CompareTo(ExtendedInt/*!*/ that) {
+ Contract.Requires(that != null);
+ if (that is PlusInfinity)
+ return -1;
+ else if (that is PureInteger)
+ return this.Value.CompareTo(that.Value);
+ else // then that is a MinusInfinity
+ return 1;
+ }
}
- abstract class InfinitaryInt : ExtendedInt
- {
- public override BigNum Value
- {
+ abstract class InfinitaryInt : ExtendedInt {
+ public override BigNum Value {
get {
throw new InvalidOperationException();
}
}
}
- class PlusInfinity : InfinitaryInt
- {
+ class PlusInfinity : InfinitaryInt {
[Pure]
- public override string! ToString()
- {
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
return "+oo";
}
public override int Signum {
- get {
- return 1;
- }
- }
-
- public override int CompareTo(ExtendedInt! that) {
- if (that is PlusInfinity)
- return 0;
- else
- return 1;
- }
+ get {
+ return 1;
+ }
+ }
+
+ public override int CompareTo(ExtendedInt/*!*/ that) {
+ Contract.Requires(that != null);
+ if (that is PlusInfinity)
+ return 0;
+ else
+ return 1;
+ }
}
- class MinusInfinity : InfinitaryInt
- {
+ class MinusInfinity : InfinitaryInt {
[Pure]
- public override string! ToString()
- {
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
return "-oo";
}
public override int Signum {
- get {
- return -1;
- }
- }
-
- public override int CompareTo(ExtendedInt! that) {
- if (that is MinusInfinity)
- return 0;
- else
- return -1;
- }
+ get {
+ return -1;
+ }
+ }
+
+ public override int CompareTo(ExtendedInt/*!*/ that) {
+ Contract.Requires(that != null);
+ if (that is MinusInfinity)
+ return 0;
+ else
+ return -1;
+ }
}
}
|