|
| |
|
| java.lang.Object
All known Subclasses: org.jmlspecs.models.JMLObjectToEqualsRelationEnumerator, org.jmlspecs.models.JMLValueSetEnumerator, org.jmlspecs.models.JML_Domain_To_Range_RelationImageEnumerator, de.uka.ilkd.key.proof.DiffMyers, de.uka.ilkd.key.rule.CheckPrgTransfSoundness, de.uka.ilkd.key.pp.PosInSequent, de.uka.ilkd.key.strategy.termProjection.CoeffGcdProjection, de.uka.ilkd.key.proof.decproc.smtlib.Formula, org.jmlspecs.models.JMLValueToValueRelation, de.uka.ilkd.key.strategy.QueueRuleApplicationManager, org.jmlspecs.models.JMLListObjectNode, org.jmlspecs.models.JMLObjectEqualsPair, de.uka.ilkd.key.proof.NullNewRuleListener, de.uka.ilkd.key.rule.inst.ProgramSVEntry, de.uka.ilkd.key.proof.mgt.ModalityClass, de.uka.ilkd.key.unittest.cogent.CogentModelGenerator, de.uka.ilkd.key.parser.Location, de.uka.ilkd.key.parser.ocl.FormulaBoolConverter, de.uka.ilkd.key.proof.init.LDTInput, de.uka.ilkd.key.proof.ProofEvent, org.jmlspecs.models.JMLEqualsBag, org.jmlspecs.lang.JMLDataGroup, org.jmlspecs.models.JMLObjectToEqualsRelationImageEnumerator, java.util.AbstractCollection, de.uka.ilkd.key.rule.UpdatePair, de.uka.ilkd.key.rule.encapsulation.RootScheme, org.jmlspecs.models.JMLObjectToObjectRelationEnumerator, de.uka.ilkd.key.util.Debug, org.jmlspecs.models.JMLObjectSequence, java.util.VMTimeZone, de.uka.ilkd.key.strategy.LongRuleAppCost, javacard.framework.Util, java.lang.Compiler, de.uka.ilkd.key.proof.TacletAppIndex, de.uka.ilkd.key.proof.incclosure.BinaryMerger, de.uka.ilkd.key.ocl.gf.StringTuple, de.uka.ilkd.key.rule.updatesimplifier.AbstractAssignmentPairLazy, de.uka.ilkd.key.proof.reuse.ReuseFindTaclet, de.uka.ilkd.key.ocl.gf.RefinementMenu, de.uka.ilkd.key.pp.ConstraintSequentPrintFilter, de.uka.ilkd.key.strategy.feature.LetFeature, de.uka.ilkd.key.rule.NotFreeIn, de.uka.ilkd.key.proof.NodeInfo, java.io.File, de.uka.ilkd.key.proof.mgt.InstantiatedMethodContract, de.uka.ilkd.key.parser.ocl.OCLCollection, de.uka.ilkd.key.rule.TacletBuilder, de.uka.ilkd.key.proof.mgt.ComplexRuleJustificationBySpec, org.jmlspecs.models.JMLEqualsToValueRelationImageEnumerator, de.uka.ilkd.key.strategy.feature.ApplyTFFeature, de.uka.ilkd.key.strategy.termfeature.BinarySumTermFeature, org.jmlspecs.models.JMLEqualsToValueRelationEnumerator, de.uka.ilkd.key.visualdebugger.BreakpointManager, de.uka.ilkd.key.ocl.OCLExport, de.uka.ilkd.key.proof.mgt.UpdatePairWithGuard, de.uka.ilkd.key.ocl.gf.GFinterface, de.uka.ilkd.key.proof.SimplifyIntegerRuleFilter, de.uka.ilkd.key.rule.AutomatedContractConfigurator, de.uka.ilkd.key.proof.decproc.smtlib.Signature, de.uka.ilkd.key.visualdebugger.executiontree.ExecutionTree, de.uka.ilkd.key.rule.UseMethodContractRule, de.uka.ilkd.key.rule.inst.SVInstantiations, de.uka.ilkd.key.rule.export.TacletExporter, de.uka.ilkd.key.proof.init.ModStrategy, de.uka.ilkd.key.proof.decproc.TypeBoundTranslation, de.uka.ilkd.key.rule.BoundUniquenessChecker, de.uka.ilkd.key.strategy.termgenerator.AllowedCutPositionsGenerator, java.io.FileDescriptor, de.uka.ilkd.key.strategy.termgenerator.RootsGenerator, org.jmlspecs.models.JMLEqualsSequence, de.uka.ilkd.key.proof.TacletIndex, org.jmlspecs.models.JMLEqualsToObjectRelationEnumerator, de.uka.ilkd.key.strategy.quantifierHeuristics.InstantiationCostScalerFeature, org.jmlspecs.models.JMLByte, de.uka.ilkd.key.proof.ApplyTacletDialogModel, org.jmlspecs.models.JMLEqualsSetEnumerator, java.util.TimerTask, de.uka.ilkd.key.proof.decproc.translation.TranslateLogicVariable, de.uka.ilkd.key.proof.BuiltInRuleAppIndex, de.uka.ilkd.key.proof.reuse.ReuseUpdateSimplificationRule, de.uka.ilkd.key.strategy.StrategyFactory, de.uka.ilkd.key.util.install.KeYInstaller, org.jmlspecs.models.JMLObjectToObjectRelationImageEnumerator, de.uka.ilkd.key.parser.ocl.MethodResolver, de.uka.ilkd.key.visualdebugger.PCLabel, de.uka.ilkd.key.speclang.AbstractClassInvariant, de.uka.ilkd.key.proof.init.CreatedAttributeTermFactory, java.util.EventListenerProxy, de.uka.ilkd.key.ocl.gf.NewCategoryMenuResult, de.uka.ilkd.key.parser.ocl.OCLPredicativeCollection, org.jmlspecs.models.JMLValueSequenceSpecs, de.uka.ilkd.key.proof.reuse.ReusePoint, de.uka.ilkd.key.rule.TacletForTests, de.uka.ilkd.key.proof.DefaultGoalChooserBuilder, de.uka.ilkd.key.proof.decproc.translation.TranslateMetavariable, de.uka.ilkd.key.parser.ocl.OCLFunctionalCollection, de.uka.ilkd.key.util.keydoc.html.Director, de.uka.ilkd.key.util.Service, de.uka.ilkd.key.proof.ProofTreeEvent, de.uka.ilkd.key.proof.decproc.DecisionProcedureSimplifyOp, de.uka.ilkd.key.ocl.gf.Utils, de.uka.ilkd.key.proof.incclosure.MultiMerger, de.uka.ilkd.key.rule.encapsulation.TypeSchemeConstraintExtractor, java.util.Locale, org.jmlspecs.models.JMLEqualsEqualsPair, de.uka.ilkd.key.strategy.feature.FindRightishFeature, de.uka.ilkd.key.logic.sort.oclsort.OclGenericSort, org.jmlspecs.models.JML_Elem_SetEnumerator, de.uka.ilkd.key.strategy.quantifierHeuristics.Instantiation, de.uka.ilkd.key.rule.encapsulation.TypeSchemeVariable, de.uka.ilkd.key.logic.op.QuanUpdateOperator, de.uka.ilkd.key.ocl.gf.TreeAnalysisResult, de.uka.ilkd.key.proof.incclosure.BufferSink, de.uka.ilkd.key.util.KeYResourceManager, de.uka.ilkd.key.proof.init.InitConfig, org.jmlspecs.models.JMLArrayOps, de.uka.ilkd.key.rule.encapsulation.TypeSchemeFalseConstraint, de.uka.ilkd.key.rule.soundness.SkolemSymbolFactory, org.jmlspecs.models.JMLValueToObjectRelation, de.uka.ilkd.key.proof.LoopInvariantProposer, de.uka.ilkd.key.rule.encapsulation.ReadonlyPrimeScheme, org.jmlspecs.models.JMLValueToEqualsRelation, de.uka.ilkd.key.ocl.gf.RefinementMenuTransformer, de.uka.ilkd.key.pp.LogicPrinter, de.uka.ilkd.key.rule.soundness.POBuilder, de.uka.ilkd.key.unittest.simplify.ast.Term, de.uka.ilkd.key.ocl.gf.GfAstNode, de.uka.ilkd.key.rule.conditions.NewJumpLabelCondition, de.uka.ilkd.key.rule.export.html.HTMLFragment, de.uka.ilkd.key.proof.mgt.RuleJustificationByAddRules, de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp, de.uka.ilkd.key.proof.mgt.GlobalProofMgt, org.jmlspecs.models.JMLObjectBag, de.uka.ilkd.key.visualization.TraceElement, de.uka.ilkd.key.strategy.feature.AbstractBetaFeature, de.uka.ilkd.key.util.pp.Printer, de.uka.ilkd.key.strategy.RuleAppContainer, de.uka.ilkd.key.proof.decproc.DecisionProcedureResult, de.uka.ilkd.key.parser.ocl.AttributeResolver, de.uka.ilkd.key.rule.conditions.NewDepOnAnonUpdates, src.LogRecord, de.uka.ilkd.key.rule.encapsulation.TypeSchemeSubConstraint, visualdebugger.VBTestRunListener, de.uka.ilkd.key.unittest.cogent.CogentResult, org.jmlspecs.models.JMLShort, de.uka.ilkd.key.ocl.gf.ReadDialog, java.io.OutputStream, de.uka.ilkd.key.parser.ocl.OCLEntity, de.uka.ilkd.key.rule.export.AbstractTacletContainer, org.jmlspecs.models.JMLMath, de.uka.ilkd.key.proof.init.Includes, de.uka.ilkd.key.util.HelperClassForTests, org.jmlspecs.models.JMLValueToEqualsRelationEnumerator, de.uka.ilkd.key.unittest.ModelGenerator, de.uka.ilkd.key.parser.IdDeclaration, de.uka.ilkd.key.strategy.termProjection.TermBuffer, visualdebugger.VBTBuilder, de.uka.ilkd.key.ocl.gf.TreeAnalyser, de.uka.ilkd.key.proof.ProblemLoader, de.uka.ilkd.key.proof.init.AbstractExecDecproc, de.uka.ilkd.key.strategy.feature.CountBranchFeature, de.uka.ilkd.key.ocl.gf.GfeditResult, de.uka.ilkd.key.rule.export.html.HTMLContainer, de.uka.ilkd.key.rule.RestrictionNone, de.uka.ilkd.key.rule.encapsulation.PeerScheme, de.uka.ilkd.key.rule.encapsulation.TypeSchemeUnion, org.jmlspecs.models.JMLValueObjectPair, org.jmlspecs.models.JMLValueToObjectRelationEnumerator, de.uka.ilkd.key.proof.mgt.DLHoareTriplePO, junit.framework.TestCase, de.uka.ilkd.key.util.make.Config, de.uka.ilkd.key.ocl.gf.Linearization, de.uka.ilkd.key.strategy.AbstractFeatureStrategy, de.uka.ilkd.key.rule.encapsulation.TypeSchemeConstraintSolver, de.uka.ilkd.key.strategy.termProjection.AbstractDividePolynomialsProjection, java.util.Arrays, de.uka.ilkd.key.strategy.TopRuleAppCost, de.uka.ilkd.key.util.pp.Layouter, de.uka.ilkd.key.ocl.gf.LinPosition, de.uka.ilkd.key.rule.soundness.MeaningFormulaBuilder, de.uka.ilkd.key.proof.init.JMLProofOblInputImpl, de.uka.ilkd.key.rule.TacletApp, de.uka.ilkd.key.strategy.feature.TernarySumFeature, de.uka.ilkd.key.pp.AbstractAsmPrinter, org.jmlspecs.models.JMLListValueNode, java.lang.Number, de.uka.ilkd.key.rule.export.TacletModelInfo, org.jmlspecs.models.JMLEqualsToEqualsRelation, de.uka.ilkd.key.parser.ocl.AxiomCollector, de.uka.ilkd.key.visualdebugger.SourceElementId, de.uka.ilkd.key.proof.decproc.translation.TranslateIfThenElse, de.uka.ilkd.key.proof.mgt.ContractUtil, de.uka.ilkd.key.pp.Range, de.uka.ilkd.key.proof.RuleSource, de.uka.ilkd.key.strategy.quantifierHeuristics.HeuristicInstantiation, java.io.StreamTokenizer, de.uka.ilkd.key.proof.decproc.ConstraintSet, de.uka.ilkd.key.ocl.gf.AstNodeData, de.uka.ilkd.key.strategy.feature.ShannonFeature, de.uka.ilkd.key.util.ObjectHashtable, de.uka.ilkd.key.proof.decproc.smtlib.Term, de.uka.ilkd.key.proof.proofevent.RuleAppInfo, de.uka.ilkd.key.speclang.FormulaWithAxioms, de.uka.ilkd.key.strategy.termfeature.ConstTermFeature, de.uka.ilkd.key.strategy.feature.instantiator.SVInstantiationCP, de.uka.ilkd.key.rule.updatesimplifier.Update, de.uka.ilkd.key.util.keydoc.html.HTMLFile, de.uka.ilkd.key.proof.InstantiationProposerCollection, de.uka.ilkd.key.ocl.gf.Hmsg, de.uka.ilkd.key.proof.init.DefaultEnvInput, de.uka.ilkd.key.unittest.TestCodeExtractor, de.uka.ilkd.key.unittest.cogent.DecisionProcedureCogent, de.uka.ilkd.key.strategy.feature.AbstractPolarityFeature, de.uka.ilkd.key.proof.mgt.AbstractContract, de.uka.ilkd.key.rule.TacletApplPart, de.uka.ilkd.key.rule.RestrictionInt, de.uka.ilkd.key.rule.BuiltInRuleApp, de.uka.ilkd.key.strategy.feature.ConstFeature, de.uka.ilkd.key.rule.AbstractIntegerRule, de.uka.ilkd.key.rule.inst.InstantiationEntry, de.uka.ilkd.key.strategy.feature.BinaryFeature, org.jmlspecs.models.JMLEqualsToObjectRelationImageEnumerator, org.jmlspecs.models.JMLEqualsToEqualsRelationImageEnumerator, de.uka.ilkd.key.strategy.SimpleFilteredStrategy, de.uka.ilkd.key.proof.TermTacletAppIndex, de.uka.ilkd.key.rule.inst.GenericSortInstantiations, de.uka.ilkd.key.util.keydoc.html.KDFilenameFilter, de.uka.ilkd.key.util.keydoc.html.BoxedFile, de.uka.ilkd.key.speclang.AbstractOperationContract, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.rule.encapsulation.TypeSchemeChecker, org.jmlspecs.models.JMLObjectSetEnumerator, org.jmlspecs.models.JMLDouble, de.uka.ilkd.key.parser.SchemaVariableModifierSet, de.uka.ilkd.key.rule.soundness.ProgramSVSkolem, de.uka.ilkd.key.util.pp.StringBackend, de.uka.ilkd.key.ocl.gf.GFCommand, de.uka.ilkd.key.rule.TacletAttributes, de.uka.ilkd.key.strategy.feature.instantiator.BackTrackingManager, de.uka.ilkd.key.proof.reuse.ReuseFrontend, java.util.Collections, de.uka.ilkd.key.strategy.termProjection.AssumptionProjection, java.util.Timer, de.uka.ilkd.key.unittest.simplify.SimplifyModelGenerator, de.uka.ilkd.key.unittest.cogent.CogentTranslation, de.uka.ilkd.key.rule.UpdateSimplificationRule, de.uka.ilkd.key.rule.encapsulation.TypeSchemeCombineTerm, de.uka.ilkd.key.strategy.feature.AgeFeature, org.jmlspecs.models.JMLEqualsToObjectRelation, de.uka.ilkd.key.strategy.termProjection.ReduceMonomialsProjection, de.uka.ilkd.key.util.install.DummyInstaller, de.uka.ilkd.key.proof.mgt.MethodContractInstantiation, de.uka.ilkd.key.proof.init.ProblemInitializer, de.uka.ilkd.key.rule.soundness.ProgramSVProxy, de.uka.ilkd.key.ocl.gf.AbstractProber, de.uka.ilkd.key.proof.VariableNameProposer, de.uka.ilkd.key.ocl.gf.Display, de.uka.ilkd.key.proof.mgt.ContractSet, junit.framework.TestSuite, de.uka.ilkd.key.proof.mgt.PrePostPair, de.uka.ilkd.key.visualdebugger.executiontree.ITNode, de.uka.ilkd.key.ocl.gf.PrintnameManager, org.jmlspecs.models.JMLObjectToValueRelationImageEnumerator, de.uka.ilkd.key.proof.decproc.AbstractDecisionProcedure, de.uka.ilkd.key.proof.decproc.NumberTranslation, org.jmlspecs.models.JMLEqualsSequenceEnumerator, de.uka.ilkd.key.proof.mgt.LemmaRuleJustification, de.uka.ilkd.key.proof.PrefixTermTacletAppIndexCache, de.uka.ilkd.key.util.KeYExceptionHandlerImpl, org.jmlspecs.models.JMLString, de.uka.ilkd.key.rule.soundness.AbstractSkolemBuilder, de.uka.ilkd.key.visualdebugger.executiontree.ETNode, de.uka.ilkd.key.strategy.quantifierHeuristics.HandleArith, de.uka.ilkd.key.proof.mgt.CvsRunner, de.uka.ilkd.key.rule.soundness.SVTypeInfo, de.uka.ilkd.key.proof.mgt.ProofEnvironment, de.uka.ilkd.key.proof.BalancedGoalChooserBuilder, de.uka.ilkd.key.rule.TacletPrefix, de.uka.ilkd.key.strategy.quantifierHeuristics.InstantiationCost, de.uka.ilkd.key.parser.ocl.AssociationResolver, de.uka.ilkd.key.rule.Taclet, de.uka.ilkd.key.visualdebugger.DebuggerEvent, de.uka.ilkd.key.proof.incclosure.Restricter, de.uka.ilkd.key.proof.decproc.smtlib.Benchmark, org.jmlspecs.models.JMLValueToEqualsRelationImageEnumerator, de.uka.ilkd.key.proof.decproc.translation.TranslateIUpdateOperator, de.uka.ilkd.key.proof.mgt.RuleConfig, org.jmlspecs.models.JMLListEqualsNode, de.uka.ilkd.key.proof.init.TacletSoundnessPOLoader, src.Client, de.uka.ilkd.key.proof.mgt.JavaModelClass, org.jmlspecs.models.JMLEqualsSet, de.uka.ilkd.key.strategy.SimpleFOLOptions, de.uka.ilkd.key.rule.NewVarcond, de.uka.ilkd.key.rule.encapsulation.UniverseAnalyser, de.uka.ilkd.key.visualization.ProofVisualization, de.uka.ilkd.key.util.make.MakefileReader, de.uka.ilkd.key.proof.ModifiesParserHelper, de.uka.ilkd.key.strategy.termfeature.RecSubTermFeature, org.jmlspecs.models.JMLObjectToEqualsRelation, de.uka.ilkd.key.unittest.TestGenerator, java.io.Writer, de.uka.ilkd.key.proof.decproc.translation.CreateTypePred, de.uka.ilkd.key.visualization.ExecutionTraceModel, de.uka.ilkd.key.proof.decproc.translation.TranslateAttributeOp, de.uka.ilkd.key.proof.decproc.translation.TranslateArrayOp, de.uka.ilkd.key.rule.inst.ProgramList, de.uka.ilkd.key.util.DesignTests, de.uka.ilkd.key.proof.proofevent.NodeReplacement, de.uka.ilkd.key.proof.Counter, org.jmlspecs.models.JMLObjectSequenceEnumerator, org.jmlspecs.models.JMLValueSetSpecs, de.uka.ilkd.key.proof.init.RuleCollection, de.uka.ilkd.key.util.keydoc.html.KeYDoc, de.uka.ilkd.key.unittest.EquivalenceClass, java.lang.Math, org.jmlspecs.models.JMLValueToValueRelationImageEnumerator, de.uka.ilkd.key.rule.inst.TacletInstantiations, de.uka.ilkd.key.strategy.feature.instantiator.OneOfCP, de.uka.ilkd.key.proof.init.OCLProofOblInput, de.uka.ilkd.key.proof.proofevent.NodeRedundantAddChange, de.uka.ilkd.key.strategy.feature.ComprehendedSumFeature, de.uka.ilkd.key.proof.OpReplacer, org.jmlspecs.models.JMLModelObjectSet, org.jmlspecs.models.JMLInteger, de.uka.ilkd.key.proof.mgt.QuantifierPrefixEntry, de.uka.ilkd.key.rule.export.TacletLoader, de.uka.ilkd.key.proof.Node, de.uka.ilkd.key.rule.export.RuleExportModel, de.uka.ilkd.key.strategy.termProjection.SubtermProjection, java.util.Date, java.util.ResourceBundle, de.uka.ilkd.key.ocl.gf.ModelExporter, de.uka.ilkd.key.pp.AbbrevMap, org.jmlspecs.models.JMLValueBagSpecs, org.jmlspecs.models.JMLObjectObjectPair, de.uka.ilkd.key.strategy.SimpleJavaCardDLOptions, de.uka.ilkd.key.rule.updatesimplifier.UpdateSimplifierTermFactory, de.uka.ilkd.key.proof.init.KeYFile, de.uka.ilkd.key.rule.export.html.HTMLLink, de.uka.ilkd.key.rule.export.html.HTMLTacletExporter, java.util.AbstractMap, de.uka.ilkd.key.proof.proofevent.NodeChangesHolder, de.uka.ilkd.key.rule.encapsulation.RepScheme, de.uka.ilkd.key.rule.metaconstruct.BreakToBeReplaced, de.uka.ilkd.key.pp.PositionTable, de.uka.ilkd.key.parser.ocl.OCLParameters, de.uka.ilkd.key.proof.proofevent.NodeChangeJournal, de.uka.ilkd.key.parser.ParserConfig, de.uka.ilkd.key.visualdebugger.DebuggerPO, de.uka.ilkd.key.proof.mgt.SpecificationRepository, de.uka.ilkd.key.rule.IfFormulaInstDirect, de.uka.ilkd.key.rule.RestrictionBool, java.util.Observable, de.uka.ilkd.key.rule.TacletPrefixBuilder, de.uka.ilkd.key.rule.inst.ProgramSVInstantiation, de.uka.ilkd.key.proof.decproc.translation.TranslateEquality, de.uka.ilkd.key.rule.NewDependingOn, java.util.Random, org.jmlspecs.models.JMLObjectToObjectRelation, de.uka.ilkd.key.logic.util.TermHelper, org.jmlspecs.models.JMLResources, de.uka.ilkd.key.proof.AndRuleFilter, de.uka.ilkd.key.unittest.simplify.ast.Function, de.uka.ilkd.key.strategy.feature.ScaleFeature, de.uka.ilkd.key.strategy.quantifierHeuristics.BasicMatching, org.jmlspecs.models.JMLEqualsObjectPair, de.uka.ilkd.key.proof.TermSVReplacer, de.uka.ilkd.key.rule.metaconstruct.arith.Monomial, de.uka.ilkd.key.proof.ProofSaver, de.uka.ilkd.key.rule.soundness.TacletPORule, de.uka.ilkd.key.proof.TermTacletAppIndexCacheSet, de.uka.ilkd.key.strategy.feature.instantiator.ForEachCP, de.uka.ilkd.key.parser.jml.JMLSpecBuilder, de.uka.ilkd.key.rule.updatesimplifier.AssignmentPairImpl, de.uka.ilkd.key.proof.NotRuleFilter, org.jmlspecs.models.JMLEqualsToEqualsRelationEnumerator, de.uka.ilkd.key.rule.RestrictionIsAttrib, de.uka.ilkd.key.proof.FormulaTag, org.jmlspecs.models.JMLChar, src.LogFile, de.uka.ilkd.key.proof.decproc.DecisionProcedureICSOp, de.uka.ilkd.key.rule.IfMatchResult, org.jmlspecs.models.JMLEqualsBagEnumerator, de.uka.ilkd.key.proof.decproc.translation.TranslateJunctor, java.io.InputStream, de.uka.ilkd.key.rule.TacletGoalTemplate, de.uka.ilkd.key.rule.updatesimplifier.GuardSimplifier, de.uka.ilkd.key.proof.ProofAggregate, de.uka.ilkd.key.logic.sort.oclsort.CollectionSort, de.uka.ilkd.key.visualdebugger.Breakpoint, org.jmlspecs.models.JMLValueSequenceEnumerator, de.uka.ilkd.key.strategy.feature.BinarySumFeature, de.uka.ilkd.key.strategy.termgenerator.SuperTermGenerator, de.uka.ilkd.key.proof.mgt.AxiomJustification, de.uka.ilkd.key.strategy.termfeature.BinaryTermFeature, java.util.Dictionary, de.uka.ilkd.key.rule.inst.ContextStatementBlockInstantiation, de.uka.ilkd.key.strategy.quantifierHeuristics.ReplacerOfQuanVariablesWithMetavariables, de.uka.ilkd.key.strategy.termProjection.SVInstantiationProjection, de.uka.ilkd.key.rule.soundness.SVTypeInfos, de.uka.ilkd.key.proof.examples.CloseProofForTrue, de.uka.ilkd.key.proof.decproc.DecProcTranslation, de.uka.ilkd.key.strategy.termProjection.FocusProjection, de.uka.ilkd.key.visualdebugger.VisualDebugger, de.uka.ilkd.key.proof.decproc.UninterpretedTermWrapper, de.uka.ilkd.key.visualdebugger.statevisualisation.SymbolicObject, de.uka.ilkd.key.strategy.FIFOStrategy, de.uka.ilkd.key.strategy.termProjection.TermConstructionProjection, java.util.Currency, de.uka.ilkd.key.ocl.gf.Printname, de.uka.ilkd.key.rule.VariableConditionAdapter, de.uka.ilkd.key.proof.init.AbstractPO, de.uka.ilkd.key.util.make.GenericParser, de.uka.ilkd.key.proof.mgt.DefaultProofCorrectnessMgt, de.uka.ilkd.key.proof.ProofTreeAdapter, java.util.EventObject, de.uka.ilkd.key.proof.decproc.translation.TranslateUnknownOp, de.uka.ilkd.key.proof.decproc.translation.TranslateProgramVariable, de.uka.ilkd.key.unittest.UnitTestBuilder, de.uka.ilkd.key.speclang.jml.JMLTranslator, de.uka.ilkd.key.proof.decproc.translation.TranslateModality, de.uka.ilkd.key.logic.op.Op, de.uka.ilkd.key.parser.ocl.FunctionFactory, de.uka.ilkd.key.rule.encapsulation.TypeSchemeAndConstraint, de.uka.ilkd.key.strategy.feature.IfThenElseMalusFeature, de.uka.ilkd.key.rule.encapsulation.ThisScheme, org.jmlspecs.models.JMLValueBagEnumerator, java.util.TimeZone, org.jmlspecs.models.JMLEqualsToValueRelation, de.uka.ilkd.key.parser.DeclPicker, java.util.Calendar, de.uka.ilkd.key.rule.encapsulation.PrimitiveScheme, de.uka.ilkd.key.proof.mgt.ProofStatus, de.uka.ilkd.key.ocl.gf.TempGrammarFiles, de.uka.ilkd.key.logic.op.SchemaVariableFactory, de.uka.ilkd.key.proof.Goal, org.jmlspecs.models.JMLObjectValuePair, de.uka.ilkd.key.rule.encapsulation.TypeSchemeEqualConstraint, java.io.Reader, de.uka.ilkd.key.visualdebugger.statevisualisation.SymbolicObjectDiagram, de.uka.ilkd.key.visualization.VisualizationModel, java.lang.Character, java.lang.Boolean, de.uka.ilkd.key.proof.init.AbstractProfile, de.uka.ilkd.key.rule.soundness.SVPartitioning, de.uka.ilkd.key.parser.ErrorHandler, de.uka.ilkd.key.strategy.feature.FindDepthFeature, de.uka.ilkd.key.strategy.termgenerator.MultiplesModEquationsGenerator, de.uka.ilkd.key.strategy.quantifierHeuristics.PredictCostProver, de.uka.ilkd.key.proof.UseMethodContractRuleFilter, org.jmlspecs.models.JMLObjectToValueRelationEnumerator, de.uka.ilkd.key.parser.ParserMode, de.uka.ilkd.key.proof.DefaultGoalChooser, de.uka.ilkd.key.strategy.quantifierHeuristics.TriggersSet, de.uka.ilkd.key.proof.init.InvariantSelectionStrategy, de.uka.ilkd.key.proof.decproc.translation.TranslateProgramMethod, de.uka.ilkd.key.strategy.quantifierHeuristics.Matching, org.jmlspecs.models.JMLInfiniteIntegerClass, org.jmlspecs.models.JMLModelValueSet, de.uka.ilkd.key.proof.init.NonInterferencePO, de.uka.ilkd.key.proof.examples.TransformProgram, de.uka.ilkd.key.proof.decproc.JavaDecisionProcedureTranslationFactory, de.uka.ilkd.key.ocl.gf.ConstraintCallback, de.uka.ilkd.key.strategy.quantifierHeuristics.TriggerUtils, de.uka.ilkd.key.proof.MethodSpecTransformation, de.uka.ilkd.key.proof.mgt.RuleJustificationInfo, de.uka.ilkd.key.proof.ProgVarReplacer, de.uka.ilkd.key.rule.UpdateSimplifier, de.uka.ilkd.key.logic.sort.oclsort.OclAnySort, de.uka.ilkd.key.strategy.termgenerator.SubtermGenerator, de.uka.ilkd.key.visualdebugger.statevisualisation.StateVisualization, de.uka.ilkd.key.strategy.quantifierHeuristics.Trigger, de.uka.ilkd.key.parser.ocl.PropertyManager, de.uka.ilkd.key.rule.conditions.JavaTypeToSortCondition, de.uka.ilkd.key.ocl.gf.MarkedAreaHighlightingStatus, org.jmlspecs.models.JMLEnumerationToIterator, visualdebugger.actions.StartVisualDebuggerAction, de.uka.ilkd.key.proof.proofevent.NodeChangeARFormula, de.uka.ilkd.key.proof.JavaModel, org.jmlspecs.models.JMLLong, java.util.BitSet, de.uka.ilkd.key.rule.conditions.TypeResolver, org.jmlspecs.models.JMLValueToValueRelationEnumerator, de.uka.ilkd.key.proof.examples.BuildProofForTrue, de.uka.ilkd.key.strategy.termfeature.SubTermFeature, de.uka.ilkd.key.rule.IfFormulaInstSeq, de.uka.ilkd.key.visualdebugger.ProofStarter, de.uka.ilkd.key.parser.SingleUpdateData, java.io.ObjectStreamClass, de.uka.ilkd.key.pp.PresentationFeatures, de.uka.ilkd.key.unittest.Model, de.uka.ilkd.key.visualdebugger.UpdateLabelListener, de.uka.ilkd.key.proof.RuleAppIndex, de.uka.ilkd.key.proof.decproc.SmtAufliaTranslation, de.uka.ilkd.key.parser.TermParserFactory, de.uka.ilkd.key.proof.init.ModifiesCheckProofOblInput, org.jmlspecs.models.JMLEqualsValuePair, de.uka.ilkd.key.strategy.termgenerator.SequentFormulasGenerator, de.uka.ilkd.key.parser.DefaultTermParser, de.uka.ilkd.key.proof.decproc.translation.TranslateFunction, org.jmlspecs.models.JMLObjectBagEnumerator, src.SaleDate, de.uka.ilkd.key.logic.op.TermSymbol, de.uka.ilkd.key.strategy.quantifierHeuristics.QuanEliminationAnalyser, de.uka.ilkd.key.logic.sort.AbstractSort, de.uka.ilkd.key.ocl.gf.GfCapsule, de.uka.ilkd.key.visualdebugger.VisualDebuggerState, org.jmlspecs.models.JMLValueEqualsPair, java.lang.Class, de.uka.ilkd.key.rule.RestrictionAtt, javacard.framework.JCSystem, de.uka.ilkd.key.rule.encapsulation.ReadonlyScheme, org.jmlspecs.models.JMLNullSafe, de.uka.ilkd.key.strategy.termfeature.ShannonTermFeature, de.uka.ilkd.key.rule.encapsulation.NullScheme, de.uka.ilkd.key.strategy.quantifierHeuristics.ClausesGraph, de.uka.ilkd.key.strategy.quantifierHeuristics.TwoSidedMatching, de.uka.ilkd.key.proof.SetRuleFilter, de.uka.ilkd.key.proof.FormulaTagManager, de.uka.ilkd.key.strategy.feature.SumFeature, de.uka.ilkd.key.proof.TacletFilter, de.uka.ilkd.key.visualization.SimpleVisualizationStrategy, de.uka.ilkd.key.proof.decproc.DecProcRunner, java.lang.ClassLoader, java.io.RandomAccessFile, org.jmlspecs.models.JMLFloat, java.io.ObjectStreamField, org.jmlspecs.models.JMLValueToObjectRelationImageEnumerator, java.util.StringTokenizer, de.uka.ilkd.key.logic.op.oclop.OclOp, de.uka.ilkd.key.parser.jml.DefaultArithOpProvider, de.uka.ilkd.key.proof.mgt.JavaModelMethod, de.uka.ilkd.key.ocl.gf.MarkedArea, de.uka.ilkd.key.pp.NotationInfo, de.uka.ilkd.key.proof.Proof, de.uka.ilkd.key.speclang.ocl.OCLTranslator, de.uka.ilkd.key.parser.ocl.BuiltInPropertyResolver, de.uka.ilkd.key.pp.Notation, de.uka.ilkd.key.rule.RuleSet, de.uka.ilkd.key.strategy.FocussedRuleApplicationManager, de.uka.ilkd.key.proof.mgt.QuantifierEliminator, org.jmlspecs.models.JMLObjectToValueRelation, org.jmlspecs.models.JMLValueValuePair, de.uka.ilkd.key.util.keydoc.html.KeYToHTMLBuilder, de.uka.ilkd.key.parser.LhsUpdateData, de.uka.ilkd.key.proof.mgt.DepAnalysis, de.uka.ilkd.key.proof.BuiltInRuleIndex, de.uka.ilkd.key.rule.export.CategoryModelInfo, de.uka.ilkd.key.strategy.termProjection.FocusFormulaProjection, de.uka.ilkd.key.unittest.ValueContainer, de.uka.ilkd.key.proof.SemisequentTacletAppIndex, de.uka.ilkd.key.strategy.feature.ConditionalFeature, de.uka.ilkd.key.rule.metaconstruct.arith.Polynomial, de.uka.ilkd.key.rule.AbstractUpdateRule, de.uka.ilkd.key.strategy.quantifierHeuristics.Substitution, org.jmlspecs.models.JMLObjectSet, de.uka.ilkd.key.strategy.termfeature.PrintTermFeature, de.uka.ilkd.key.proof.examples.BuildEmptyProof, de.uka.ilkd.key.proof.mgt.NonInterferenceCheck, de.uka.ilkd.key.proof.decproc.translation.TranslateQuantifier, de.uka.ilkd.key.rule.inst.GenericSortCondition, de.uka.ilkd.key.strategy.feature.RuleSetDispatchFeature, de.uka.ilkd.key.util.pp.WriterBackend, de.uka.ilkd.key.util.AddAHead, de.uka.ilkd.key.proof.UpdateSimplificationRuleFilter,
| Object | | public class Object (Code) | | |
| Constructor Summary | |
| public | Object()
The number of times this object has been finalized. |
| Object | | public Object()(Code) | | The number of times this object has been finalized.
|
| hashCode | | public int hashCode()(Code) | | The Class of this object. Needed to specify that invoking
getClass() on an object always produces the same result: no
methods include this model field in their assignable clause,
so no methods can alter the outcome of invoking getClass() on
some object. This property is important when using ESC/Java
on specs that use getClass(), just knowing that getClass() is
pure is not enough.
|
|
|
|