diff options
Diffstat (limited to 'Source/AIFramework/Expr.cs')
| -rw-r--r-- | Source/AIFramework/Expr.cs | 337 |
1 files changed, 259 insertions, 78 deletions
diff --git a/Source/AIFramework/Expr.cs b/Source/AIFramework/Expr.cs index 1f21f84a..58473592 100644 --- a/Source/AIFramework/Expr.cs +++ b/Source/AIFramework/Expr.cs @@ -16,7 +16,8 @@ namespace Microsoft.AbstractInterpretationFramework
{
using System.Collections;
- using Microsoft.Contracts;
+ using System;
+ using System.Diagnostics.Contracts;
//----------------------------- Expressions -----------------------------
@@ -28,6 +29,7 @@ namespace Microsoft.AbstractInterpretationFramework /// This only serves as a place for operations on expressions. Clients
/// should implement directly IVariable, IFunApp, ...
/// </summary>
+ [ContractClass(typeof(IExprContracts))]
public interface IExpr
{
/// <summary>
@@ -35,34 +37,62 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
/// <param name="visitor">The expression visitor.</param>
/// <returns>The result of the visit.</returns>
- [Pure] object DoVisit(ExprVisitor! visitor);
+ [Pure] object DoVisit(ExprVisitor/*!*/ visitor);
// TODO: Type checking of the expressions.
}
+ [ContractClassFor(typeof(IExpr))]
+ public abstract class IExprContracts:IExpr{
+ #region IExpr Members
+
+public object DoVisit(ExprVisitor visitor)
+{
+ Contract.Requires(visitor != null);
+ throw new System.NotImplementedException();
+}
+
+#endregion
+}
/// <summary>
/// An interface for variables.
///
/// This interface should be implemented by the client.
/// </summary>
+ [ContractClass(typeof(IVariableContracts))]
public interface IVariable : IExpr
{
- string! Name { get; } // Each client must define the name for variables
+ string/*!*/ Name { get; } // Each client must define the name for variables
+ }
+ [ContractClassFor(typeof(IVariable))]
+ public abstract class IVariableContracts:IVariable{
+ string IVariable.Name{get{Contract.Ensures(Contract.Result<string>() != null);throw new NotImplementedException();}
+
+ }
+
+ #region IExpr Members
+
+ object IExpr.DoVisit(ExprVisitor visitor) {
+ throw new NotImplementedException();
}
+ #endregion
+ }
+
/// <summary>
/// An interface for function applications.
///
/// This interface should be implemented by the client.
/// </summary>
+ ///
+ [ContractClass(typeof(IFunAppContracts))]
public interface IFunApp : IExpr
{
- IFunctionSymbol! FunctionSymbol { get; }
- IList/*<IExpr!>*/! Arguments
+ IFunctionSymbol/*!*/ FunctionSymbol { get; }
+ IList/*<IExpr!>*//*!*/ Arguments
{
- [Pure][Rep] get
- ensures result.IsReadOnly;
- ;
+ [Pure][Rep] get;
+
}
/// <summary>
@@ -72,23 +102,103 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
/// <param name="args">The new arguments.</param>
/// <returns>A copy of the function with the new arguments.</returns>
- IFunApp! CloneWithArguments(IList/*<IExpr!>*/! args)
- //TODO requires this.Arguments.Count == args.Count;
+ IFunApp/*!*/ CloneWithArguments(IList/*<IExpr!>*//*!*/ args)
+ //TODO Contract.Requires(this.Arguments.Count == args.Count);
;
}
+ [ContractClassFor(typeof(IFunApp))]
+public abstract class IFunAppContracts:IFunApp{
+
+#region IFunApp Members
+
+public IFunctionSymbol FunctionSymbol
+{
+ get {Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+ throw new System.NotImplementedException(); }
+}
+
+public IList Arguments
+{
+ get {Contract.Ensures(Contract.Result<IList>() != null);
+ Contract.Ensures(Contract.Result<IList>().IsReadOnly);
+ throw new System.NotImplementedException(); }
+}
+
+public IFunApp CloneWithArguments(IList args)
+{
+ Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+
+
+ throw new System.NotImplementedException();
+}
+
+#endregion
+
+#region IExpr Members
+
+object IExpr.DoVisit(ExprVisitor visitor) {
+ throw new NotImplementedException();
+}
+
+#endregion
+}
/// <summary>
/// An interface for anonymous functions (i.e., lambda expressions)
/// </summary>
+ [ContractClass(typeof(IFunctionContracts))]
public interface IFunction : IExpr
{
- IVariable! Param { get; }
- AIType! ParamType { get; }
- IExpr! Body { get; }
+ IVariable/*!*/ Param { get; }
+ AIType/*!*/ ParamType { get; }
+ IExpr/*!*/ Body { get; }
+
+ IFunction/*!*/ CloneWithBody(IExpr/*!*/ body);
+ }
+ [ContractClassFor(typeof(IFunction))]
+ public abstract class IFunctionContracts:IFunction{
+
+ #region IFunction Members
+
+ IVariable IFunction.Param {
+ get {
+ Contract.Ensures(Contract.Result<IVariable>() != null);
+ throw new NotImplementedException();
+ }
+ }
- IFunction! CloneWithBody(IExpr! body);
+ AIType IFunction.ParamType {
+ get {
+ Contract.Ensures(Contract.Result<AIType>() != null);
+ throw new NotImplementedException();
+ }
}
+ IExpr IFunction.Body {
+ get {
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ throw new NotImplementedException();
+ }
+ }
+
+ IFunction IFunction.CloneWithBody(IExpr body) {
+ Contract.Requires(body != null);
+ Contract.Ensures(Contract.Result<IFunction>() != null);
+ throw new NotImplementedException();
+ }
+
+ #endregion
+
+ #region IExpr Members
+
+ object IExpr.DoVisit(ExprVisitor visitor) {
+ throw new NotImplementedException();
+ }
+
+ #endregion
+ }
+
/// <summary>
/// An interface representing an expression that at any moment could, in principle, evaluate
/// to a different value. That is, the abstract interpreter should treat these IExpr's
@@ -100,25 +210,32 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// An abstract class that provides an interface for expression visitors.
/// </summary>
+ [ContractClass(typeof(ExprVisitorContracts))]
public abstract class ExprVisitor
{
- public abstract object Default(IExpr! expr);
+ public abstract object Default(IExpr/*!*/ expr);
- public virtual object VisitVariable(IVariable! var)
- {
+ public virtual object VisitVariable(IVariable/*!*/ var){
+Contract.Requires(var != null);
return Default(var);
}
- public virtual object VisitFunApp(IFunApp! funapp)
- {
+ public virtual object VisitFunApp(IFunApp/*!*/ funapp){
+Contract.Requires(funapp != null);
return Default(funapp);
}
- public virtual object VisitFunction(IFunction! fun)
- {
+ public virtual object VisitFunction(IFunction/*!*/ fun){
+Contract.Requires(fun != null);
return Default(fun);
}
}
+ [ContractClassFor(typeof(ExprVisitor))]
+ public abstract class ExprVisitorContracts:ExprVisitor{
+ public override object Default(IExpr expr)
+{
+ Contract.Requires(expr != null); throw new NotImplementedException();
+}}
/// <summary>
/// A utility class for dealing with expressions.
@@ -131,8 +248,11 @@ namespace Microsoft.AbstractInterpretationFramework /// <param name="subst">The expression to substitute.</param>
/// <param name="var">The variable to substitute for.</param>
/// <param name="inexpr">The expression to substitute into.</param>
- public static IExpr! Substitute(IExpr! subst, IVariable! var, IExpr! inexpr)
- {
+ public static IExpr/*!*/ Substitute(IExpr/*!*/ subst, IVariable/*!*/ var, IExpr/*!*/ inexpr){
+Contract.Requires(inexpr != null);
+Contract.Requires(var != null);
+Contract.Requires(subst != null);
+Contract.Ensures(Contract.Result<IExpr>() != null);
IExpr result = null;
if (inexpr is IVariable)
@@ -141,14 +261,20 @@ namespace Microsoft.AbstractInterpretationFramework }
else if (inexpr is IFunApp)
{
- IFunApp! funapp = (IFunApp!)inexpr;
+ IFunApp/*!*/ funapp = (IFunApp/*!*/)cce.NonNull(inexpr);
IList newargs = null;
- newargs = new ArrayList{ IExpr! arg in funapp.Arguments; Substitute(subst, var, arg) };
+
+ var x = new System.Collections.Generic.List<IExpr>();
+ foreach (IExpr arg in funapp.Arguments){
+ x.Add(Substitute(subst,var, arg));
+ }
+ newargs = new ArrayList(x);
+ //newargs = new ArrayList{ IExpr/*!*/ arg in funapp.Arguments; Substitute(subst, var, arg) };
result = funapp.CloneWithArguments(newargs);
}
else if (inexpr is IFunction)
{
- IFunction! fun = (IFunction!)inexpr;
+ IFunction/*!*/ fun = (IFunction/*!*/)cce.NonNull(inexpr);
if (fun.Param.Equals(var))
result = fun;
@@ -161,7 +287,7 @@ namespace Microsoft.AbstractInterpretationFramework }
else
{
- assert false;
+ {Contract.Assert(false);throw new cce.UnreachableException();}
}
return result;
@@ -179,10 +305,11 @@ namespace Microsoft.AbstractInterpretationFramework // out z)
// which sees if 'e' matches Prop.Imp(Prop.And(x,y),z) binding x,y,z to the subtrees.
//
- public delegate bool Matcher(IExpr! expr);
+ public delegate bool Matcher(IExpr/*!*/ expr);
- private static IFunApp/*?*/ MatchFunctionSymbol(IExpr! expr, IFunctionSymbol! f)
- {
+ private static IFunApp/*?*/ MatchFunctionSymbol(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f){
+Contract.Requires(f != null);
+Contract.Requires(expr != null);
IFunApp app = expr as IFunApp;
if (app != null)
{
@@ -195,15 +322,17 @@ namespace Microsoft.AbstractInterpretationFramework return null;
}
- public static bool Match(IExpr! expr, IFunctionSymbol! f, params Matcher[]! subs)
- {
+ public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, params Matcher[]/*!*/ subs){
+Contract.Requires(subs != null);
+Contract.Requires(f != null);
+Contract.Requires(expr != null);
IFunApp app = MatchFunctionSymbol(expr,f);
if (app != null)
{
int i = 0; // Note ***0***
- foreach (Matcher! s in subs)
- {
- if (!s((IExpr!)app.Arguments[i])) { return false; }
+ foreach(Matcher/*!*/ s in subs){
+Contract.Assert(s != null);
+ if (!s(cce.NonNull((IExpr)app.Arguments[i]))) { return false; }
i++;
}
return true;
@@ -212,19 +341,21 @@ namespace Microsoft.AbstractInterpretationFramework }
// Unary Binding
- public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, params Matcher[]! subs)
- {
+ public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, out IExpr arg0, params Matcher[]/*!*/ subs){
+Contract.Requires(subs != null);
+Contract.Requires(f != null);
+Contract.Requires(expr != null);
arg0 = null;
IFunApp app = MatchFunctionSymbol(expr,f);
if (app != null)
{
- arg0 = (IExpr!)app.Arguments[0];
+ arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]);
int i = 1; // Note ***1***
- foreach (Matcher! s in subs)
- {
- if (!s((IExpr!)app.Arguments[i])) { return false; }
+ foreach(Matcher/*!*/ s in subs){
+Contract.Assert(s != null);
+ if (!s(cce.NonNull((IExpr/*!*/)app.Arguments[i]))) { return false; }
i++;
}
return true;
@@ -233,21 +364,24 @@ namespace Microsoft.AbstractInterpretationFramework }
// Binary Binding
- public static bool Match(IExpr! expr, IFunctionSymbol! f, Matcher! sub0, out IExpr arg1, params Matcher[]! subs)
- {
+ public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, Matcher/*!*/ sub0, out IExpr arg1, params Matcher[]/*!*/ subs){
+Contract.Requires(subs != null);
+Contract.Requires(sub0 != null);
+Contract.Requires(f != null);
+Contract.Requires(expr != null);
arg1 = null;
IFunApp app = MatchFunctionSymbol(expr,f);
if (app != null)
{
- if (!sub0((IExpr!)app.Arguments[0])) { return false; }
+ if (!sub0(cce.NonNull((IExpr/*!*/)app.Arguments[0]))) { return false; }
- arg1 = (IExpr!)app.Arguments[1];
+ arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]);
int i = 2; // Note ***2***
- foreach (Matcher! s in subs)
- {
- if (!s((IExpr!)app.Arguments[i])) { return false; }
+ foreach(Matcher/*!*/ s in subs){
+Contract.Assert(s != null);
+ if (!s(cce.NonNull((IExpr)app.Arguments[i]))) { return false; }
i++;
}
return true;
@@ -255,21 +389,23 @@ namespace Microsoft.AbstractInterpretationFramework else { return false; }
}
- public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, out IExpr arg1, params Matcher[]! subs)
- {
+ public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, out IExpr arg0, out IExpr arg1, params Matcher[]/*!*/ subs){
+Contract.Requires(subs != null);
+Contract.Requires(f != null);
+Contract.Requires(expr != null);
arg0 = null;
arg1 = null;
IFunApp app = MatchFunctionSymbol(expr,f);
if (app != null)
{
- arg0 = (IExpr!)app.Arguments[0];
- arg1 = (IExpr!)app.Arguments[1];
+ arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]);
+ arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]);
int i = 2; // Note ***2***
- foreach (Matcher! s in subs)
- {
- if (!s((IExpr!)app.Arguments[i])) { return false; }
+ foreach(Matcher/*!*/ s in subs){
+Contract.Assert(s != null);
+ if (!s(cce.NonNull((IExpr/*!*/)app.Arguments[i]))) { return false; }
i++;
}
return true;
@@ -278,8 +414,10 @@ namespace Microsoft.AbstractInterpretationFramework }
// Ternary Binding
- public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, out IExpr arg1, out IExpr arg2, params Matcher[]! subs)
- {
+ public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, out IExpr arg0, out IExpr arg1, out IExpr arg2, params Matcher[]/*!*/ subs){
+Contract.Requires(subs != null);
+Contract.Requires(f != null);
+Contract.Requires(expr != null);
arg0 = null;
arg1 = null;
arg2 = null;
@@ -287,14 +425,14 @@ namespace Microsoft.AbstractInterpretationFramework IFunApp app = MatchFunctionSymbol(expr,f);
if (app != null)
{
- arg0 = (IExpr!)app.Arguments[0];
- arg1 = (IExpr!)app.Arguments[1];
- arg2 = (IExpr!)app.Arguments[2];
+ arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]);
+ arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]);
+ arg2 = (IExpr/*!*/)cce.NonNull(app.Arguments[2]);
int i = 3; // Note ***3***
- foreach (Matcher! s in subs)
- {
- if (!s((IExpr!)app.Arguments[i])) { return false; }
+ foreach(Matcher/*!*/ s in subs){
+Contract.Assert(s != null);
+ if (!s(cce.NonNull((IExpr/*!*/)app.Arguments[i]))) { return false; }
i++;
}
return true;
@@ -317,11 +455,25 @@ namespace Microsoft.AbstractInterpretationFramework /// This interface should be implemented by abstract domains, but client
/// expressions need keep track of function symbols.
/// </summary>
+ [ContractClass(typeof(IFunctionSymbolContracts))]
public interface IFunctionSymbol
{
- AIType! AIType { [Rep][ResultNotNewlyAllocated]
+ AIType/*!*/ AIType { [Rep][ResultNotNewlyAllocated]
get; }
}
+ [ContractClassFor(typeof(IFunctionSymbol))]
+ public abstract class IFunctionSymbolContracts:IFunctionSymbol{
+ #region IFunctionSymbol Members
+
+ AIType IFunctionSymbol.AIType {
+ get {
+ Contract.Ensures(Contract.Result<AIType>() != null);
+ throw new NotImplementedException();
+ }
+ }
+
+ #endregion
+ }
/// <summary>
/// The type of the arguments to ExprUtil.Match, a poor man's pattern
@@ -345,31 +497,39 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
public sealed class FunctionType : AIType
{
- /*[Own]*/ private readonly IList/*<Type!>*/! argTypes;
- /*[Own]*/ private readonly AIType! retType;
+ /*[Own]*/ private readonly IList/*<Type!>*//*!*/ argTypes;
+ /*[Own]*/ private readonly AIType/*!*/ retType;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(argTypes != null);
+ Contract.Invariant(retType != null);
+}
- public FunctionType(params AIType[]! types)
- requires types.Length >= 2;
- {
+
+ public FunctionType(params AIType[]/*!*/ types){
+Contract.Requires(types != null);
+ Contract.Requires(types.Length >= 2);
AIType type = types[types.Length-1];
- assume type != null;
+ Contract.Assume(type != null);
this.retType = type;
ArrayList argTypes = new ArrayList();
for (int i = 0; i < types.Length-1; i++)
{
type = types[i];
- assume type != null;
+ Contract.Assume(type != null);
argTypes.Add(types);
}
this.argTypes = ArrayList.ReadOnly(argTypes);
}
- public IList/*<AIType!>*/! Arguments
+ public IList/*<AIType!>*//*!*/ Arguments
{
[Pure][Rep]
get
- ensures result.IsReadOnly;
- {
+ {
+ Contract.Ensures(Contract.Result<IList>() != null);
+ Contract.Ensures(Contract.Result<IList>().IsReadOnly);
return argTypes;
}
}
@@ -379,9 +539,9 @@ namespace Microsoft.AbstractInterpretationFramework get { return argTypes.Count; }
}
- public AIType! ReturnType
+ public AIType/*!*/ ReturnType
{
- get { return retType; }
+ get {Contract.Ensures(Contract.Result<AIType>() != null); return retType; }
}
/* TODO Do we have the invariant that two functions are equal iff they're the same object.
@@ -418,6 +578,8 @@ namespace Microsoft.AbstractInterpretationFramework /// An interface that specifies a queryable object that can answer
/// whether a predicate holds.
/// </summary>
+ ///
+ [ContractClass(typeof(IQueryableContracts))]
public interface IQueryable
{
/// <summary>
@@ -425,14 +587,31 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
/// <param name="pred">The given predicate.</param>
/// <returns>Yes, No, or Maybe.</returns>
- Answer CheckPredicate(IExpr! pred);
+ Answer CheckPredicate(IExpr/*!*/ pred);
/// <summary>
/// A simplified interface for disequalities. One can always
/// implement this by calling CheckPredicate, but it may be
/// more efficient with this method.
/// </summary>
- Answer CheckVariableDisequality(IVariable! var1, IVariable! var2);
+ Answer CheckVariableDisequality(IVariable/*!*/ var1, IVariable/*!*/ var2);
+ }
+ [ContractClassFor(typeof(IQueryable))]
+ public abstract class IQueryableContracts : IQueryable {
+ #region IQueryable Members
+
+ public Answer CheckPredicate(IExpr pred) {
+ Contract.Requires(pred != null);
+ throw new NotImplementedException();
+ }
+
+ public Answer CheckVariableDisequality(IVariable var1, IVariable var2) {
+ Contract.Requires(var1 != null);
+ Contract.Requires(var2 != null);
+ throw new NotImplementedException();
+ }
+
+ #endregion
}
public static class QueryUtil
@@ -453,6 +632,8 @@ namespace Microsoft.AbstractInterpretationFramework //----------------------------- Exceptions -----------------------------
+ public class CheckedException : System.Exception {
+ }
public class TypeError : CheckedException
{
}
|