|
|||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||
| Packages that use jml2b.formula | |
| jml2b.formula | Provides the classes necessary to create and manage formulas. |
| jml2b.languages | |
| jml2b.languages.java | |
| jml2b.pog | Provides the classes necessary to generate proof obligations. |
| jml2b.pog.lemma | |
| jml2b.pog.proofobligation | |
| jml2b.pog.substitution | Provides the classes necessary to create and manage substitutions. |
| jml2b.pog.util | |
| jml2b.structure | |
| jml2b.structure.bytecode | |
| jml2b.structure.java | |
| jml2b.structure.jml | Provides the classes necessary to create and manage jml clauses such that depends, represents, specification cases, modifies and exsures. |
| jml2b.structure.statement | Provides the classes necessary to create and manage java and jml statements and expressions. |
| jpov.structure | |
| jpov.substitution | |
| jpov.viewer.lemma | |
| Classes in jml2b.formula used by jml2b.formula | |
| BasicType
Type of formula, the type can be boolean integer reference proposition JML \TYPE function of two types. |
|
| BinaryForm
This class implements binary formula. |
|
| ElementsForm
This class implements terminal formulas that correspond to variables xxxelements_n, where xxx can be int, short, byte, boolean, char ou ref and n is a natural number. |
|
| Formula
This class describes a formula. |
|
| IFormToken
This interface defines the token associated to formulas corresponding to operators. |
|
| IModifiesField
|
|
| ModifiedFieldForm
|
|
| QuantifiedForm
This class implements quantified formula: universal, existential or union. |
|
| QuantifiedVarForm
This class implements a list of quatified variables. |
|
| TerminalForm
This class implements terminal formula: identifiers, literal constants and builtin types. |
|
| TriaryForm
This class implements tri-ary formula, that is conditional formula coming from the Java structure a ? b : c or equals with restricted
domains formulas. |
|
| TTypeForm
This class implements type formula. |
|
| UnaryForm
This class implements unary Formula. |
|
| Classes in jml2b.formula used by jml2b.languages | |
| Formula
This class describes a formula. |
|
| QuantifiedVarForm
This class implements a list of quatified variables. |
|
| TerminalForm
This class implements terminal formula: identifiers, literal constants and builtin types. |
|
| Classes in jml2b.formula used by jml2b.languages.java | |
| BinaryForm
This class implements binary formula. |
|
| Formula
This class describes a formula. |
|
| IFormToken
This interface defines the token associated to formulas corresponding to operators. |
|
| ModifiedFieldForm
|
|
| QuantifiedForm
This class implements quantified formula: universal, existential or union. |
|
| QuantifiedVarForm
This class implements a list of quatified variables. |
|
| TerminalForm
This class implements terminal formula: identifiers, literal constants and builtin types. |
|
| TriaryForm
This class implements tri-ary formula, that is conditional formula coming from the Java structure a ? b : c or equals with restricted
domains formulas. |
|
| TTypeForm
This class implements type formula. |
|
| UnaryForm
This class implements unary Formula. |
|
| Classes in jml2b.formula used by jml2b.pog | |
| Formula
This class describes a formula. |
|
| IFormToken
This interface defines the token associated to formulas corresponding to operators. |
|
| Classes in jml2b.formula used by jml2b.pog.lemma | |
| Formula
This class describes a formula. |
|
| IFormToken
This interface defines the token associated to formulas corresponding to operators. |
|
| Classes in jml2b.formula used by jml2b.pog.proofobligation | |
| Formula
This class describes a formula. |
|
| IFormToken
This interface defines the token associated to formulas corresponding to operators. |
|
| Classes in jml2b.formula used by jml2b.pog.substitution | |
| ElementsForm
This class implements terminal formulas that correspond to variables xxxelements_n, where xxx can be int, short, byte, boolean, char ou ref and n is a natural number. |
|
| Formula
This class describes a formula. |
|
| IFormToken
This interface defines the token associated to formulas corresponding to operators. |
|
| Classes in jml2b.formula used by jml2b.pog.util | |
| Formula
This class describes a formula. |
|
| IFormToken
This interface defines the token associated to formulas corresponding to operators. |
|
| Classes in jml2b.formula used by jml2b.structure | |
| IModifiesField
|
|
| Classes in jml2b.formula used by jml2b.structure.bytecode | |
| IModifiesField
|
|
| Classes in jml2b.formula used by jml2b.structure.java | |
| Formula
This class describes a formula. |
|
| IModifiesField
|
|
| Classes in jml2b.formula used by jml2b.structure.jml | |
| Formula
This class describes a formula. |
|
| IFormToken
This interface defines the token associated to formulas corresponding to operators. |
|
| IModifiesField
|
|
| Classes in jml2b.formula used by jml2b.structure.statement | |
| Formula
This class describes a formula. |
|
| IFormToken
This interface defines the token associated to formulas corresponding to operators. |
|
| IModifiesField
|
|
| Classes in jml2b.formula used by jpov.structure | |
| Formula
This class describes a formula. |
|
| Classes in jml2b.formula used by jpov.substitution | |
| IFormToken
This interface defines the token associated to formulas corresponding to operators. |
|
| Classes in jml2b.formula used by jpov.viewer.lemma | |
| Formula
This class describes a formula. |
|
|
|||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||