public static class AbstractBlockContractRule.BlockContractHint
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
protected static AbstractBlockContractRule.BlockContractHint |
USAGE_BRANCH |
Constructor and Description |
---|
BlockContractHint(java.lang.String description) |
BlockContractHint(java.lang.String description,
ProgramVariable excVar) |
Modifier and Type | Method and Description |
---|---|
static AbstractBlockContractRule.BlockContractHint |
createUsageBranchHint() |
static AbstractBlockContractRule.BlockContractHint |
createValidityBranchHint(ProgramVariable excVar) |
java.lang.String |
getDescription() |
ProgramVariable |
getExceptionalVariable() |
java.lang.String |
toString() |
protected static final AbstractBlockContractRule.BlockContractHint USAGE_BRANCH
public BlockContractHint(java.lang.String description)
public BlockContractHint(java.lang.String description, ProgramVariable excVar)
public static AbstractBlockContractRule.BlockContractHint createUsageBranchHint()
public static AbstractBlockContractRule.BlockContractHint createValidityBranchHint(ProgramVariable excVar)
public ProgramVariable getExceptionalVariable()
public java.lang.String getDescription()
public java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.