| java.lang.Object
 de.uka.ilkd.key.proof.init.LDTInput
| LDTInput | | public class LDTInput implements EnvInput(Code) | | Represents the LDT .key files as a whole. Special treatment of these
files is necessary because their parts need to be read in a special
order, namely first all sort declarations then all function and predicate
declarations and third the rules. This procedure makes it possible to
use all declared sorts in all rules.
|
| Constructor Summary | |
| public | LDTInput(KeYFile[] keyFiles, Main main)
creates a representation of the LDT files to be used as input
to the KeY prover. |
| LDTInput | | public LDTInput(KeYFile[] keyFiles, Main main)(Code) | | creates a representation of the LDT files to be used as input
to the KeY prover.
Parameters:
keyFiles - an array containing the LDT .key files
Parameters:
main - the main class used to report the progress of reading |
| getNumberOfChars | | public int getNumberOfChars()(Code) | | |
| hashCode | | public int hashCode()(Code) | | |
| read | | public void read(ModStrategy mod) throws ProofInputException(Code) | | reads all LDTs, i.e., all associated .key files with respect to
the given modification strategy. Reading is done in a special order: first
all sort declarations then all function and predicate declarations and
third the rules. This procedure makes it possible to use all declared
sorts in all rules, e.g.
|
|
|