diff options
Diffstat (limited to 'Source/AIFramework/VariableMap/MicroLattice.cs')
| -rw-r--r-- | Source/AIFramework/VariableMap/MicroLattice.cs | 42 |
1 files changed, 34 insertions, 8 deletions
diff --git a/Source/AIFramework/VariableMap/MicroLattice.cs b/Source/AIFramework/VariableMap/MicroLattice.cs index d38a37c0..ef98f8f7 100644 --- a/Source/AIFramework/VariableMap/MicroLattice.cs +++ b/Source/AIFramework/VariableMap/MicroLattice.cs @@ -5,22 +5,24 @@ //-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework
{
- using Microsoft.Contracts;
+ using System.Diagnostics.Contracts;
using System.Collections;
using System.Diagnostics;
- using System.Compiler;
+ //using System.Compiler;
using Microsoft.AbstractInterpretationFramework.Collections;
/// <summary>
/// Interface for a lattice that works on a per-variable basis.
/// </summary>
+ ///
+ [ContractClass(typeof(MicroLatticeContracts))]
public abstract class MicroLattice : MathematicalLattice
{
/// <summary>
/// Returns the predicate on the given variable for the given
/// lattice element.
/// </summary>
- public abstract IExpr! ToPredicate(IVariable! v, Element! e);
+ public abstract IExpr/*!*/ ToPredicate(IVariable/*!*/ v, Element/*!*/ e);
/* requires !e.IsBottom && !e.IsTop; */
/// <summary>
@@ -39,7 +41,7 @@ namespace Microsoft.AbstractInterpretationFramework /// <param name="f">The function symbol.</param>
/// <param name="args">The argument context.</param>
/// <returns>True if it may understand f, false if it does not understand f.</returns>
- public abstract bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args);
+ public abstract bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args);
/// <summary>
/// Set this property to true if the implemented MicroLattice can handle basic arithmetic.
@@ -56,15 +58,16 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
/// <param name="e">The predicate that is assumed to contain 1 variable.</param>
/// <returns>The most precise lattice element that is implied by the predicate.</returns>
- public abstract Element! EvaluatePredicate(IExpr! e);
+ public abstract Element/*!*/ EvaluatePredicate(IExpr/*!*/ e);
/// <summary>
/// Evaluate the predicate e and yield an overapproximation of the predicate under the state that is passed as a parameter
/// Note that unless the subclass implement it, the default behavior is to evaluate the predicate stateless, that implies that it
/// is evaluated in any possible context, i.e. it is an upper approximation
/// </summary>
- public virtual Element! EvaluatePredicateWithState(IExpr! e, IFunctionalMap state)
- {
+ public virtual Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ e, IFunctionalMap state){
+Contract.Requires(e != null);
+Contract.Ensures(Contract.Result<Element>() != null);
return EvaluatePredicate(e);
}
@@ -74,6 +77,29 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
/// <param name="e">A lattice element.</param>
/// <returns>The null value if no such expression can be given.</returns>
- public abstract IExpr GetFoldExpr(Element! e);
+ public abstract IExpr GetFoldExpr(Element/*!*/ e);
+ }
+ [ContractClassFor(typeof(MicroLattice))]
+ public abstract class MicroLatticeContracts : MicroLattice {
+ public override IExpr ToPredicate(IVariable v, MathematicalLattice.Element e) {
+ Contract.Requires(v != null);
+ Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ throw new System.NotImplementedException();
+ }
+ public override bool Understands(IFunctionSymbol f, IList args) {
+ Contract.Requires(f != null);
+ Contract.Requires(args != null);
+ throw new System.NotImplementedException();
+ }
+ public override Element EvaluatePredicate(IExpr e) {
+ Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ throw new System.NotImplementedException();
+ }
+ public override IExpr GetFoldExpr(MathematicalLattice.Element e) {
+ Contract.Requires(e != null);
+ throw new System.NotImplementedException();
+ }
}
}
\ No newline at end of file |