JmlContract
constructor(jmlTags: NodeList<SimpleName>, type: ContractType, behavior: Behavior, name: SimpleName, modifiers: NodeList<Modifier>, clauses: NodeList<JmlClause>, subContracts: NodeList<JmlContract>)(source)
constructor(type: ContractType, behavior: Behavior, name: SimpleName, modifiers: NodeList<Modifier>, clauses: NodeList<JmlClause>, subContracts: NodeList<JmlContract>)(source)
constructor(range: TokenRange, behavior: Behavior, modifiers: NodeList<Modifier>, clauses: NodeList<JmlClause>, subContracts: NodeList<JmlContract>)(source)
constructor(tokenRange: TokenRange, isLoopContract: Boolean, behavior: Behavior, modifiers: NodeList<Modifier>, clauses: NodeList<JmlClause>, subContracts: NodeList<JmlContract>)(source)
constructor(tokenRange: TokenRange, type: ContractType, isLoopContract: Boolean, behavior: Behavior, name: SimpleName, modifiers: NodeList<Modifier>, clauses: NodeList<JmlClause>, subContracts: NodeList<JmlContract>)(source)
constructor(tokenRange: TokenRange, jmlTags: NodeList<SimpleName>, type: ContractType, behavior: Behavior, name: SimpleName, modifiers: NodeList<Modifier>, clauses: NodeList<JmlClause>, subContracts: NodeList<JmlContract>)(source)
This constructor is used by the parser and is considered private.