//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Text;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Numerics;
using Microsoft.Boogie;
namespace Microsoft.Dafny {
public class Program {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Name != null);
Contract.Invariant(DefaultModule != null);
}
public readonly string Name;
public List/*!*/ Modules; // filled in during resolution.
// Resolution essentially flattens the module hierarchy, for
// purposes of translation and compilation.
public List CompileModules; // filled in during resolution.
// Contains the definitions to be used for compilation.
public readonly ModuleDecl DefaultModule;
public readonly ModuleDefinition DefaultModuleDef;
public readonly BuiltIns BuiltIns;
public readonly List TranslationTasks;
public Program(string name, [Captured] ModuleDecl module, [Captured] BuiltIns builtIns) {
Contract.Requires(name != null);
Contract.Requires(module != null);
Contract.Requires(module is LiteralModuleDecl);
Name = name;
DefaultModule = module;
DefaultModuleDef = (DefaultModuleDecl)((LiteralModuleDecl)module).ModuleDef;
BuiltIns = builtIns;
Modules = new List();
CompileModules = new List();
TranslationTasks = new List();
}
}
public class BuiltIns
{
public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, true);
Dictionary arrayTypeDecls = new Dictionary();
public readonly ClassDecl ObjectDecl;
public BuiltIns() {
// create class 'object'
ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List(), new List(), null);
SystemModule.TopLevelDecls.Add(ObjectDecl);
// add one-dimensional arrays, since they may arise during type checking
UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true);
}
public UserDefinedType ArrayType(int dims, Type arg) {
return ArrayType(Token.NoToken, dims, arg, false);
}
public UserDefinedType ArrayType(IToken tok, int dims, Type arg, bool allowCreationOfNewClass) {
Contract.Requires(tok != null);
Contract.Requires(1 <= dims);
Contract.Requires(arg != null);
Contract.Ensures(Contract.Result() != null);
List typeArgs = new List();
typeArgs.Add(arg);
UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null);
if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {
ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);
for (int d = 0; d < dims; d++) {
string name = dims == 1 ? "Length" : "Length" + d;
string compiledName = dims == 1 ? "Length" : "GetLength(" + d + ")";
Field len = new SpecialField(Token.NoToken, name, compiledName, "new BigInteger(", ")", false, false, Type.Int, null);
len.EnclosingClass = arrayClass; // resolve here
arrayClass.Members.Add(len);
}
arrayTypeDecls.Add(dims, arrayClass);
SystemModule.TopLevelDecls.Add(arrayClass);
}
udt.ResolvedClass = arrayTypeDecls[dims];
return udt;
}
public static string ArrayClassName(int dims) {
Contract.Requires(1 <= dims);
if (dims == 1) {
return "array";
} else {
return "array" + dims;
}
}
}
public class Attributes {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Name != null);
Contract.Invariant(cce.NonNullElements(Args));
}
public readonly string Name;
/*Frozen*/
public readonly List/*!*/ Args;
public readonly Attributes Prev;
public Attributes(string name, [Captured] List/*!*/ args, Attributes prev) {
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(args));
Name = name;
Args = args;
Prev = prev;
}
public static bool Contains(Attributes attrs, string nm) {
Contract.Requires(nm != null);
for (; attrs != null; attrs = attrs.Prev) {
if (attrs.Name == nm) {
return true;
}
}
return false;
}
///
/// Returns true if "nm" is a specified attribute. If it is, then:
/// - if the attribute is {:nm true}, then value==true
/// - if the attribute is {:nm false}, then value==false
/// - if the attribute is anything else, then value returns as whatever it was passed in as.
///
public static bool ContainsBool(Attributes attrs, string nm, ref bool value) {
Contract.Requires(nm != null);
for (; attrs != null; attrs = attrs.Prev) {
if (attrs.Name == nm) {
if (attrs.Args.Count == 1) {
var arg = attrs.Args[0].E as LiteralExpr;
if (arg != null && arg.Value is bool) {
value = (bool)arg.Value;
}
}
return true;
}
}
return false;
}
public class Argument
{
public readonly IToken Tok;
public readonly string S;
public readonly Expression E;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Tok != null);
Contract.Invariant((S == null) != (E == null));
}
public Argument(IToken tok, string s) {
Contract.Requires(tok != null);
Contract.Requires(s != null);
Tok = tok;
S = s;
}
public Argument(IToken tok, Expression e) {
Contract.Requires(tok != null);
Contract.Requires(e != null);
Tok = tok;
E = e;
}
}
}
// ------------------------------------------------------------------------------------------------------
public abstract class Type {
public static readonly BoolType Bool = new BoolType();
public static readonly IntType Int = new IntType();
///
/// Used in error situations in order to reduce further error messages.
///
//[Pure(false)]
public static Type Flexible {
get {
Contract.Ensures(Contract.Result() != null);
return new InferredTypeProxy();
}
}
[Pure]
public abstract string TypeName(ModuleDefinition/*?*/ context);
[Pure]
public override string ToString() {
return TypeName(null);
}
///
/// Return the most constrained version of "this".
///
///
public Type Normalize() {
Contract.Ensures(Contract.Result() != null);
Type type = this;
while (true) {
TypeProxy pt = type as TypeProxy;
if (pt != null && pt.T != null) {
type = pt.T;
} else {
return type;
}
}
}
public bool IsSubrangeType {
get { return this is NatType; }
}
public bool IsRefType {
get {
if (this is ObjectType) {
return true;
} else {
UserDefinedType udt = this as UserDefinedType;
return udt != null && udt.ResolvedParam == null && udt.ResolvedClass is ClassDecl;
}
}
}
public bool IsArrayType {
get {
return AsArrayType != null;
}
}
public ArrayClassDecl/*?*/ AsArrayType {
get {
UserDefinedType udt = UserDefinedType.DenotesClass(this);
return udt == null ? null : udt.ResolvedClass as ArrayClassDecl;
}
}
public bool IsDatatype {
get {
return AsDatatype != null;
}
}
public DatatypeDecl AsDatatype {
get {
UserDefinedType udt = this as UserDefinedType;
if (udt == null) {
return null;
} else {
return udt.ResolvedClass as DatatypeDecl;
}
}
}
public bool IsIndDatatype {
get {
return AsIndDatatype != null;
}
}
public IndDatatypeDecl AsIndDatatype {
get {
UserDefinedType udt = this as UserDefinedType;
if (udt == null) {
return null;
} else {
return udt.ResolvedClass as IndDatatypeDecl;
}
}
}
public bool IsCoDatatype {
get {
return AsCoDatatype != null;
}
}
public CoDatatypeDecl AsCoDatatype {
get {
UserDefinedType udt = this as UserDefinedType;
if (udt == null) {
return null;
} else {
return udt.ResolvedClass as CoDatatypeDecl;
}
}
}
public bool InvolvesCoDatatype {
get {
return IsCoDatatype; // TODO: should really check structure of the type recursively
}
}
public bool IsTypeParameter {
get {
return AsTypeParameter != null;
}
}
public TypeParameter AsTypeParameter {
get {
UserDefinedType ct = this as UserDefinedType;
return ct == null ? null : ct.ResolvedParam;
}
}
public virtual bool SupportsEquality {
get {
return true;
}
}
}
///
/// A NonProxy type is a fully constrained type. It may contain members.
///
public abstract class NonProxyType : Type
{
}
public abstract class BasicType : NonProxyType
{
}
public class BoolType : BasicType {
[Pure]
public override string TypeName(ModuleDefinition context) {
return "bool";
}
}
public class IntType : BasicType {
[Pure]
public override string TypeName(ModuleDefinition context) {
return "int";
}
}
public class NatType : IntType
{
[Pure]
public override string TypeName(ModuleDefinition context) {
return "nat";
}
}
public class ObjectType : BasicType
{
[Pure]
public override string TypeName(ModuleDefinition context) {
return "object";
}
}
public abstract class CollectionType : NonProxyType
{
public readonly Type Arg; // denotes the Domain type for a Map
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Arg != null);
}
public CollectionType(Type arg) {
Contract.Requires(arg != null);
this.Arg = arg;
}
public override bool SupportsEquality {
get {
return Arg.SupportsEquality;
}
}
}
public class SetType : CollectionType {
public SetType(Type arg) : base(arg) {
Contract.Requires(arg != null);
}
[Pure]
public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result() != null);
Contract.Assume(cce.IsPeerConsistent(Arg));
return "set<" + base.Arg.TypeName(context) + ">";
}
}
public class MultiSetType : CollectionType
{
public MultiSetType(Type arg) : base(arg) {
Contract.Requires(arg != null);
}
[Pure]
public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result() != null);
Contract.Assume(cce.IsPeerConsistent(Arg));
return "multiset<" + base.Arg.TypeName(context) + ">";
}
}
public class SeqType : CollectionType {
public SeqType(Type arg) : base(arg) {
Contract.Requires(arg != null);
}
[Pure]
public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result() != null);
Contract.Assume(cce.IsPeerConsistent(Arg));
return "seq<" + base.Arg.TypeName(context) + ">";
}
}
public class MapType : CollectionType
{
public Type Range;
public MapType(Type domain, Type range) : base(domain) {
Contract.Requires(domain != null && range != null);
Range = range;
}
public Type Domain {
get { return Arg; }
}
[Pure]
public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result() != null);
Contract.Assume(cce.IsPeerConsistent(Domain));
Contract.Assume(cce.IsPeerConsistent(Range));
return "map<" + Domain.TypeName(context) + ", " + Range.TypeName(context) + ">";
}
}
public class UserDefinedType : NonProxyType
{
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(tok != null);
Contract.Invariant(Name != null);
Contract.Invariant(cce.NonNullElements(TypeArgs));
Contract.Invariant(cce.NonNullElements(Path));
}
public readonly List Path; // may be null
public readonly IToken tok; // token of the Name
public readonly string Name;
[Rep]
public readonly List/*!*/ TypeArgs;
public string FullName {
get {
if (ResolvedClass != null && !ResolvedClass.Module.IsDefaultModule) {
return ResolvedClass.Module.Name + "." + Name;
} else {
return Name;
}
}
}
string compileName;
public string CompileName {
get {
if (compileName == null) {
compileName = NonglobalVariable.CompilerizeName(Name);
}
return compileName;
}
}
public string FullCompileName {
get {
if (ResolvedClass != null && !ResolvedClass.Module.IsDefaultModule) {
return ResolvedClass.Module.CompileName + "." + CompileName;
} else {
return CompileName;
}
}
}
public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype/iterator and TypeArgs match the type parameters of that class/datatype/iterator
public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list
public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List/*!*/ typeArgs, List moduleName) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(moduleName == null || cce.NonNullElements(moduleName));
if (moduleName != null) this.Path = moduleName;
else this.Path = new List();
this.tok = tok;
this.Name = name;
this.TypeArgs = typeArgs;
}
///
/// This constructor constructs a resolved class/datatype/iterator type
///
public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, TopLevelDecl/*!*/ cd, [Captured] List/*!*/ typeArgs) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cd != null);
Contract.Requires(cce.NonNullElements(typeArgs));
this.tok = tok;
this.Name = name;
this.TypeArgs = typeArgs;
this.ResolvedClass = cd;
this.Path = new List();
}
///
/// This constructor constructs a resolved type parameter
///
public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, TypeParameter/*!*/ tp) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(tp != null);
this.tok = tok;
this.Name = name;
this.TypeArgs = new List();
this.ResolvedParam = tp;
this.Path = new List();
}
///
/// If type denotes a resolved class type, then return that class type.
/// Otherwise, return null.
///
public static UserDefinedType DenotesClass(Type/*!*/ type) {
Contract.Requires(type != null);
Contract.Ensures(Contract.Result() == null || Contract.Result().ResolvedClass is ClassDecl);
type = type.Normalize();
UserDefinedType ct = type as UserDefinedType;
if (ct != null && ct.ResolvedClass is ClassDecl) {
return ct;
} else {
return null;
}
}
public static Type ArrayElementType(Type type) {
Contract.Requires(type.IsArrayType);
Contract.Requires(type != null);
Contract.Ensures(Contract.Result() != null);
UserDefinedType udt = DenotesClass(type);
Contract.Assert(udt != null);
Contract.Assert(udt.TypeArgs.Count == 1); // holds true of all array types
return udt.TypeArgs[0];
}
[Pure]
public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result() != null);
string s = "";
foreach (var t in Path) {
if (context != null && t == context.tok) {
// drop the prefix up to here
s = "";
} else {
s += t.val + ".";
}
}
s += Name;
if (TypeArgs.Count != 0) {
s += "<" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ">";
}
return s;
}
public override bool SupportsEquality {
get {
if (ResolvedClass is ClassDecl) {
return true;
} else if (ResolvedClass is CoDatatypeDecl) {
return false;
} else if (ResolvedClass is IndDatatypeDecl) {
var dt = (IndDatatypeDecl)ResolvedClass;
Contract.Assume(dt.EqualitySupport != IndDatatypeDecl.ES.NotYetComputed);
if (dt.EqualitySupport == IndDatatypeDecl.ES.Never) {
return false;
}
Contract.Assert(dt.TypeArgs.Count == TypeArgs.Count);
var i = 0;
foreach (var tp in dt.TypeArgs) {
if (tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype && !TypeArgs[i].SupportsEquality) {
return false;
}
i++;
}
return true;
} else if (ResolvedParam != null) {
return ResolvedParam.MustSupportEquality;
}
Contract.Assume(false); // the SupportsEquality getter requires the Type to have been successfully resolved
return true;
}
}
}
public abstract class TypeProxy : Type {
public Type T; // filled in during resolution
internal TypeProxy() {
}
[Pure]
public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result() != null);
Contract.Assume(T == null || cce.IsPeerConsistent(T));
return T == null ? "?" : T.TypeName(context);
}
public override bool SupportsEquality {
get {
if (T != null) {
return T.SupportsEquality;
} else {
return base.SupportsEquality;
}
}
}
}
public abstract class UnrestrictedTypeProxy : TypeProxy {
}
///
/// This proxy stands for any type.
///
public class InferredTypeProxy : UnrestrictedTypeProxy {
}
///
/// This proxy stands for any type, but it originates from an instantiated type parameter.
///
public class ParamTypeProxy : UnrestrictedTypeProxy {
public TypeParameter orig;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(orig != null);
}
public ParamTypeProxy(TypeParameter orig) {
Contract.Requires(orig != null);
this.orig = orig;
}
}
public abstract class RestrictedTypeProxy : TypeProxy {
///
/// The OrderID is used to simplify the unification code. Each restricted type proxy should use its
/// own OrderID.
///
public abstract int OrderID {
get;
}
}
///
/// This proxy stands for any datatype.
///
public class DatatypeProxy : RestrictedTypeProxy {
public override int OrderID {
get {
return 0;
}
}
}
///
/// This proxy stands for object or any class/array type.
///
public class ObjectTypeProxy : RestrictedTypeProxy {
public override int OrderID {
get {
return 1;
}
}
}
///
/// This proxy stands for:
/// set(Arg) or seq(Arg) or map(Arg, Range)
///
public class CollectionTypeProxy : RestrictedTypeProxy {
public readonly Type Arg;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Arg != null);
}
public CollectionTypeProxy(Type arg) {
Contract.Requires(arg != null);
Arg = arg;
}
public override int OrderID {
get {
return 2;
}
}
}
///
/// This proxy stands for either:
/// int or set or multiset or seq
/// if AllowSeq, or:
/// int or set or multiset
/// if !AllowSeq.
///
public class OperationTypeProxy : RestrictedTypeProxy {
public readonly bool AllowSeq;
public OperationTypeProxy(bool allowSeq) {
AllowSeq = allowSeq;
}
public override int OrderID {
get {
return 3;
}
}
}
///
/// This proxy stands for:
/// seq(Arg) or array(Arg) or map(Arg, Range)
///
public class IndexableTypeProxy : RestrictedTypeProxy {
public readonly Type Arg, Domain;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Arg != null);
}
public IndexableTypeProxy(Type arg, Type domain) {
Contract.Requires(arg != null);
Arg = arg;
Domain = domain;
}
public override int OrderID {
get {
return 4;
}
}
}
// ------------------------------------------------------------------------------------------------------
public abstract class Declaration {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(tok != null);
Contract.Invariant(Name != null);
}
public IToken/*!*/ tok;
public IToken BodyStartTok = Token.NoToken;
public IToken BodyEndTok = Token.NoToken;
public readonly string/*!*/ Name;
string compileName;
public string CompileName {
get {
if (compileName == null) {
compileName = NonglobalVariable.CompilerizeName(Name);
}
return compileName;
}
}
public readonly Attributes Attributes;
public Declaration(IToken tok, string name, Attributes attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
this.tok = tok;
this.Name = name;
this.Attributes = attributes;
}
[Pure]
public override string ToString() {
Contract.Ensures(Contract.Result() != null);
return Name;
}
}
public class TypeParameter : Declaration {
public interface ParentType {
}
[Peer]
ParentType parent;
public ParentType Parent {
get {
return parent;
}
[param: Captured]
set {
Contract.Requires(Parent == null); // set it only once
Contract.Requires(value != null);
// BUGBUG: The following line is a workaround to tell the verifier that 'value' is not of an Immutable type.
// A proper solution would be to be able to express that in the program (in a specification or attribute) or
// to be able to declare 'parent' as [PeerOrImmutable].
Contract.Requires(value is TopLevelDecl || value is Function || value is Method || value is DatatypeCtor);
//modifies parent;
parent = value;
}
}
public enum EqualitySupportValue { Required, InferredRequired, Unspecified }
public EqualitySupportValue EqualitySupport; // the resolver may change this value from Unspecified to InferredRequired (for some signatures that may immediately imply that equality support is required)
public bool MustSupportEquality {
get { return EqualitySupport != EqualitySupportValue.Unspecified; }
}
public bool NecessaryForEqualitySupportOfSurroundingInductiveDatatype = false; // computed during resolution; relevant only when Parent denotes an IndDatatypeDecl
public bool IsAbstractTypeDeclaration { // true if this type parameter represents t in type t;
get { return parent == null; }
}
public bool IsToplevelScope { // true if this type parameter is on a toplevel (ie. class C), and false if it is on a member (ie. method m(...))
get { return parent is TopLevelDecl; }
}
public int PositionalIndex; // which type parameter this is (ie. in C, S is 0, T is 1 and U is 2).
public TypeParameter(IToken tok, string name, EqualitySupportValue equalitySupport = EqualitySupportValue.Unspecified)
: base(tok, name, null) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
EqualitySupport = equalitySupport;
}
}
// Represents a submodule declaration at module level scope
abstract public class ModuleDecl : TopLevelDecl
{
public ModuleSignature Signature; // filled in by resolution, in topological order.
public int Height;
public readonly bool Opened;
public ModuleDecl(IToken tok, string name, ModuleDefinition parent, bool opened)
: base(tok, name, parent, new List(), null) {
Height = -1;
Signature = null;
Opened = opened;
}
}
// Represents module X { ... }
public class LiteralModuleDecl : ModuleDecl
{
public readonly ModuleDefinition ModuleDef;
public LiteralModuleDecl(ModuleDefinition module, ModuleDefinition parent)
: base(module.tok, module.Name, parent, false) {
ModuleDef = module;
}
}
// Represents "module name = path;", where name is a identifier and path is a possibly qualified name.
public class AliasModuleDecl : ModuleDecl
{
public ModuleDecl ModuleReference; // should refer to another declaration somewhere. NOTE: cyclicity is possible, and should
// be detected and warned.
public readonly List Path; // generated by the parser, this is looked up
public ModuleDecl Root; // the moduleDecl that Path[0] refers to.
public AliasModuleDecl(List path, IToken name, ModuleDefinition parent, bool opened)
: base(name, name.val, parent, opened) {
Contract.Requires(path != null && path.Count > 0);
Path = path;
ModuleReference = null;
}
}
// Represents "module name as path [ = compilePath];", where name is a identifier and path is a possibly qualified name.
public class AbstractModuleDecl : ModuleDecl
{
public ModuleDecl Root;
public readonly List Path;
public ModuleDecl CompileRoot;
public readonly List CompilePath;
public ModuleSignature OriginalSignature;
public AbstractModuleDecl(List path, IToken name, ModuleDefinition parent, List compilePath, bool opened)
: base(name, name.val, parent, opened) {
Path = path;
Root = null;
CompilePath = compilePath;
}
}
public class ModuleSignature {
public readonly Dictionary TopLevels = new Dictionary();
public readonly Dictionary> Ctors = new Dictionary>();
public readonly Dictionary StaticMembers = new Dictionary();
public ModuleDefinition ModuleDef = null; // Note: this is null if this signature does not correspond to a specific definition (i.e.
// it is abstract). Otherwise, it points to that definition.
public ModuleSignature CompileSignature = null; // This is the version of the signature that should be used at compile time.
public ModuleSignature Refines = null;
public bool IsGhost = false;
public ModuleSignature() {}
public bool FindSubmodule(string name, out ModuleSignature pp) {
TopLevelDecl top;
pp = null;
if (TopLevels.TryGetValue(name, out top)) {
if (top is ModuleDecl) {
pp = ((ModuleDecl)top).Signature;
return true;
} else return false;
} else return false;
}
}
public class ModuleDefinition : Declaration {
public readonly List RefinementBaseName; // null if no refinement base
public ModuleDecl RefinementBaseRoot; // filled in early during resolution, corresponds to RefinementBaseName[0]
public ModuleDefinition RefinementBase; // filled in during resolution (null if no refinement base)
public readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that
public readonly Graph CallGraph = new Graph(); // filled in during resolution
public int Height; // height in the topological sorting of modules; filled in during resolution
public readonly bool IsGhost;
public readonly bool IsAbstract; // True iff this module represents an abstract interface
private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled.
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(TopLevelDecls));
Contract.Invariant(CallGraph != null);
}
public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List refinementBase, Attributes attributes, bool isBuiltinName)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
RefinementBaseName = refinementBase;
IsGhost = isGhost;
IsAbstract = isAbstract;
RefinementBaseRoot = null;
RefinementBase = null;
IsBuiltinName = isBuiltinName;
}
public virtual bool IsDefaultModule {
get {
return false;
}
}
string compileName;
new public string CompileName {
get {
if (compileName == null) {
if (IsBuiltinName)
compileName = Name;
else
compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name);
}
return compileName;
}
}
public static IEnumerable AllFunctions(List declarations) {
foreach (var d in declarations) {
var cl = d as ClassDecl;
if (cl != null) {
foreach (var member in cl.Members) {
var fn = member as Function;
if (fn != null) {
yield return fn;
}
}
}
}
}
}
public class DefaultModuleDecl : ModuleDefinition {
public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, true) {
}
public override bool IsDefaultModule {
get {
return true;
}
}
}
public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType {
public readonly ModuleDefinition Module;
public readonly List/*!*/ TypeArgs;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(TypeArgs));
}
public TopLevelDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition module, List/*!*/ typeArgs, Attributes attributes)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Module = module;
TypeArgs = typeArgs;
}
public string FullName {
get {
return Module.Name + "." + Name;
}
}
public string FullNameInContext(ModuleDefinition context) {
if (Module == context) {
return Name;
} else {
return Module.Name + "." + Name;
}
}
public string FullCompileName {
get {
return Module.CompileName + "." + CompileName;
}
}
}
public class ClassDecl : TopLevelDecl {
public readonly List/*!*/ Members;
public bool HasConstructor; // filled in (early) during resolution; true iff there exists a member that is a Constructor
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Members));
}
public ClassDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module,
List/*!*/ typeArgs, [Captured] List/*!*/ members, Attributes attributes)
: base(tok, name, module, typeArgs, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(module != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(members));
Members = members;
}
public virtual bool IsDefaultClass {
get {
return false;
}
}
}
public class DefaultClassDecl : ClassDecl {
public DefaultClassDecl(ModuleDefinition/*!*/ module, [Captured] List/*!*/ members)
: base(Token.NoToken, "_default", module, new List(), members, null) {
Contract.Requires(module != null);
Contract.Requires(cce.NonNullElements(members));
}
public override bool IsDefaultClass {
get {
return true;
}
}
}
public class ArrayClassDecl : ClassDecl {
public readonly int Dims;
public ArrayClassDecl(int dims, ModuleDefinition module)
: base(Token.NoToken, BuiltIns.ArrayClassName(dims), module,
new List(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}),
new List(), null)
{
Contract.Requires(1 <= dims);
Contract.Requires(module != null);
Dims = dims;
}
}
public abstract class DatatypeDecl : TopLevelDecl {
public readonly List/*!*/ Ctors;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Ctors));
Contract.Invariant(1 <= Ctors.Count);
}
public DatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, List/*!*/ typeArgs,
[Captured] List/*!*/ ctors, Attributes attributes)
: base(tok, name, module, typeArgs, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(module != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(ctors));
Contract.Requires(1 <= ctors.Count);
Ctors = ctors;
}
public bool HasFinitePossibleValues {
get {
return (TypeArgs.Count == 0 && Ctors.TrueForAll(ctr => ctr.Formals.Count == 0));
}
}
}
public class IndDatatypeDecl : DatatypeDecl
{
public DatatypeCtor DefaultCtor; // set during resolution
public bool[] TypeParametersUsedInConstructionByDefaultCtor; // set during resolution; has same length as the number of type arguments
public enum ES { NotYetComputed, Never, ConsultTypeArguments }
public ES EqualitySupport = ES.NotYetComputed;
public IndDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, List/*!*/ typeArgs,
[Captured] List/*!*/ ctors, Attributes attributes)
: base(tok, name, module, typeArgs, ctors, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(module != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(ctors));
Contract.Requires(1 <= ctors.Count);
}
}
public class CoDatatypeDecl : DatatypeDecl
{
public CoDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, List/*!*/ typeArgs,
[Captured] List/*!*/ ctors, Attributes attributes)
: base(tok, name, module, typeArgs, ctors, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(module != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(ctors));
Contract.Requires(1 <= ctors.Count);
}
}
public class DatatypeCtor : Declaration, TypeParameter.ParentType
{
public readonly List/*!*/ Formals;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Formals));
Contract.Invariant(Destructors != null);
Contract.Invariant(
Destructors.Count == 0 || // this is until resolution
Destructors.Count == Formals.Count); // after resolution
}
// TODO: One could imagine having a precondition on datatype constructors
public DatatypeDecl EnclosingDatatype; // filled in during resolution
public SpecialField QueryField; // filled in during resolution
public List Destructors = new List(); // contents filled in during resolution
public DatatypeCtor(IToken/*!*/ tok, string/*!*/ name, [Captured] List/*!*/ formals, Attributes attributes)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(formals));
this.Formals = formals;
}
public string FullName {
get {
Contract.Requires(EnclosingDatatype != null);
Contract.Ensures(Contract.Result() != null);
return "#" + EnclosingDatatype.FullCompileName + "." + Name;
}
}
}
public interface ICodeContext : ICallable
{
bool IsGhost { get; }
bool IsStatic { get; }
List TypeArgs { get; }
List Ins { get ; }
List Outs { get; }
ModuleDefinition EnclosingModule { get; } // to be called only after signature-resolution is complete
}
public class IteratorDecl : ClassDecl, ICodeContext
{
public readonly List Ins;
public readonly List Outs;
public readonly List OutsHistory; // these are the 'xs' variables
public readonly Specification Reads;
public readonly Specification Modifies;
public readonly Specification Decreases;
public readonly List Requires;
public readonly List Ensures;
public readonly List YieldRequires;
public readonly List YieldEnsures;
public readonly BlockStmt Body;
public readonly bool SignatureIsOmitted;
public IteratorDecl(IToken tok, string name, ModuleDefinition module, List typeArgs,
List ins, List outs,
Specification reads, Specification mod, Specification decreases,
List requires,
List ensures,
List yieldRequires,
List yieldEnsures,
BlockStmt body, Attributes attributes, bool signatureIsOmitted)
: base(tok, name, module, typeArgs, new List(), attributes)
{
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(module != null);
Contract.Requires(typeArgs != null);
Contract.Requires(ins != null);
Contract.Requires(outs != null);
Contract.Requires(reads != null);
Contract.Requires(mod != null);
Contract.Requires(decreases != null);
Contract.Requires(requires != null);
Contract.Requires(ensures != null);
Contract.Requires(yieldRequires != null);
Contract.Requires(yieldEnsures != null);
Ins = ins;
Outs = outs;
Reads = reads;
Modifies = mod;
Decreases = decreases;
Requires = requires;
Ensures = ensures;
YieldRequires = yieldRequires;
YieldEnsures = yieldEnsures;
Body = body;
SignatureIsOmitted = signatureIsOmitted;
OutsHistory = new List();
foreach (var p in Outs) {
OutsHistory.Add(new Formal(p.tok, p.Name + "s", new SeqType(p.Type), false, true));
}
}
bool ICodeContext.IsGhost { get { return false; } }
bool ICodeContext.IsStatic { get { return true; } }
List ICodeContext.TypeArgs { get { return this.TypeArgs; } }
List ICodeContext.Ins { get { return this.Ins; } }
List ICodeContext.Outs { get { return this.Outs; } }
ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } }
}
///
/// An "ICallable" is a function, method, or iterator.
///
public interface ICallable { }
public abstract class MemberDecl : Declaration {
public readonly bool IsStatic;
public readonly bool IsGhost;
public TopLevelDecl EnclosingClass; // filled in during resolution
public MemberDecl(IToken tok, string name, bool isStatic, bool isGhost, Attributes attributes)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
IsStatic = isStatic;
IsGhost = isGhost;
}
///
/// Returns className+"."+memberName. Available only after resolution.
///
public string FullName {
get {
Contract.Requires(EnclosingClass != null);
Contract.Ensures(Contract.Result() != null);
return EnclosingClass.FullName + "." + Name;
}
}
public string FullNameInContext(ModuleDefinition context) {
Contract.Requires(EnclosingClass != null);
Contract.Ensures(Contract.Result() != null);
return EnclosingClass.FullNameInContext(context) + "." + Name;
}
public string FullCompileName {
get {
Contract.Requires(EnclosingClass != null);
Contract.Ensures(Contract.Result() != null);
return EnclosingClass.FullCompileName + "." + CompileName;
}
}
}
public class Field : MemberDecl {
public readonly bool IsMutable;
public readonly Type Type;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Type != null);
}
public Field(IToken tok, string name, bool isGhost, Type type, Attributes attributes)
: this(tok, name, isGhost, true, type, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(type != null);
}
public Field(IToken tok, string name, bool isGhost, bool isMutable, Type type, Attributes attributes)
: base(tok, name, false, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(type != null);
IsMutable = isMutable;
Type = type;
}
}
public class SpecialField : Field
{
public readonly string CompiledName;
public readonly string PreString;
public readonly string PostString;
public SpecialField(IToken tok, string name, string compiledName, string preString, string postString, bool isGhost, bool isMutable, Type type, Attributes attributes)
: base(tok, name, isGhost, isMutable, type, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(compiledName != null);
Contract.Requires(preString != null);
Contract.Requires(postString != null);
Contract.Requires(type != null);
CompiledName = compiledName;
PreString = preString;
PostString = postString;
}
}
public class DatatypeDestructor : SpecialField
{
public readonly DatatypeCtor EnclosingCtor;
public readonly Formal CorrespondingFormal;
public DatatypeDestructor(IToken tok, DatatypeCtor enclosingCtor, Formal correspondingFormal, string name, string compiledName, string preString, string postString, bool isGhost, Type type, Attributes attributes)
: base(tok, name, compiledName, preString, postString, isGhost, false, type, attributes)
{
Contract.Requires(tok != null);
Contract.Requires(enclosingCtor != null);
Contract.Requires(correspondingFormal != null);
Contract.Requires(name != null);
Contract.Requires(compiledName != null);
Contract.Requires(preString != null);
Contract.Requires(postString != null);
Contract.Requires(type != null);
EnclosingCtor = enclosingCtor;
CorrespondingFormal = correspondingFormal;
}
}
public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType
{
public readonly TypeParameter TheType;
public TypeParameter.EqualitySupportValue EqualitySupport {
get { return TheType.EqualitySupport; }
}
public bool MustSupportEquality {
get { return TheType.MustSupportEquality; }
}
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(TheType != null && Name == TheType.Name);
}
public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, TypeParameter.EqualitySupportValue equalitySupport, Attributes attributes)
: base(tok, name, module, new List(), attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(module != null);
TheType = new TypeParameter(tok, name, equalitySupport);
}
}
[ContractClass(typeof(IVariableContracts))]
public interface IVariable {
string/*!*/ Name {
get;
}
string/*!*/ DisplayName { // what the user thinks he wrote
get;
}
string/*!*/ UniqueName {
get;
}
string/*!*/ CompileName {
get;
}
Type/*!*/ Type {
get;
}
bool IsMutable {
get;
}
bool IsGhost {
get;
}
}
[ContractClassFor(typeof(IVariable))]
public abstract class IVariableContracts : IVariable {
public string Name {
get {
Contract.Ensures(Contract.Result() != null);
throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
}
}
public string DisplayName {
get {
Contract.Ensures(Contract.Result() != null);
throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
}
}
public string UniqueName {
get {
Contract.Ensures(Contract.Result() != null);
throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
}
}
public string CompileName {
get {
Contract.Ensures(Contract.Result() != null);
throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
}
}
public Type Type {
get {
Contract.Ensures(Contract.Result() != null);
throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
}
}
public bool IsMutable {
get {
throw new NotImplementedException();
}
}
public bool IsGhost {
get {
throw new NotImplementedException();
}
}
}
public abstract class NonglobalVariable : IVariable {
public readonly IToken tok;
readonly string name;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(tok != null);
Contract.Invariant(name != null);
Contract.Invariant(type != null);
}
public string Name {
get {
Contract.Ensures(Contract.Result() != null);
return name;
}
}
public string/*!*/ DisplayName {
get { return VarDecl.DisplayNameHelper(this); }
}
readonly int varId = varIdCount++;
public string UniqueName {
get {
Contract.Ensures(Contract.Result() != null);
return name + "#" + varId;
}
}
static char[] specialChars = new char[] { '\'', '_', '?', '\\' };
public static string CompilerizeName(string nm) {
string name = null;
int i = 0;
while (true) {
int j = nm.IndexOfAny(specialChars, i);
if (j == -1) {
if (i == 0) {
return nm; // this is the common case
} else {
return name + nm.Substring(i);
}
} else {
string nxt = nm.Substring(i, j - i);
name = name == null ? nxt : name + nxt;
switch (nm[j]) {
case '\'': name += "_k"; break;
case '_': name += "__"; break;
case '?': name += "_q"; break;
case '\\': name += "_b"; break;
default:
Contract.Assume(false); // unexpected character
break;
}
i = j + 1;
if (i == nm.Length) {
return name;
}
}
}
}
protected string compileName;
public virtual string CompileName {
get {
if (compileName == null) {
compileName = string.Format("_{0}_{1}", varId, CompilerizeName(name));
}
return compileName;
}
}
Type type;
//[Pure(false)] // TODO: if Type gets the status of [Frozen], then this attribute is not needed
public Type/*!*/ Type {
get {
Contract.Ensures(Contract.Result() != null);
return type.Normalize();
}
}
public abstract bool IsMutable {
get;
}
bool isGhost; // readonly, except for BoundVar's of match expressions/statements during resolution
public bool IsGhost {
get {
return isGhost;
}
set {
isGhost = value;
}
}
public NonglobalVariable(IToken tok, string name, Type type, bool isGhost) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(type != null);
this.tok = tok;
this.name = name;
this.type = type;
this.isGhost = isGhost;
}
internal static int varIdCount; // this varIdCount is used for both NonglobalVariable's and VarDecl's.
}
public class Formal : NonglobalVariable {
public readonly bool InParam; // true to in-parameter, false for out-parameter
public override bool IsMutable {
get {
return !InParam;
}
}
public Formal(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type, bool inParam, bool isGhost)
: base(tok, name, type, isGhost) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(type != null);
InParam = inParam;
}
public bool HasName {
get {
return !Name.StartsWith("#");
}
}
public override string CompileName {
get {
if (compileName == null) {
compileName = CompilerizeName(Name);
}
return compileName;
}
}
}
///
/// A "ThisSurrogate" is used during translation time to make the treatment of the receiver more similar to
/// the treatment of other in-parameters.
///
public class ThisSurrogate : Formal
{
public ThisSurrogate(IToken tok, Type type)
: base(tok, "this", type, true, false) {
Contract.Requires(tok != null);
Contract.Requires(type != null);
}
}
public class BoundVar : NonglobalVariable {
public override bool IsMutable {
get {
return false;
}
}
public BoundVar(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type)
: base(tok, name, type, false) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(type != null);
}
}
public class Function : MemberDecl, TypeParameter.ParentType, ICallable {
public bool IsRecursive; // filled in during resolution
public readonly List/*!*/ TypeArgs;
public readonly IToken OpenParen; // can be null (for predicates), if there are no formals
public readonly List/*!*/ Formals;
public readonly Type/*!*/ ResultType;
public readonly List/*!*/ Req;
public readonly List/*!*/ Reads;
public readonly List/*!*/ Ens;
public readonly Specification/*!*/ Decreases;
public Expression Body; // an extended expression; Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution
public readonly bool SignatureIsOmitted; // is "false" for all Function objects that survive into resolution
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(TypeArgs));
Contract.Invariant(cce.NonNullElements(Formals));
Contract.Invariant(ResultType != null);
Contract.Invariant(cce.NonNullElements(Req));
Contract.Invariant(cce.NonNullElements(Reads));
Contract.Invariant(cce.NonNullElements(Ens));
Contract.Invariant(Decreases != null);
}
///
/// Note, functions are "ghost" by default; a non-ghost function is called a "function method".
///
public Function(IToken tok, string name, bool isStatic, bool isGhost,
List typeArgs, IToken openParen, List formals, Type resultType,
List req, List reads, List ens, Specification decreases,
Expression body, Attributes attributes, bool signatureOmitted)
: base(tok, name, isStatic, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(formals));
Contract.Requires(resultType != null);
Contract.Requires(cce.NonNullElements(req));
Contract.Requires(cce.NonNullElements(reads));
Contract.Requires(cce.NonNullElements(ens));
Contract.Requires(decreases != null);
this.TypeArgs = typeArgs;
this.OpenParen = openParen;
this.Formals = formals;
this.ResultType = resultType;
this.Req = req;
this.Reads = reads;
this.Ens = ens;
this.Decreases = decreases;
this.Body = body;
this.SignatureIsOmitted = signatureOmitted;
}
}
public class Predicate : Function
{
public enum BodyOriginKind
{
OriginalOrInherited, // this predicate definition is new (and the predicate may or may not have a body), or the predicate's body (whether or not it exists) is being inherited unmodified (from the previous refinement--it may be that the inherited body was itself an extension, for example)
DelayedDefinition, // this predicate declaration provides, for the first time, a body--the declaration refines a previously declared predicate, but the previous one had no body
Extension // this predicate extends the definition of a predicate with a body in a module being refined
}
public readonly BodyOriginKind BodyOrigin;
public Predicate(IToken tok, string name, bool isStatic, bool isGhost,
List typeArgs, IToken openParen, List formals,
List req, List reads, List ens, Specification decreases,
Expression body, BodyOriginKind bodyOrigin, Attributes attributes, bool signatureOmitted)
: base(tok, name, isStatic, isGhost, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureOmitted) {
Contract.Requires(bodyOrigin == Predicate.BodyOriginKind.OriginalOrInherited || body != null);
BodyOrigin = bodyOrigin;
}
}
public class CoPredicate : Function
{
public readonly List Uses = new List(); // filled in during resolution, used by verifier
public CoPredicate(IToken tok, string name, bool isStatic,
List typeArgs, IToken openParen, List formals,
List req, List reads, List ens,
Expression body, Attributes attributes, bool signatureOmitted)
: base(tok, name, isStatic, true, typeArgs, openParen, formals, new BoolType(),
req, reads, ens, new Specification(new List(), null), body, attributes, signatureOmitted) {
}
}
public class Method : MemberDecl, TypeParameter.ParentType, ICodeContext
{
public readonly bool SignatureIsOmitted;
public bool MustReverify;
public readonly List/*!*/ TypeArgs;
public readonly List/*!*/ Ins;
public readonly List/*!*/ Outs;
public readonly List/*!*/ Req;
public readonly Specification/*!*/ Mod;
public readonly List/*!*/ Ens;
public readonly Specification/*!*/ Decreases;
public BlockStmt Body; // Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution
public bool IsTailRecursive; // filled in during resolution
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(TypeArgs));
Contract.Invariant(cce.NonNullElements(Ins));
Contract.Invariant(cce.NonNullElements(Outs));
Contract.Invariant(cce.NonNullElements(Req));
Contract.Invariant(Mod != null);
Contract.Invariant(cce.NonNullElements(Ens));
Contract.Invariant(Decreases != null);
}
public Method(IToken tok, string name,
bool isStatic, bool isGhost,
[Captured] List/*!*/ typeArgs,
[Captured] List/*!*/ ins, [Captured] List/*!*/ outs,
[Captured] List/*!*/ req, [Captured] Specification/*!*/ mod,
[Captured] List/*!*/ ens,
[Captured] Specification/*!*/ decreases,
[Captured] BlockStmt body,
Attributes attributes, bool signatureOmitted)
: base(tok, name, isStatic, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(ins));
Contract.Requires(cce.NonNullElements(outs));
Contract.Requires(cce.NonNullElements(req));
Contract.Requires(mod != null);
Contract.Requires(cce.NonNullElements(ens));
Contract.Requires(decreases != null);
this.TypeArgs = typeArgs;
this.Ins = ins;
this.Outs = outs;
this.Req = req;
this.Mod = mod;
this.Ens = ens;
this.Decreases = decreases;
this.Body = body;
this.SignatureIsOmitted = signatureOmitted;
MustReverify = false;
}
bool ICodeContext.IsGhost { get { return this.IsGhost; } }
bool ICodeContext.IsStatic { get { return this.IsStatic; } }
List ICodeContext.TypeArgs { get { return this.TypeArgs; } }
List ICodeContext.Ins { get { return this.Ins; } }
List ICodeContext.Outs { get { return this.Outs; } }
ModuleDefinition ICodeContext.EnclosingModule {
get {
Contract.Assert(this.EnclosingClass != null); // this getter is supposed to be called only after signature-resolution is complete
return this.EnclosingClass.Module;
}
}
}
public class Constructor : Method
{
public Constructor(IToken tok, string name,
[Captured] List/*!*/ typeArgs,
[Captured] List/*!*/ ins,
[Captured] List/*!*/ req, [Captured] Specification/*!*/ mod,
[Captured] List/*!*/ ens,
[Captured] Specification/*!*/ decreases,
[Captured] BlockStmt body,
Attributes attributes, bool signatureOmitted)
: base(tok, name, false, false, typeArgs, ins, new List(), req, mod, ens, decreases, body, attributes, signatureOmitted) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(ins));
Contract.Requires(cce.NonNullElements(req));
Contract.Requires(mod != null);
Contract.Requires(cce.NonNullElements(ens));
Contract.Requires(decreases != null);
}
}
// ------------------------------------------------------------------------------------------------------
public abstract class Statement {
public readonly IToken Tok;
public LList