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/AbsyQuant.cs | |
| parent | 96d9624e9e22dbe9090e0bd7d538cafbf0a16463 (diff) | |
Boogie: Committing changed source files
Diffstat (limited to 'Source/Core/AbsyQuant.cs')
| -rw-r--r-- | Source/Core/AbsyQuant.cs | 836 |
1 files changed, 497 insertions, 339 deletions
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 7515d37d..c30211ca 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -7,17 +7,16 @@ // BoogiePL - AbsyQuant.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;
using Microsoft.Basetypes;
-
+
//---------------------------------------------------------------------
// Quantifiers and general binders
@@ -28,34 +27,77 @@ namespace Microsoft.Boogie Exists,
Lambda
}
+ [ContractClassFor(typeof(BinderExpr))]
+ abstract class BinderExprContracts : BinderExpr {
+ public override BinderKind Kind {
+ get {
+ throw new NotImplementedException();
+ }
+ }
+ public BinderExprContracts():base(null,null,null,null,null){
+ }
+
+ public override Microsoft.AbstractInterpretationFramework.IFunctionSymbol FunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<AI.IFunctionSymbol>() != null);
+ throw new NotImplementedException();
+ }
+ }
- public abstract class BinderExpr : Expr
- {
- public TypeVariableSeq! TypeParameters;
- public VariableSeq! Dummies;
+ public override Type ShallowType {
+ get {
+ throw new NotImplementedException();
+ }
+ }
+
+ public override Microsoft.AbstractInterpretationFramework.IExpr IExpr {
+ get {
+ throw new NotImplementedException();
+ }
+ }
+ }
+ [ContractClass(typeof(BinderExprContracts))]
+ public abstract class BinderExpr : Expr {
+ public TypeVariableSeq/*!*/ TypeParameters;
+ public VariableSeq/*!*/ Dummies;
public QKeyValue Attributes;
- public Expr! Body;
+ public Expr/*!*/ Body;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(TypeParameters != null);
+ Contract.Invariant(Dummies != null);
+ Contract.Invariant(Body != null);
+ }
- public BinderExpr(IToken! tok, TypeVariableSeq! typeParameters,
- VariableSeq! dummies, QKeyValue kv, Expr! body)
- requires dummies.Length + typeParameters.Length > 0;
- {
- base(tok);
+ public BinderExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,
+ VariableSeq/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)
+ : base(tok)//BASEMOVEA
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(typeParameters != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(body != null);
+ Contract.Requires(dummies.Length + typeParameters.Length > 0);
+ //base(tok);
TypeParameters = typeParameters;
Dummies = dummies;
Attributes = kv;
Body = body;
}
- abstract public BinderKind Kind { get; }
+ abstract public BinderKind Kind {
+ get;
+ }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
if (!(obj is BinderExpr) ||
- this.Kind != ((BinderExpr)obj).Kind) return false;
+ this.Kind != ((BinderExpr)obj).Kind)
+ return false;
BinderExpr other = (BinderExpr)obj;
// Note, we consider quantifiers equal modulo the Triggers.
@@ -64,27 +106,26 @@ namespace Microsoft.Boogie && object.Equals(this.Body, other.Body);
}
- [Pure]
- public override int GetHashCode()
- {
+ [Pure]
+ public override int GetHashCode() {
int h = this.Dummies.GetHashCode();
// Note, we consider quantifiers equal modulo the Triggers.
h ^= this.Body.GetHashCode();
- h = h*5 + this.TypeParameters.GetHashCode();
+ h = h * 5 + this.TypeParameters.GetHashCode();
h *= ((int)Kind + 1);
return h;
}
- protected virtual void EmitTypeHint(TokenTextWriter! stream)
- {
+ protected virtual void EmitTypeHint(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
}
- protected virtual void EmitTriggers(TokenTextWriter! stream)
- {
+ protected virtual void EmitTriggers(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
}
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
stream.Write(this, "({0}", Kind.ToString().ToLower());
this.EmitTypeHint(stream);
Type.EmitOptionalTypeParams(stream, TypeParameters);
@@ -96,29 +137,31 @@ namespace Microsoft.Boogie stream.Write(" ");
}
this.EmitTriggers(stream);
-
+
this.Body.Emit(stream);
stream.Write(")");
}
- protected virtual void ResolveTriggers(ResolutionContext! rc)
- {
+ protected virtual void ResolveTriggers(ResolutionContext rc) {
+ Contract.Requires(rc != null);
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
if (rc.TriggerMode) {
rc.Error(this, "quantifiers are not allowed in triggers");
}
int previousTypeBinderState = rc.TypeBinderState;
try {
- foreach (TypeVariable! v in TypeParameters)
+ foreach (TypeVariable/*!*/ v in TypeParameters) {
+ Contract.Assert(v != null);
rc.AddTypeBinder(v);
+ }
rc.PushVarContext();
- foreach (Variable! v in Dummies)
- {
+ foreach (Variable/*!*/ v in Dummies) {
+ Contract.Assert(v != null);
v.Register(rc);
v.Resolve(rc);
}
@@ -128,7 +171,7 @@ namespace Microsoft.Boogie this.ResolveTriggers(rc);
Body.Resolve(rc);
rc.PopVarContext();
-
+
// establish a canonical order of the type parameters
this.TypeParameters = Type.SortTypeParams(TypeParameters, Dummies.ToTypeSeq, null);
@@ -137,79 +180,101 @@ namespace Microsoft.Boogie }
}
- public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
- foreach (Variable! v in Dummies) {
- assert !freeVars[v];
+ public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ //Contract.Requires(freeVars != null);
+ foreach (Variable/*!*/ v in Dummies) {
+ Contract.Assert(v != null);
+ Contract.Assert(!freeVars[v]);
}
Body.ComputeFreeVariables(freeVars);
- foreach (Variable! v in Dummies) {
- foreach (TypeVariable! w in v.TypedIdent.Type.FreeVariables)
+ foreach (Variable/*!*/ v in Dummies) {
+ Contract.Assert(v != null);
+ foreach (TypeVariable/*!*/ w in v.TypedIdent.Type.FreeVariables) {
+ Contract.Assert(w != null);
freeVars.Add(w);
+ }
}
- foreach (Variable! v in Dummies) {
+ foreach (Variable/*!*/ v in Dummies) {
+ Contract.Assert(v != null);
freeVars.Remove(v);
}
- foreach (TypeVariable! v in TypeParameters) {
+ foreach (TypeVariable/*!*/ v in TypeParameters) {
+ Contract.Assert(v != null);
freeVars.Remove(v);
}
}
- protected TypeVariableSeq! GetUnmentionedTypeParameters()
- {
- TypeVariableSeq! dummyParameters = Type.FreeVariablesIn(Dummies.ToTypeSeq);
- TypeVariableSeq! unmentionedParameters = new TypeVariableSeq ();
- foreach (TypeVariable! var in TypeParameters)
+ protected TypeVariableSeq GetUnmentionedTypeParameters() {
+ Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
+ TypeVariableSeq/*!*/ dummyParameters = Type.FreeVariablesIn(Dummies.ToTypeSeq);
+ Contract.Assert(dummyParameters != null);
+ TypeVariableSeq/*!*/ unmentionedParameters = new TypeVariableSeq();
+ foreach (TypeVariable/*!*/ var in TypeParameters) {
+ Contract.Assert(var != null);
if (!dummyParameters.Has(var))
unmentionedParameters.Add(var);
+ }
return unmentionedParameters;
}
-
- public abstract AI.IFunctionSymbol! FunctionSymbol { get; }
-
- internal sealed class AIQuantifier : AI.IFunApp
- {
- internal readonly AIFunctionRep! arg;
- internal AIQuantifier(BinderExpr! realQuantifier, int dummyIndex)
- : this(new AIFunctionRep(realQuantifier, dummyIndex))
- {
+
+ public abstract AI.IFunctionSymbol/*!*/ FunctionSymbol {
+ get;
+ }
+
+ internal sealed class AIQuantifier : AI.IFunApp {
+ internal readonly AIFunctionRep/*!*/ arg;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(arg != null);
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is AIQuantifier)) return false;
-
+
+ internal AIQuantifier(BinderExpr/*!*/ realQuantifier, int dummyIndex)
+ : this(new AIFunctionRep(realQuantifier, dummyIndex)) {
+ Contract.Requires(realQuantifier != null);
+ }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is AIQuantifier))
+ return false;
+
AIQuantifier other = (AIQuantifier)obj;
return object.Equals(this.arg, other.arg);
}
- [Pure]
- public override int GetHashCode()
- {
+ [Pure]
+ public override int GetHashCode() {
return this.arg.GetHashCode();
}
-
- private AIQuantifier(AIFunctionRep! arg)
- {
+
+ private AIQuantifier(AIFunctionRep arg) {
+ Contract.Requires(arg != null);
this.arg = arg;
// base();
}
-
+
[Pure]
- public object DoVisit(AI.ExprVisitor! visitor)
- {
+ public object DoVisit(AI.ExprVisitor visitor) {
+ Contract.Requires(visitor != null);
return visitor.VisitFunApp(this);
}
-
- public AI.IFunctionSymbol! FunctionSymbol { get { return arg.RealQuantifier.FunctionSymbol; } }
-
+
+ public AI.IFunctionSymbol/*!*/ FunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<AI.IFunctionSymbol>() != null);
+ return arg.RealQuantifier.FunctionSymbol;
+ }
+ }
+
private IList/*?*/ argCache = null;
- public IList/*<IExpr!>*/! Arguments
- {
- get
- {
- if (argCache == null)
- {
+ public IList/*<IExpr!>*//*!*/ Arguments {
+
+ get {
+ Contract.Ensures(Contract.Result<IList>() != null);
+
+ if (argCache == null) {
IList a = new ArrayList(1);
a.Add(arg);
argCache = ArrayList.ReadOnly(a);
@@ -217,81 +282,93 @@ namespace Microsoft.Boogie return argCache;
}
}
-
- public AI.IFunApp! CloneWithArguments(IList/*<IExpr!>*/! args)
- {
- assume args.Count == 1;
-
+
+ public AI.IFunApp CloneWithArguments(IList/*<IExpr!>*/ args) {
+ Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
+ Contract.Assume(args.Count == 1);
+
AIFunctionRep rep = args[0] as AIFunctionRep;
if (rep != null)
return new AIQuantifier(rep);
else
throw new System.NotImplementedException();
}
-
+
[Pure]
- public override string! ToString()
- {
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
return string.Format("{0}({1})", FunctionSymbol, arg);
}
}
-
- internal sealed class AIFunctionRep : AI.IFunction
- {
- internal readonly BinderExpr! RealQuantifier;
+
+ internal sealed class AIFunctionRep : AI.IFunction {
+ internal readonly BinderExpr/*!*/ RealQuantifier;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(RealQuantifier != null);
+ }
+
private readonly int dummyIndex;
-
- internal AIFunctionRep(BinderExpr! realQuantifier, int dummyIndex)
- {
+
+ internal AIFunctionRep(BinderExpr realQuantifier, int dummyIndex) {
+ Contract.Requires(realQuantifier != null);
this.RealQuantifier = realQuantifier;
this.dummyIndex = dummyIndex;
- assert realQuantifier.TypeParameters.Length == 0; // PR: don't know how to handle this yet
+ Contract.Assert(realQuantifier.TypeParameters.Length == 0); // PR: don't know how to handle this yet
// base();
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is AIFunctionRep)) return false;
-
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is AIFunctionRep))
+ return false;
+
AIFunctionRep other = (AIFunctionRep)obj;
return object.Equals(this.RealQuantifier, other.RealQuantifier) && this.dummyIndex == other.dummyIndex;
}
- [Pure]
- public override int GetHashCode()
- {
+ [Pure]
+ public override int GetHashCode() {
return this.RealQuantifier.GetHashCode() ^ dummyIndex;
}
-
+
[Pure]
- public object DoVisit(AI.ExprVisitor! visitor)
- {
+ public object DoVisit(AI.ExprVisitor visitor) {
+ Contract.Requires(visitor != null);
return visitor.VisitFunction(this);
}
-
- public AI.IVariable! Param
- {
- get { return (!)RealQuantifier.Dummies[dummyIndex]; }
+
+ public AI.IVariable/*!*/ Param {
+
+ get {
+ Contract.Ensures(Contract.Result<AI.IVariable>() != null);
+ return cce.NonNull(RealQuantifier.Dummies[dummyIndex]);
+ }
+ }
+ public AI.AIType/*!*/ ParamType {
+ get {
+ Contract.Ensures(Contract.Result<AI.AIType>() != null);
+ throw new System.NotImplementedException();
+ }
}
- public AI.AIType! ParamType { get { throw new System.NotImplementedException(); } }
-
+
// We lazily convert to 1 dummy per quantifier representation for AIFramework
private AI.IExpr/*?*/ bodyCache = null;
- public AI.IExpr! Body
- {
- get
- {
- if (bodyCache == null)
- {
+ public AI.IExpr/*!*/ Body {
+ get {
+ Contract.Ensures(Contract.Result<AI.IExpr>() != null);
+
+ if (bodyCache == null) {
int dummyi = dummyIndex;
int dummylen = RealQuantifier.Dummies.Length;
- assume dummylen > dummyi;
-
+ Contract.Assume(dummylen > dummyi);
+
// return the actual body if there are no more dummies
if (dummyi + 1 == dummylen)
bodyCache = RealQuantifier.Body.IExpr;
- else
- {
+ else {
AIQuantifier innerquant = new AIQuantifier(RealQuantifier, dummyi + 1);
bodyCache = innerquant;
}
@@ -299,76 +376,83 @@ namespace Microsoft.Boogie return bodyCache;
}
}
- public AI.IFunction! CloneWithBody(AI.IExpr! body)
- {
+ public AI.IFunction CloneWithBody(AI.IExpr body) {
+ Contract.Requires(body != null);
+ Contract.Ensures(Contract.Result<AI.IFunction>() != null);
BinderExpr realquant;
-
+
AIQuantifier innerquant = body as AIQuantifier;
- if (innerquant == null)
- {
+ if (innerquant == null) {
// new quantifier body, clone the real quantifier
realquant = (BinderExpr)RealQuantifier.Clone();
realquant.Body = BoogieFactory.IExpr2Expr(body);
- }
- else
- {
- if (innerquant.arg.dummyIndex > 0)
- {
+ } else {
+ if (innerquant.arg.dummyIndex > 0) {
realquant = innerquant.arg.RealQuantifier;
- }
- else
- {
+ } else {
realquant = (QuantifierExpr)RealQuantifier.Clone();
- VariableSeq! newdummies = new VariableSeq();
+ VariableSeq/*!*/ newdummies = new VariableSeq();
newdummies.Add(Param);
newdummies.AddRange(innerquant.arg.RealQuantifier.Dummies);
realquant.Dummies = newdummies;
realquant.Body = innerquant.arg.RealQuantifier.Body;
}
}
-
+
return new AIFunctionRep(realquant, dummyIndex);
}
[Pure]
- public override string! ToString()
- {
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
return string.Format("\\{0} :: {1}", Param, Body);
}
}
-
+
private AI.IExpr aiexprCache = null;
- public override AI.IExpr! IExpr {
+ public override AI.IExpr/*!*/ IExpr {
get {
+ Contract.Ensures(Contract.Result<AI.IExpr>() != null);
+
if (TypeParameters.Length > 0)
return new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "anon", Type.Bool));
- if (aiexprCache == null)
- {
+ if (aiexprCache == null) {
aiexprCache = new AIQuantifier(this, 0);
}
return aiexprCache;
}
- }
+ }
}
public class QKeyValue : Absy {
- public readonly string! Key;
- public readonly List<object!>! Params; // each element is either a string or an Expr
+ public readonly string/*!*/ Key;
+ public readonly List<object/*!*/>/*!*/ Params; // each element is either a string or an Expr
public QKeyValue Next;
-
- public QKeyValue(IToken! tok, string! key, [Captured] List<object!>! parameters, QKeyValue next)
- {
- base(tok);
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Key != null);
+ Contract.Invariant(cce.NonNullElements(Params));
+ }
+
+
+ public QKeyValue(IToken tok, string key, [Captured] List<object/*!*/>/*!*/ parameters, QKeyValue next)
+ : base(tok) {//BASEMOVEA
+ Contract.Requires(key != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(cce.NonNullElements(parameters));
+ //:base(tok);
Key = key;
Params = parameters;
Next = next;
}
-
- public void Emit(TokenTextWriter! stream) {
+
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
stream.Write("{:");
stream.Write(Key);
string sep = " ";
foreach (object p in Params) {
- stream.Write(sep); sep = ", ";
+ stream.Write(sep);
+ sep = ", ";
if (p is string) {
stream.Write("\"");
stream.Write((string)p);
@@ -379,32 +463,35 @@ namespace Microsoft.Boogie }
stream.Write("}");
}
-
- public override void Resolve(ResolutionContext! rc) {
+
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
foreach (object p in Params) {
if (p is Expr) {
((Expr)p).Resolve(rc);
}
}
}
-
- public override void Typecheck(TypecheckingContext! tc) {
+
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
foreach (object p in Params) {
if (p is Expr) {
((Expr)p).Typecheck(tc);
}
}
}
- public void AddLast(QKeyValue! other){
+ public void AddLast(QKeyValue other) {
+ Contract.Requires(other != null);
QKeyValue current = this;
- while(current.Next!=null){
+ while (current.Next != null) {
current = current.Next;
}
current.Next = other;
}
// Look for {:name string} in list of attributes.
- public static string? FindStringAttribute(QKeyValue? kv, string! name)
- {
+ public static string FindStringAttribute(QKeyValue kv, string name) {
+ Contract.Requires(name != null);
for (; kv != null; kv = kv.Next) {
if (kv.Key == name) {
if (kv.Params.Count == 1 && kv.Params[0] is string) {
@@ -415,8 +502,8 @@ namespace Microsoft.Boogie return null;
}
// Look for {:name expr} in list of attributes.
- public static Expr? FindExprAttribute(QKeyValue? kv, string! name)
- {
+ public static Expr FindExprAttribute(QKeyValue kv, string name) {
+ Contract.Requires(name != null);
for (; kv != null; kv = kv.Next) {
if (kv.Key == name) {
if (kv.Params.Count == 1 && kv.Params[0] is Expr) {
@@ -427,8 +514,8 @@ namespace Microsoft.Boogie return null;
}
// Return 'true' if {:name true} or {:name} is an attribute in 'kv'
- public static bool FindBoolAttribute(QKeyValue? kv, string! name)
- {
+ public static bool FindBoolAttribute(QKeyValue kv, string name) {
+ Contract.Requires(name != null);
for (; kv != null; kv = kv.Next) {
if (kv.Key == name) {
return kv.Params.Count == 0 ||
@@ -438,63 +525,76 @@ namespace Microsoft.Boogie return false;
}
- public static int FindIntAttribute(QKeyValue? kv, string! name, int defl)
- {
- Expr? e = FindExprAttribute(kv, name);
- LiteralExpr? l = e as LiteralExpr;
+ public static int FindIntAttribute(QKeyValue kv, string name, int defl) {
+ Contract.Requires(name != null);
+ Expr e = FindExprAttribute(kv, name);
+ LiteralExpr l = e as LiteralExpr;
if (l != null && l.isBigNum)
return l.asBigNum.ToIntSafe;
return defl;
}
}
-
+
public class Trigger : Absy {
public readonly bool Pos;
[Rep]
- public ExprSeq! Tr;
- invariant 1 <= Tr.Length;
- invariant !Pos ==> Tr.Length == 1;
+ public ExprSeq/*!*/ Tr;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Tr != null);
+ Contract.Invariant(1 <= Tr.Length);
+ Contract.Invariant(Pos || Tr.Length == 1);
+ }
+
+
public Trigger Next;
-
- public Trigger(IToken! tok, bool pos, ExprSeq! tr)
- requires 1 <= tr.Length;
- requires !pos ==> tr.Length == 1;
- {
- this(tok, pos, tr, null);
- }
-
- public Trigger(IToken! tok, bool pos, ExprSeq! tr, Trigger next)
- : base(tok)
- requires 1 <= tr.Length;
- requires !pos ==> tr.Length == 1;
- {
+
+ public Trigger(IToken tok, bool pos, ExprSeq tr)
+ : this(tok, pos, tr, null) {//BASEMOVEA
+ Contract.Requires(tr != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(1 <= tr.Length);
+ Contract.Requires(pos || tr.Length == 1);
+ //:this(tok, pos, tr, null);
+ }
+
+ public Trigger(IToken/*!*/ tok, bool pos, ExprSeq/*!*/ tr, Trigger next)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(tr != null);
+ Contract.Requires(1 <= tr.Length);
+ Contract.Requires(pos || tr.Length == 1);
this.Pos = pos;
this.Tr = tr;
this.Next = next;
// base(tok);
}
- public void Emit(TokenTextWriter! stream) {
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
stream.SetToken(this);
- assert this.Tr.Length >= 1;
- string! sep = Pos ? "{ " : "{:nopats ";
- foreach (Expr! e in this.Tr) {
+ Contract.Assert(this.Tr.Length >= 1);
+ string/*!*/ sep = Pos ? "{ " : "{:nopats ";
+ foreach (Expr/*!*/ e in this.Tr) {
+ Contract.Assert(e != null);
stream.Write(sep);
sep = ", ";
e.Emit(stream);
}
stream.Write(" }");
}
- public override void Resolve(ResolutionContext! rc) {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.TriggerMode = true;
- foreach (Expr! e in this.Tr) {
+ foreach (Expr/*!*/ e in this.Tr) {
+ Contract.Assert(e != null);
e.Resolve(rc);
// just a variable by itself is not allowed
if (e is IdentifierExpr) {
rc.Error(e, "a matching pattern must be more than just a variable by itself: {0}", e);
}
-
+
// the free-variable check is performed in the surrounding quantifier expression (because that's
// where the bound variables are known)
}
@@ -504,134 +604,171 @@ namespace Microsoft.Boogie /// <summary>
/// Add to "freeVars" the free variables in the triggering expressions.
/// </summary>
- public void ComputeFreeVariables(Set /*Variable*/! freeVars) {
- foreach (Expr! e in this.Tr) {
+ public void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ Contract.Requires(freeVars != null);
+ foreach (Expr/*!*/ e in this.Tr) {
+ Contract.Assert(e != null);
e.ComputeFreeVariables(freeVars);
}
}
- public override void Typecheck(TypecheckingContext! tc) {
- foreach (Expr! e in this.Tr) {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ foreach (Expr/*!*/ e in this.Tr) {
+ Contract.Assert(e != null);
e.Typecheck(tc);
}
}
- public void AddLast(Trigger other){
- Trigger current = this;
- while(current.Next!=null){
- current = current.Next;
- }
- current.Next = other;
+ public void AddLast(Trigger other) {
+ Trigger current = this;
+ while (current.Next != null) {
+ current = current.Next;
+ }
+ current.Next = other;
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitTrigger(this);
}
}
+ public class ForallExpr : QuantifierExpr {
+ public ForallExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParams,
+ VariableSeq/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)
+ : base(tok, typeParams, dummies, kv, triggers, body) {//BASEMOVEA
+ Contract.Requires(tok != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(body != null);
+ Contract.Requires(dummies.Length + typeParams.Length > 0);
+ //:base(tok, typeParams, dummies, kv, triggers, body); // here for aesthetic reasons
+ }
+ public ForallExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)
+ : base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {//BASEMOVEA
+ Contract.Requires(body != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(dummies.Length > 0);
+ //:base(tok, new TypeVariableSeq(), dummies, null, triggers, body); // here for aesthetic reasons
+ }
+ public ForallExpr(IToken tok, VariableSeq dummies, Expr body)
+ : base(tok, new TypeVariableSeq(), dummies, null, null, body) {//BASEMOVEA
+ Contract.Requires(body != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(dummies.Length > 0);
+ //:base(tok, new TypeVariableSeq(), dummies, null, null, body); // here for aesthetic reasons
+ }
+ public ForallExpr(IToken tok, TypeVariableSeq typeParams, VariableSeq dummies, Expr body)
+ : base(tok, typeParams, dummies, null, null, body) {//BASEMOVEA
+ Contract.Requires(body != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(dummies.Length + typeParams.Length > 0);
+ //:base(tok, typeParams, dummies, null, null, body); // here for aesthetic reasons
+ }
+ public override AI.IFunctionSymbol/*!*/ FunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<AI.IFunctionSymbol>() != null);
- public class ForallExpr : QuantifierExpr
- {
- public ForallExpr(IToken! tok, TypeVariableSeq! typeParams,
- VariableSeq! dummies, QKeyValue kv, Trigger triggers, Expr! body)
- requires dummies.Length + typeParams.Length > 0;
- {
- base(tok, typeParams, dummies, kv, triggers, body); // here for aesthetic reasons
- }
- public ForallExpr(IToken! tok, VariableSeq! dummies, Trigger triggers, Expr! body)
- requires dummies.Length > 0;
- {
- base(tok, new TypeVariableSeq(), dummies, null, triggers, body); // here for aesthetic reasons
- }
- public ForallExpr(IToken! tok, VariableSeq! dummies, Expr! body)
- requires dummies.Length > 0;
- {
- base(tok, new TypeVariableSeq(), dummies, null, null, body); // here for aesthetic reasons
- }
- public ForallExpr(IToken! tok, TypeVariableSeq! typeParams, VariableSeq! dummies, Expr! body)
- requires dummies.Length + typeParams.Length > 0;
- {
- base(tok, typeParams, dummies, null, null, body); // here for aesthetic reasons
- }
- public override AI.IFunctionSymbol! FunctionSymbol
- {
- get {
return AI.Prop.Forall;
}
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitForallExpr(this);
}
- public override BinderKind Kind { get { return BinderKind.Forall; } }
+ public override BinderKind Kind {
+ get {
+ return BinderKind.Forall;
+ }
+ }
}
-
- public class ExistsExpr : QuantifierExpr
- {
- public ExistsExpr(IToken! tok, TypeVariableSeq! typeParams, VariableSeq! dummies,
- QKeyValue kv, Trigger triggers, Expr! body)
- requires dummies.Length + typeParams.Length > 0;
- {
- base(tok, typeParams, dummies, kv, triggers, body); // here for aesthetic reasons
- }
- public ExistsExpr(IToken! tok, VariableSeq! dummies, Trigger triggers, Expr! body)
- requires dummies.Length > 0;
- {
- base(tok, new TypeVariableSeq (), dummies, null, triggers, body); // here for aesthetic reasons
- }
- public ExistsExpr(IToken! tok, VariableSeq! dummies, Expr! body)
- requires dummies.Length > 0;
- {
- base(tok, new TypeVariableSeq(), dummies, null, null, body); // here for aesthetic reasons
- }
- public override AI.IFunctionSymbol! FunctionSymbol
- {
+ public class ExistsExpr : QuantifierExpr {
+ public ExistsExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ dummies,
+ QKeyValue kv, Trigger triggers, Expr/*!*/ body)
+ : base(tok, typeParams, dummies, kv, triggers, body) {//BASEMOVEA
+ Contract.Requires(tok != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(body != null);
+ Contract.Requires(dummies.Length + typeParams.Length > 0);
+ //:base(tok, typeParams, dummies, kv, triggers, body); // here for aesthetic reasons
+ }
+ public ExistsExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)
+ : base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {//BASEMOVEA
+ Contract.Requires(body != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(dummies.Length > 0);
+ //:base(tok, new TypeVariableSeq(), dummies, null, triggers, body); // here for aesthetic reasons
+ }
+ public ExistsExpr(IToken tok, VariableSeq dummies, Expr body)
+ : base(tok, new TypeVariableSeq(), dummies, null, null, body) {//BASEMOVEA
+ Contract.Requires(body != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(dummies.Length > 0);
+ //:base(tok, new TypeVariableSeq(), dummies, null, null, body); // here for aesthetic reasons
+ }
+ public override AI.IFunctionSymbol/*!*/ FunctionSymbol {
get {
+ Contract.Ensures(Contract.Result<AI.IFunctionSymbol>() != null);
+
return AI.Prop.Exists;
}
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitExistsExpr(this);
}
- public override BinderKind Kind { get { return BinderKind.Exists; } }
+ public override BinderKind Kind {
+ get {
+ return BinderKind.Exists;
+ }
+ }
}
-
-
- public abstract class QuantifierExpr : BinderExpr
- {
+ public abstract class QuantifierExpr : BinderExpr {
public Trigger Triggers;
static int SkolemIds = 0;
- public static int GetNextSkolemId()
- {
+ public static int GetNextSkolemId() {
SkolemIds++;
return SkolemIds;
}
-
+
public readonly int SkolemId;
-
- public QuantifierExpr(IToken! tok, TypeVariableSeq! typeParameters,
- VariableSeq! dummies, QKeyValue kv, Trigger triggers, Expr! body)
- requires dummies.Length + typeParameters.Length > 0;
- {
- base(tok, typeParameters, dummies, kv, body);
-
- assert (this is ForallExpr) || (this is ExistsExpr);
-
+
+ public QuantifierExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,
+ VariableSeq/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)
+ : base(tok, typeParameters, dummies, kv, body) {//BASEMOVEA
+ Contract.Requires(tok != null);
+ Contract.Requires(typeParameters != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(body != null);
+ Contract.Requires(dummies.Length + typeParameters.Length > 0);
+ //:base(tok, typeParameters, dummies, kv, body);
+
+ Contract.Assert((this is ForallExpr) || (this is ExistsExpr));
+
Triggers = triggers;
SkolemId = SkolemIds++;
}
- protected override void EmitTriggers(TokenTextWriter! stream)
- {
+ protected override void EmitTriggers(TokenTextWriter stream) {
+ //Contract.Requires(stream != null);
for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
tr.Emit(stream);
stream.Write(" ");
@@ -640,8 +777,7 @@ namespace Microsoft.Boogie // if the user says ( forall x :: forall y :: { f(x,y) } ... ) we transform it to
// (forall x, y :: { f(x,y) } ... ) otherwise the prover ignores the trigger
- private void MergeAdjecentQuantifier()
- {
+ private void MergeAdjecentQuantifier() {
QuantifierExpr qbody = Body as QuantifierExpr;
if (!(qbody != null && (qbody is ForallExpr) == (this is ForallExpr) && Triggers == null)) {
return;
@@ -668,18 +804,23 @@ namespace Microsoft.Boogie }
#region never triggers
- private class NeverTriggerCollector : StandardVisitor
- {
- QuantifierExpr! parent;
- public NeverTriggerCollector(QuantifierExpr! p)
- {
+ private class NeverTriggerCollector : StandardVisitor {
+ QuantifierExpr/*!*/ parent;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(parent != null);
+ }
+
+ public NeverTriggerCollector(QuantifierExpr p) {
+ Contract.Requires(p != null);
parent = p;
}
- public override Expr! VisitNAryExpr(NAryExpr! node)
- {
+ public override Expr VisitNAryExpr(NAryExpr node) {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
FunctionCall fn = node.Fun as FunctionCall;
- if (fn != null && ((!)fn.Func).NeverTrigger) {
+ if (fn != null && cce.NonNull(fn.Func).NeverTrigger) {
parent.Triggers = new Trigger(fn.Func.tok, false, new ExprSeq(node), parent.Triggers);
}
return base.VisitNAryExpr(node);
@@ -687,15 +828,16 @@ namespace Microsoft.Boogie }
private bool neverTriggerApplied;
- private void ApplyNeverTriggers()
- {
+ private void ApplyNeverTriggers() {
if (neverTriggerApplied) {
return;
}
neverTriggerApplied = true;
for (Trigger t = Triggers; t != null; t = t.Next) {
- if (t.Pos) { return; }
+ if (t.Pos) {
+ return;
+ }
}
NeverTriggerCollector visitor = new NeverTriggerCollector(this);
@@ -703,8 +845,8 @@ namespace Microsoft.Boogie }
#endregion
- protected override void ResolveTriggers(ResolutionContext! rc)
- {
+ protected override void ResolveTriggers(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
int prevErrorCount = rc.ErrorCount;
tr.Resolve(rc);
@@ -713,7 +855,8 @@ namespace Microsoft.Boogie if (tr.Pos) {
Set /*Variable*/ freeVars = new Set /*Variable*/ ();
tr.ComputeFreeVariables(freeVars);
- foreach (Variable! v in Dummies) {
+ foreach (Variable/*!*/ v in Dummies) {
+ Contract.Assert(v != null);
if (!freeVars[v]) {
rc.Error(tr, "trigger must mention all quantified variables, but does not mention: {0}", v);
}
@@ -723,10 +866,10 @@ namespace Microsoft.Boogie }
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
int oldErrorCount = rc.ErrorCount;
-
+
this.MergeAdjecentQuantifier();
base.Resolve(rc);
@@ -737,8 +880,8 @@ namespace Microsoft.Boogie }
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
kv.Typecheck(tc);
}
@@ -746,9 +889,8 @@ namespace Microsoft.Boogie tr.Typecheck(tc);
}
Body.Typecheck(tc);
- assert Body.Type != null; // follows from postcondition of Expr.Typecheck
- if (!Body.Type.Unify(Type.Bool))
- {
+ Contract.Assert(Body.Type != null); // follows from postcondition of Expr.Typecheck
+ if (!Body.Type.Unify(Type.Bool)) {
tc.Error(this, "quantifier body must be of type bool");
}
this.Type = Type.Bool;
@@ -756,7 +898,8 @@ namespace Microsoft.Boogie // Check that type parameters occur in the types of the
// dummies, or otherwise in the triggers. This can only be
// done after typechecking
- TypeVariableSeq! unmentionedParameters = GetUnmentionedTypeParameters();
+ TypeVariableSeq/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();
+ Contract.Assert(unmentionedParameters != null);
if (unmentionedParameters.Length > 0) {
// all the type parameters that do not occur in dummy types
@@ -767,7 +910,8 @@ namespace Microsoft.Boogie if (tr.Pos) {
Set /*Variable*/ freeVars = new Set /*Variable*/ ();
tr.ComputeFreeVariables(freeVars);
- foreach (TypeVariable! v in unmentionedParameters) {
+ foreach (TypeVariable/*!*/ v in unmentionedParameters) {
+ Contract.Assert(v != null);
if (!freeVars[v])
tc.Error(tr,
"trigger does not mention {0}, which does not occur in variables types either",
@@ -777,41 +921,51 @@ namespace Microsoft.Boogie }
}
}
- public override Type! ShallowType {
+ public override Type/*!*/ ShallowType {
get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
return Type.Bool;
}
}
-
+
}
- public class LambdaExpr : BinderExpr
- {
- public LambdaExpr(IToken! tok, TypeVariableSeq! typeParameters,
- VariableSeq! dummies, QKeyValue kv, Expr! body)
- requires dummies.Length + typeParameters.Length > 0;
- {
- base(tok, typeParameters, dummies, kv, body);
+ public class LambdaExpr : BinderExpr {
+ public LambdaExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,
+ VariableSeq/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)
+ : base(tok, typeParameters, dummies, kv, body) {//BASEMOVEA
+ Contract.Requires(tok != null);
+ Contract.Requires(typeParameters != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(body != null);
+ Contract.Requires(dummies.Length + typeParameters.Length > 0);
+ //:base(tok, typeParameters, dummies, kv, body);
}
- public override BinderKind Kind { get { return BinderKind.Lambda; } }
+ public override BinderKind Kind {
+ get {
+ return BinderKind.Lambda;
+ }
+ }
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
base.Resolve(rc);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
kv.Typecheck(tc);
}
Body.Typecheck(tc);
- assert Body.Type != null; // follows from postcondition of Expr.Typecheck
+ Contract.Assert(Body.Type != null); // follows from postcondition of Expr.Typecheck
- TypeSeq! argTypes = new TypeSeq();
- foreach (Variable! v in Dummies) {
+ TypeSeq/*!*/ argTypes = new TypeSeq();
+ foreach (Variable/*!*/ v in Dummies) {
+ Contract.Assert(v != null);
argTypes.Add(v.TypedIdent.Type);
}
this.Type = new MapType(this.tok, this.TypeParameters, argTypes, Body.Type);
@@ -819,19 +973,23 @@ namespace Microsoft.Boogie // Check that type parameters occur in the types of the
// dummies, or otherwise in the triggers. This can only be
// done after typechecking
- TypeVariableSeq! unmentionedParameters = GetUnmentionedTypeParameters();
+ TypeVariableSeq/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();
+ Contract.Assert(unmentionedParameters != null);
if (unmentionedParameters.Length > 0) {
tc.Error(this, "the type variable {0} does not occur in types of the lambda parameters", unmentionedParameters[0]);
}
}
- private Type? mapType;
- public override Type! ShallowType {
+ private Type mapType;
+ public override Type/*!*/ ShallowType {
get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
if (mapType == null) {
- TypeSeq! argTypes = new TypeSeq();
- foreach (Variable! v in Dummies) {
+ TypeSeq/*!*/ argTypes = new TypeSeq();
+ foreach (Variable/*!*/ v in Dummies) {
+ Contract.Assert(v != null);
argTypes.Add(v.TypedIdent.Type);
}
mapType = new MapType(this.tok, this.TypeParameters, argTypes, Body.ShallowType);
@@ -840,21 +998,21 @@ namespace Microsoft.Boogie return mapType;
}
}
-
- public override AI.IFunctionSymbol! FunctionSymbol
- {
+
+ public override AI.IFunctionSymbol/*!*/ FunctionSymbol {
+
get {
+ Contract.Ensures(Contract.Result<AI.IFunctionSymbol>() != null);
+
return AI.Prop.Lambda;
}
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitLambdaExpr(this);
}
}
-
-
-}
-
+}
\ No newline at end of file |