Uses of Class
org.jmlspecs.jmlrac.AssertionMethod

Packages that use AssertionMethod

org.jmlspecs.jmlrac

Generates Java classes from JML specifications that check assertions at runtime.

Uses of AssertionMethod in org.jmlspecs.jmlrac

Subclasses of AssertionMethod in org.jmlspecs.jmlrac

class	ConstraintMethod A class for generating assertion check methods for (history) constraints.
class	ExceptionalPostconditionMethod A class for generating exceptional postcondition check methods.
class	InvariantLikeMethod A class for generating assertion check methods for class-level assertions such as invariants and history constraints.
class	InvariantMethod A class for generating assertion check methods for invariants.
class	LocalConstraintMethod A class for generating constaint check methods that check locally specified type constraints without inheriting any constraints from supertypes.
class	MotherConstraintMethod A class for generating constraint check methods that check locally specified type constraints and inherit constraints from supertypes.
class	PostconditionMethod A class for generating postcondition check methods.
class	PreconditionMethod A class for generating precondition check methods.
class	PreOrPostconditionMethod An abstract class for generating precondition or postconditin check methods for the given methods.
class	SubtypeConstraintMethod A class for generating constaint check methods that check locally specified type constraints and inherit constraints from supertypes.