|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||
| Packages that use JMLCheckable | |
| org.jmlspecs.jmlrac.runtime | Classes for use during runtime assertion checking for code compiled with JML's runtime assertion checking compiler (jmlc). |
| Uses of JMLCheckable in org.jmlspecs.jmlrac.runtime |
| Fields in org.jmlspecs.jmlrac.runtime declared as JMLCheckable | |
protected JMLCheckable |
JMLSurrogate.self
object that this object is surrogate for. |
| Methods in org.jmlspecs.jmlrac.runtime that return JMLCheckable | |
JMLCheckable |
JMLSurrogate.getSelf()
Returns the delegee of this object. |
| Constructors in org.jmlspecs.jmlrac.runtime with parameters of type JMLCheckable | |
JMLSurrogate(JMLCheckable self)
Constructs a new surrogate for the given object, obj. |
|
|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||