| java.lang.Object de.uka.ilkd.key.proof.init.CreatedAttributeTermFactory
CreatedAttributeTermFactory | public class CreatedAttributeTermFactory (Code) | | Convenience class for creating terms related to the implicit
"created" attribute.
Should possibly be merged into TermBuilder?
|
createCreatedAndNotNullTerm | public Term createCreatedAndNotNullTerm(Services services, Term objectTerm)(Code) | | Creates the formula "objectTerm. = TRUE & objectTerm != null"
|
createCreatedNotNullQuantifierTerm | public Term createCreatedNotNullQuantifierTerm(Services services, Quantifier q, LogicVariable[] vars, Term subTerm)(Code) | | Creates a quantifier term where the quantification only covers
objects which have already been created and which are not null.
|
createCreatedNotNullQuantifierTerm | public Term createCreatedNotNullQuantifierTerm(Services services, Quantifier q, LogicVariable var, Term subTerm)(Code) | | Creates a quantifier term where the quantification only covers
objects which have already been created and which are not null.
|
createCreatedOrNullTerm | public Term createCreatedOrNullTerm(Services services, Term objectTerm)(Code) | | Creates the formula "objectTerm. = TRUE | objectTerm = null"
|
createCreatedTerm | public Term createCreatedTerm(Services services, Term objectTerm)(Code) | | Creates the formula "objectTerm. = TRUE".
|
|
|