|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||
| Packages that use org.jmlspecs.jmlrac.runtime | |
| org.jmlspecs.jmlrac.runtime | Classes for use during runtime assertion checking for code compiled with JML's runtime assertion checking compiler (jmlc). |
| org.jmlspecs.jmlunit.strategies | The types in this package are used in providing test data for JML/JUnit testing. |
| org.jmlspecs.lang | This package is a collection of types used in the definition of the JML language. |
| org.jmlspecs.models | This package is a collection of types with immutable objects; it also enumerators (which have mutable objects) for the types of the immutable collections in the package. |
| org.jmlspecs.models.resolve | This package is a collection of types with immutable objects based on the RESOLVE specification language's mathematical models. |
| org.jmlspecs.samples.dbc | This package contains samples of JML specifications written in the style of design by contract. |
| org.jmlspecs.samples.digraph | This package contains samples of JML specifications for directed graphs. |
| org.jmlspecs.samples.jmlkluwer | This package contains samples of JML specifications from the paper "JML: a Notation for Detailed Design". |
| org.jmlspecs.samples.jmlrefman | This package contains samples of JML specifications from the JML Reference Manual. |
| org.jmlspecs.samples.jmltutorial | This package contains samples of JML specifications from the tutorials. |
| org.jmlspecs.samples.list.list1 | |
| org.jmlspecs.samples.list.list1.node | |
| org.jmlspecs.samples.list.list2 | |
| org.jmlspecs.samples.list.node | |
| org.jmlspecs.samples.list.node2 | |
| org.jmlspecs.samples.misc | This package contains miscellaneous samples of JML specifications. |
| org.jmlspecs.samples.prelimdesign | This package contains samples of JML specifications from the paper Preliminary Design of JML. |
| org.jmlspecs.samples.reader | This package contains samples of JML specifications relating to some abstractions of input and output. |
| org.jmlspecs.samples.sets | This package contains samples of JML specifications relating to sets. |
| org.jmlspecs.samples.stacks | This package contains samples of JML specifications relating to stacks of various sorts. |
| org.jmlspecs.samples.table | This package contains samples of JML specifications relating to tables. |
| org.jmlspecs.util | |
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.jmlrac.runtime | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| JMLCheckable
The common behavior of all runtime assertion checkable classes. |
|
| JMLExceptionalPostconditionError
A JML error class to notify exceptional postcondition violations. |
|
| JMLExitPostconditionError
A mark interface for JML exit postcondition errors. |
|
| JMLInternalPostconditionError
A mark interface for JML internal postcondition errors. |
|
| JMLIntraconditionError
A JML exception class to signal intracondition violations. |
|
| JMLNonExecutableException
Thrown by generated runtime assertion check code to indicate that an attempt has been made to execute a JML expression that is not executable. |
|
| JMLNormalPostconditionError
A JML error class to notify normal postcondition violations. |
|
| JMLOption
An interface to provide compile-time and runtime options. |
|
| JMLPostconditionError
A JML error class to notify postcondition violations. |
|
| JMLPreconditionError
A JML exception class for notifying precondition violations. |
|
| JMLRacValue
A class for denoting JML expressible values for the runtime assertion checker. |
|
| JMLSurrogate.MapKey
A class for implementing keys for the method cache. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.jmlunit.strategies | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.lang | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.models | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.models.resolve | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.dbc | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.digraph | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.jmlkluwer | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.jmlrefman | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.jmltutorial | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.list.list1 | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.list.list1.node | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.list.list2 | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.list.node | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.list.node2 | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.misc | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.prelimdesign | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.reader | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.sets | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.stacks | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.samples.table | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
| Classes in org.jmlspecs.jmlrac.runtime used by org.jmlspecs.util | |
| JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations. |
|
|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||