See: Description
| Interface | Description |
|---|---|
| SequentPrintFilterEntry |
One element of a sequent as delivered by SequentPrintFilter
|
| VisibleTermLabels |
This abstract class is used by SequentViewLogicPrinter to determine the set
of printed TermLabels.
|
| Class | Description |
|---|---|
| AbbrevMap | |
| AbbrevMap.AbbrevWrapper | |
| CharListNotation | |
| FieldPrinter |
Common superclass of
StorePrinter and SelectPrinter. |
| HideSequentPrintFilter |
This filter takes a search string and yields a sequent containing only
sequent formulas that match the search.
|
| IdentitySequentPrintFilter |
Identity Filter not doing anything
|
| IdentitySequentPrintFilter.IdentityFilterEntry |
A filter entry, representing one sequent formula.
|
| InitialPositionTable |
An InitialPositionTable is a PositionTable that describes the
beginning of the element/subelement relationship.
|
| LogicPrinter |
The front end for the Sequent pretty-printer.
|
| LogicPrinter.PosTableStringBackend |
A
Backend which puts its
result in a StringBuffer and builds a PositionTable. |
| LogicPrinter.StackEntry |
Utility class for stack entries containing the position table
and the position of the start of the subterm in the result.
|
| ModalityPositionTable |
This is a position table for program modality formulae.
|
| Notation |
Encapsulate the concrete syntax used to print a term.
|
| Notation.CastFunction |
The standard concrete syntax for casts.
|
| Notation.CharLiteral |
The standard concrete syntax for the character literal indicator `C'.
|
| Notation.Constant |
The standard concrete syntax for constants like true and false.
|
| Notation.ElementaryUpdateNotation |
The standard concrete syntax for elementary updates.
|
| Notation.ElementOfNotation |
The standard concrete syntax for the element of operator.
|
| Notation.FunctionNotation |
The standard concrete syntax for function and predicate terms.
|
| Notation.HeapConstructorNotation |
The standard concrete syntax for heap constructors.
|
| Notation.IfThenElse |
The standard concrete syntax for conditional terms
if (phi) (t1) (t2). |
| Notation.Infix |
The standard concrete syntax for infix operators.
|
| Notation.LabelNotation | |
| Notation.ModalityNotation |
The standard concrete syntax for DL modalities box and diamond.
|
| Notation.ModalSVNotation |
The concrete syntax for DL modalities represented with a
SchemaVariable.
|
| Notation.NumLiteral |
The standard concrete syntax for the number literal indicator `Z'.
|
| Notation.ObserverNotation |
The standard concrete syntax for observer function terms.
|
| Notation.ParallelUpdateNotation |
The standard concrete syntax for parallel updates
|
| Notation.Postfix |
The standard concrete syntax for length.
|
| Notation.Prefix |
The standard concrete syntax for prefix operators.
|
| Notation.Quantifier |
The standard concrete syntax for quantifiers.
|
| Notation.SchemaVariableNotation | |
| Notation.SelectNotation |
The standard concrete syntax for select.
|
| Notation.SeqConcatNotation | |
| Notation.SeqGetNotation | |
| Notation.SeqSingletonNotation |
The standard concrete syntax for sequence singletons.
|
| Notation.SingletonNotation |
The standard concrete syntax for singleton sets.
|
| Notation.StoreNotation |
The standard concrete syntax for store.
|
| Notation.Subst |
The standard concrete syntax for substitution terms.
|
| Notation.UpdateApplicationNotation |
The standard concrete syntax for update application.
|
| Notation.VariableNotation |
The standard concrete syntax for all kinds of variables.
|
| NotationInfo |
Stores the mapping from operators to
Notations. |
| PosInSequent |
describes a position in a sequent including the bounds within a string
representation of the sequent.
|
| PositionTable |
A PositionTable describes the start and end positions of substrings of a
String in order to get a PosInSequent from an int describing a position in a
string representing a Term or a Sequent, etc.
|
| ProgramPrinter | |
| Range |
A class specifying a range of integer numbers e.g. character positions.
|
| RegroupSequentPrintFilter | |
| SearchSequentPrintFilter |
This is an interface for filters that are used to
modify the sequent view, improving the search function.
|
| SelectPrinter |
This class is used by LogicPrinter.java to print out select-terms, i.e. terms
of the following form: T::select(heap, object, field)
|
| SequentPrintFilter |
Filter a given sequent to prepare it for the SequentPrinter class
by adjusting constraints, deleting formulas, etc.
|
| SequentViewLogicPrinter |
Subclass of
LogicPrinter used in GUI. |
| StorePrinter |
This class is used by LogicPrinter.java to print out store-terms, i.e. terms
of the following form: store(heap, object, field, value)
|
| Enum | Description |
|---|---|
| LogicPrinter.MarkType | |
| LogicPrinter.QuantifiableVariablePrintMode |
| Exception | Description |
|---|---|
| AbbrevException | |
| IllegalRegexException |
This exception is thrown when a String is expected be a valid
regular expression, but is not.
|