- GeneralHashFunctionLibrary - Class in fmrisc.External
-
General Purpose Hash Function Algorithms Library
http://www.partow.net/programming/hashfunctions/index.html
- GeneralHashFunctionLibrary() - Constructor for class fmrisc.External.GeneralHashFunctionLibrary
-
- generate(ParamSymbol, Map<Statement, Formula>, StateType, Name[], Name[], Vector<TheorySymbol>, Declaration[][], ErrorStream) - Static method in class fmrisc.ProgramExplorer.Tasks.PreconditionTasks
-
Construct the precondition tasks for a given method.
- generateCounterExamples(boolean) - Method in class fmrisc.ProofNavigator.Proving.CVCL.CVCL
-
generate counterexamples, if possible.
- generateCounterExamples(boolean) - Method in interface fmrisc.ProofNavigator.Proving.Prover
-
generate counterexamples, if possible.
- generateTasks(PrintWriter) - Static method in class fmrisc.ProgramExplorer.Tasks.ClassTasks
-
Generate those tasks for which the information has been previously registered.
- generateTasks(PrintWriter) - Static method in class fmrisc.ProgramExplorer.Tasks.MethodTasks
-
Generate those tasks for which the information has been previously registered.
- generateTasks(PrintWriter) - Static method in class fmrisc.ProgramExplorer.Tasks.TerminationTasks
-
Generate those tasks for which the information has been previously registered.
- get(TypeExpression[]) - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbols
-
Returns value associated to argument types.
- get(Identifier, TypeExpression[]) - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbolTable
-
Returns symbol associated to key consisting of an identifier and
a sequence of types and links key to symbol.
- get(Identifier) - Method in class fmrisc.ProgramExplorer.Semantics.SymbolTable
-
Returns symbol associated to key and links key with symbol.
- getAnalyzeImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get analyze image for cancel buttons.
- getAnnotation() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotationPosition
-
Get the annotation of the position.
- getAnnotation() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.ASTProgramAnnotated
-
Get the annotation for this item.
- getAnnotation() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ASTProgramAnnotatedBase
-
Get the annotation for this item.
- getAnnotation() - Method in class fmrisc.ProgramExplorer.Syntax.Program.DeclarationBase
-
Get the annotation for this item.
- getAnnotation() - Method in class fmrisc.ProgramExplorer.Syntax.Program.StatementBase
-
Get the annotation for this item.
- getAnnotation() - Method in class fmrisc.ProgramExplorer.Syntax.Program.TopDeclarationBase
-
Get the annotation for this item.
- getAnnotationColumn() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotationPosition
-
Get the annotation column number of the position.
- getAnnotationLine() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotationPosition
-
Get the annotation number of the position.
- getArgument() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PostfixApplication
-
Get the argument.
- getArgument() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PostfixFormula
-
Get the argument.
- getArgument() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PostfixTerm
-
Get the argument.
- getArgumentExpressions() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ApplicationExpression
-
Get the argument expressions.
- getArguments() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TermApplication
-
Get the arguments.
- getArguments() - Method in class fmrisc.ProofNavigator.Syntax.ApplicationExpression
-
get arguments
- getArgumentTypes() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get the argument types of the entity
- getAssertion() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.StatementSpec
-
Get pre-state assertion.
- getAssumption(String) - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
returns assumption with denoted label
- getAssumptions() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
get assumptions of proof state
- getAxiom() - Method in class fmrisc.ProofNavigator.Syntax.ArrayTerm
-
Get declaration of axiom replacing expression
- getAxioms() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
get axioms of proof state
- getBackgroundColor() - Method in class fmrisc.ProgramExplorer.SWT.MainSWT
-
Get background color.
- getBackgroundColor() - Static method in class fmrisc.ProofNavigator.SWT.MainSWT
-
Get background color.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ArrayType
-
Get base type.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.RecordTerm
-
Get base terms.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.RecordType
-
Get named base types.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.SelectionTerm
-
Get base term.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.SubType
-
Returns (non-subtype) base type.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TupleTerm
-
Get base terms.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TupleType
-
Get base types.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.UnaryExpression
-
Get base expression.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.UnaryFormula
-
Get base formula.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.UnaryTerm
-
Get base term.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.UpdateTerm
-
Get base term.
- getBase() - Method in class fmrisc.ProgramExplorer.Syntax.Name
-
Get the base identifier of the name.
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.ArrayType
-
returns base type
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.LetExpression
-
get base expression
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.LetType
-
get base type
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.QuantifiedExpression
-
get base expression
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.RecordTerm
-
returns base terms
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.RecordType
-
returns base types
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.SelectionTerm
-
get base expression
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.SubType
-
returns base type
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.TupleTerm
-
get base expressions
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.TupleType
-
returns base types
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.UnaryExpression
-
Returns base expression
- getBase() - Method in class fmrisc.ProofNavigator.Syntax.UpdateTerm
-
get the base expression
- getBaseName(String) - Static method in class fmrisc.ProofNavigator.Syntax.ASTUtil
-
Get base name from name.
- getBaseName(String) - Static method in class fmrisc.ProofNavigator.Syntax.UniqueNameTable
-
Get base name from name.
- getBaseTheory() - Method in class fmrisc.ProgramExplorer.Semantics.TypeTranslator
-
Get the base theory symbol.
- getBaseType() - Method in class fmrisc.ProgramExplorer.Syntax.Program.SelectorExpression
-
Get type of base expression.
- getBitType() - Static method in class fmrisc.ProofNavigator.Semantics.Checking
-
Get canonical type BIT
- getBlackColor() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get color black.
- getBody() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ArrayTerm
-
Get the body of the term.
- getBody() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LambdaFormula
-
Get the body of the term.
- getBody() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LambdaTerm
-
Get the body of the term.
- getBody() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LetExpression
-
Get body.
- getBody() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LetFormula
-
Get body.
- getBody() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LetTerm
-
Get body.
- getBody() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.QuantifiedExpression
-
Get body of expression.
- getBody() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.QuantifiedFormula
-
Get the body of the formula.
- getBody() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.ParamDeclaration
-
Get body of declaration.
- getBody() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ParamDeclarationBase
-
Get body of declaration.
- getBodyJudgement() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get body statement judgement.
- getBooleanType() - Static method in class fmrisc.ProofNavigator.Semantics.Checking
-
Get canonical type BOOLEAN
- getBrowser() - Method in class fmrisc.ProgramExplorer.SWT.BrowserWindow
-
Get browser from window.
- getCall() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get the set of methods called by this method.
- getCancelImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get image for cancel buttons.
- getChildren() - Method in class fmrisc.ProgramExplorer.InOut.Breaks.Info
-
Get the children information.
- getChildren() - Method in class fmrisc.ProofNavigator.Communication.BreakInfo
-
Get the children of this node.
- getChildren() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
get children of proof state
- getClass(Name) - Method in class fmrisc.ProgramExplorer.Semantics.Environment
-
Return symbol for class denoted by name in current environment.
- getClasses() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get set of classes held by package.
- getClassImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get class image.
- getClassInvariant() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.ClassSpec
-
Get class invariant.
- getClassMethodImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get class method image.
- getClassMethods() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get set of class methods of this class.
- getClassMethodSet() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get set of class methods of this class.
- getClassSet() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get set of classes held by package as collection.
- getClassSpec() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ClassDeclaration
-
Get class specification
- getClassSymbol() - Method in class fmrisc.ProgramExplorer.Semantics.GlobalVariableSymbolBase
-
Get the class to which the variable belongs.
- getClassSymbol() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get the class to which the entity belongs.
- getClassSymbol() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Returns class from which theory is derived (if any).
- getClassSymbol() - Method in class fmrisc.ProgramExplorer.Semantics.ThisSymbol
-
Get the class of this symbol.
- getClassSymbols(Name[]) - Static method in class fmrisc.ProgramExplorer.Syntax.NameUtils
-
Get set of class symbols denoted by names.
- getClassTheory() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get theory symbol holding the logical type declaration for this class.
- getClassTheory(ErrorStream) - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get theory symbol holding the logical type declaration for this class.
- getClassVariables() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get set of class values of this class.
- getClassVariables() - Method in class fmrisc.ProgramExplorer.Semantics.Environment
-
Get currently visible class variables.
- getClassVariableSet() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get set of class values of this class.
- getClassVarImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get class variable image.
- getClearType() - Method in class fmrisc.ProofNavigator.Semantics.ValueSymbol
-
Get clear type.
- getClosedColor() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get color for closed tasks.
- getClosedColor() - Static method in class fmrisc.ProofNavigator.SWT.MainSWT
-
Get color for closed proof tree nodes.
- getColumn() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotationPosition
-
Get the column number of the position.
- getColumn() - Method in interface fmrisc.ProgramExplorer.InOut.SourcePosition
-
Get the column number of the position.
- getColumn() - Method in class fmrisc.ProgramExplorer.InOut.SourcePositionClass
-
Get the column number of the position.
- getColumn() - Method in class fmrisc.ProgramExplorer.InOut.StringSourcePosition
-
Get the column number of the position.
- getCommand() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
get command of proof state
- getCommandServerPort() - Method in class fmrisc.ProgramExplorer.SWT.MainSWT
-
Get port of command server.
- getCondition() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseExpression
-
Get condition.
- getCondition() - Method in class fmrisc.ProofNavigator.Syntax.IfThenElseExpression
-
get condition of expression
- getConsole() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get console output writer.
- getConstant() - Method in class fmrisc.ProofNavigator.Syntax.ArrayTerm
-
Get declaration of constant replacing expression
- getConstructor(CallStatement, TypeExpression[]) - Method in class fmrisc.ProgramExplorer.Semantics.Environment
-
Return symbol for constructor denoted by name and argument types
in current environment.
- getConstructorImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get constructor image.
- getConstructors() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get set of constructors of this class.
- getConstructorSet() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get set of constructors of this class.
- getContext() - Static method in class fmrisc.ProofNavigator.State
-
get context used by proof navigator
- getContextDir() - Static method in class fmrisc.ProofNavigator.State
-
Get current context directory.
- getCounterExample() - Method in class fmrisc.ProofNavigator.Proving.CVCL.InvalidAnswerCVCL
-
Interpret justification as a counterexample.
- getCounterExample() - Method in class fmrisc.ProofNavigator.Proving.InvalidAnswer
-
Interpret justification as a counterexample.
- getCounterExample() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
Get counterexample for state.
- getCurrent() - Method in class fmrisc.ProofNavigator.Proving.Proof
-
get current open proof state
- getCurrentColor() - Static method in class fmrisc.ProofNavigator.SWT.MainSWT
-
Get color for current proof node.
- getCurrentMenu() - Method in class fmrisc.ProofNavigator.SWT.Top
-
Get menu bar
- getCurrentMethod() - Method in class fmrisc.ProgramExplorer.Semantics.Environment
-
Get symbol of current method.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.AxiomSymbol
-
Get declaration.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.BodySymbol
-
Get declaration of variable.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.ClassMethodSymbol
-
Get declaration of method.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get the declaration of the class.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.ClassVariableSymbol
-
Return declaration associated to symbol.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.ConstructorSymbol
-
Get declaration of method.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.FormulaSymbol
-
Get declaration.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.ObjectMethodSymbol
-
Get declaration of method.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.ObjectVariableSymbol
-
Return declaration associated to symbol.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.ParameterSymbol
-
Get the declaration of this parameter.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get declaration associated to symbol (may be null).
- getDeclaration() - Method in interface fmrisc.ProgramExplorer.Semantics.Symbol
-
Get declaration of variable (if any).
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.SymbolBase
-
Get declaration of variable (if any).
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get the declaration of the theory.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.TypeSymbol
-
Get declaration.
- getDeclaration() - Method in class fmrisc.ProgramExplorer.Semantics.ValueSymbol
-
Get declaration.
- getDeclarations() - Method in class fmrisc.ProgramExplorer.Proving.ClassicalProblem
-
Get the declarations.
- getDeclarations() - Method in class fmrisc.ProgramExplorer.Semantics.LogicEnvironment
-
Get sequence of ordered declarations sequences where declarations in a
later sequence supersede the previous declarations.
- getDeclarations() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.TheoryDeclaration
-
Get declarations introduced in unit.
- getDeclarations() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.UnitSpec
-
Get declarations introduced in unit.
- getDeclarations() - Method in class fmrisc.ProofNavigator.Syntax.LetExpression
-
get declarations
- getDeclarations() - Method in class fmrisc.ProofNavigator.Syntax.LetType
-
get declarations
- getDeclFile() - Method in class fmrisc.ProofNavigator.Communication.Presenter
-
Get file where all declarations are stored
- getDefinitions() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LetExpression
-
Get definitions.
- getDefinitions() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LetFormula
-
Get definitions.
- getDefinitions() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LetTerm
-
Get definitions.
- getDelegates() - Method in class fmrisc.ProgramExplorer.Parser.MiniJavaLexer
-
- getDelegates() - Method in class fmrisc.ProgramExplorer.Parser.MiniJavaParser
-
- getDeleteImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get delete image.
- getDepth() - Method in class fmrisc.ProgramExplorer.Semantics.TCCGenerator
-
Return depth of context stack.
- getDepth() - Method in class fmrisc.ProofNavigator.Semantics.ValueSymbol
-
Return environment depth of symbol.
- getDetailImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get detail image.
- getDigits() - Method in class fmrisc.ProofNavigator.Syntax.Number
-
get digit representation of number
- getDirectory() - Method in interface fmrisc.ProgramExplorer.Tasks.Task
-
Get directory to be used for writing persistent data
- getDirectory() - Method in class fmrisc.ProgramExplorer.Tasks.TaskBase
-
Get directory to be used for writing persistent data
- getDisplay() - Method in class fmrisc.ProgramExplorer.SWT.MainSWT
-
Get the display of this GUI.
- getDivergesCondition() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.MethodSpec
-
Get method diverges condition.
- getDomain() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.FunctionType
-
Get domain types.
- getDomain() - Method in class fmrisc.ProofNavigator.Syntax.FunctionType
-
returns domain of type
- getElseBranch() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseExpression
-
Get "else" branch.
- getElseBranch() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseFormula
-
Get "else" branch.
- getElseBranch() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseTerm
-
Get "else" branch.
- getElseBranch() - Method in class fmrisc.ProofNavigator.Syntax.IfThenElseExpression
-
get else branch of expression
- getEnvironment() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
get environment of proof state
- getEnvironment() - Method in class fmrisc.ProofNavigator.Semantics.FormulaSymbol
-
Return environment of symbol (up to the point where the symbol was decld).
- getEnvironment() - Static method in class fmrisc.ProofNavigator.State
-
get environment used by proof navigator
- getError() - Static method in class fmrisc.ProgramExplorer.Main
-
Get error stream for printing error messages.
- getError() - Method in class fmrisc.ProofNavigator.Proving.CVCL.CVCL
-
error message, if CVCL instance is not okay
- getError() - Method in interface fmrisc.ProofNavigator.Proving.Prover
-
error message, if last command signalled a problem
- getError() - Static method in class fmrisc.ProofNavigator.State
-
get error message set
- getErrorHeader(RecognitionException) - Method in class fmrisc.ProgramExplorer.Parser.MiniJavaLexer
-
- getErrorHeader(RecognitionException) - Method in class fmrisc.ProgramExplorer.Parser.MiniJavaParser
-
- getErrorHeader(RecognitionException) - Method in class fmrisc.ProgramExplorer.Parser.SpecLangLexer
-
- getErrorHeader(RecognitionException) - Method in class fmrisc.ProgramExplorer.Parser.SpecLangParser
-
- getErrorImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get error image.
- getErrorNumber() - Method in class fmrisc.ProgramExplorer.InOut.ErrorStream
-
Return the number of errors generated.
- getEvidence() - Method in interface fmrisc.ProgramExplorer.Tasks.Task
-
Get evidence for task status.
- getEvidence() - Method in class fmrisc.ProgramExplorer.Tasks.TaskBase
-
Get evidence for task status.
- getException() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.StateThrowsException
-
Get the name of the exception.
- getExceptions() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.MethodSpec
-
Get list of exceptions that may be thrown by method.
- getExpression() - Method in class fmrisc.ProofNavigator.Proving.Formula
-
Get formula expression.
- getExpression() - Method in class fmrisc.ProofNavigator.Semantics.TypeExpression
-
get exp
- getExpressionLogic() - Method in class fmrisc.ProgramExplorer.Judgements.Satisfies
-
Get expression translator of this judgement processor
- getExpressions() - Method in class fmrisc.ProofNavigator.Proving.GroundExpressions
-
Get the collection of ground expressions collected in this set.
- getExternalName(ValueDeclIdentifier) - Static method in class fmrisc.ProofNavigator.Proving.CVCL.CVCL
-
create CVCL identifier from given name
- getFile() - Method in class fmrisc.ProgramExplorer.InOut.Source
-
Get the file denoting the source.
- getFile(ProofState) - Method in class fmrisc.ProofNavigator.Communication.Presenter
-
Construct file name for proof state
- getFileImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get image for generic files.
- getFileStack() - Static method in class fmrisc.ProofNavigator.State
-
Get file stack.
- getFirst() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BinaryAtomicFormula
-
Get first subterm.
- getFirst() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BinaryExpression
-
Get first subexpression.
- getFirst() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BinaryFormula
-
Get first subformula.
- getFirst() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BinaryTerm
-
Get first subterm.
- getFirst() - Method in class fmrisc.ProofNavigator.Syntax.BinaryExpression
-
Returns first subexpression
- getFolderImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get image for folders.
- getFolderProcessImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get process folder image.
- getFolders() - Method in class fmrisc.ProgramExplorer.Tasks.TaskFolder
-
Get subfolders appropriately sorted for display.
- getFontSize() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get current font size.
- getFormula() - Method in class fmrisc.ProgramExplorer.Semantics.FormulaSymbol
-
Get formula.
- getFormula() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ValueDeclarationFormula
-
Get value of the declaration.
- getFormula(Identifier) - Method in class fmrisc.ProofNavigator.Proving.CVCL.CVCLFormulaMask
-
Get formula associated to mask identifier
- getFormula(String) - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
returns formula (assumption or goal) with denoted label
- getFormula() - Method in class fmrisc.ProofNavigator.Semantics.Context
-
return the formula currently on the top of the stack
- getFormula() - Method in class fmrisc.ProofNavigator.Semantics.FormulaSymbol
-
Return formula of symbol.
- getFormula(Identifier) - Method in class fmrisc.ProofNavigator.Semantics.FormulaTable
-
returns formula associated to key
- getFormula() - Method in class fmrisc.ProofNavigator.Syntax.FormulaDeclaration
-
returns declaration formula
- getFormulaDeclIdentifier() - Method in class fmrisc.ProofNavigator.Semantics.FormulaSymbol
-
Return identifier of symbol.
- getFormulaDeclIdentifier() - Method in class fmrisc.ProofNavigator.Syntax.FormulaDeclaration
-
returns declaration name
- getFormulaImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get formula image.
- getFormulaMask() - Static method in class fmrisc.ProofNavigator.State
-
Get formula mask.
- getFormulas() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get set of formulas of this class.
- getFormulaSymbol(Identifier) - Method in class fmrisc.ProgramExplorer.Semantics.LogicEnvironment
-
Returns formula symbol associated to name.
- getFormulaSymbol(Identifier) - Method in class fmrisc.ProofNavigator.Semantics.Environment
-
returns symbol associated to name (null, if none)
- getFormulaSymbols() - Method in class fmrisc.ProgramExplorer.Semantics.LogicEnvironment
-
Get all formula symbols.
- getFormulaSymbols() - Method in class fmrisc.ProofNavigator.Semantics.Environment
-
Get all formula symbols.
- getFormulaTasks() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get the formula tasks.
- getFree() - Method in class fmrisc.ProofNavigator.Syntax.ArrayTerm
-
Get free variables
- getFrom() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.SubrangeType
-
Get lower bound.
- getFrom() - Method in class fmrisc.ProofNavigator.Syntax.SubrangeType
-
returns lower bound
- getFunction() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TermApplication
-
Get the function.
- getFunction() - Method in class fmrisc.ProofNavigator.Syntax.ApplicationExpression
-
get function/predicate
- getFunctionExpression() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ApplicationExpression
-
Get the expression that is applied.
- getGlobal() - Static method in class fmrisc.ProofNavigator.State
-
get global environment of proof navigator
- getGlobalValueSymbols() - Method in class fmrisc.ProofNavigator.Semantics.Environment
-
Get global value symbols in the order in which they were entered.
- getGoal() - Method in class fmrisc.ProgramExplorer.Proving.ClassicalProblem
-
Get the goal.
- getGoal(String) - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
returns goal with denoted label
- getGoals() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
get goals of proof state
- getGrammarFileName() - Method in class fmrisc.ProgramExplorer.Parser.MiniJavaLexer
-
- getGrammarFileName() - Method in class fmrisc.ProgramExplorer.Parser.MiniJavaParser
-
- getGrammarFileName() - Method in class fmrisc.ProgramExplorer.Parser.SpecLangLexer
-
- getGrammarFileName() - Method in class fmrisc.ProgramExplorer.Parser.SpecLangParser
-
- getGrammarFileName() - Method in class fmrisc.ProofNavigator.PN2Lexer
-
- getGrammarFileName() - Method in class fmrisc.ProofNavigator.PN2Parser
-
- getHostClass() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get the class for which this theory is local.
- getIdent() - Method in class fmrisc.ProofNavigator.Commands.Prove
-
get name of formula to be proved
- getIdentifier() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotationPosition
-
Get identifier registered with denoted position.
- getIdentifier() - Method in interface fmrisc.ProgramExplorer.InOut.SourcePosition
-
Get identifier registered with denoted position.
- getIdentifier() - Method in class fmrisc.ProgramExplorer.InOut.SourcePositionClass
-
Get identifier registered with denoted position.
- getIdentifier() - Method in class fmrisc.ProgramExplorer.InOut.StringSourcePosition
-
Get identifier registered with denoted position.
- getIdentifier() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PostfixApplication
-
Get the function.
- getIdentifier() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.SelectorIdentifier
-
Get identifier.
- getIdentifier() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ValuedIdentifier
-
Get identifier.
- getIdentifier() - Method in interface fmrisc.ProofNavigator.Semantics.Symbol
-
Get identifier associated to symbol.
- getIdentifier() - Method in class fmrisc.ProofNavigator.Semantics.SymbolBase
-
get identifier associated to symbol
- getIdentifier() - Method in interface fmrisc.ProofNavigator.Syntax.Declaration
-
Returns declaration name.
- getIdentifier() - Method in class fmrisc.ProofNavigator.Syntax.FormulaDeclaration
-
returns declaration name
- getIdentifier() - Method in class fmrisc.ProofNavigator.Syntax.SelectorIdentifier
-
return identifier
- getIdentifier() - Method in class fmrisc.ProofNavigator.Syntax.TypeDeclaration
-
returns declaration name
- getIdentifier() - Method in class fmrisc.ProofNavigator.Syntax.TypedIdentifier
-
returns identifier name
- getIdentifier() - Method in class fmrisc.ProofNavigator.Syntax.ValueDeclaration
-
returns declaration name
- getIdentifier() - Method in class fmrisc.ProofNavigator.Syntax.ValuedIdentifier
-
returns identifier
- getImports() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.CompilationUnit
-
Get import statements of unit
- getImports() - Method in class fmrisc.ProgramExplorer.Syntax.Program.CompilationUnitBase
-
Get import statements of unit
- getImports() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.UnitSpec
-
Get imports used by unit.
- getIndex() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ArrayType
-
Get index type.
- getIndex() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.SelectorIndex
-
Get index.
- getIndex() - Method in class fmrisc.ProofNavigator.Syntax.ArrayType
-
returns index type
- getIndex() - Method in class fmrisc.ProofNavigator.Syntax.SelectorIndex
-
get index expression
- getInfo() - Method in interface fmrisc.ProgramExplorer.Tasks.Task
-
Get additional information for task status.
- getInfo() - Method in class fmrisc.ProgramExplorer.Tasks.TaskBase
-
Get additional information for task status.
- getInitFormula() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get the formula representing the initial values of the object variables.
- getIntType() - Static method in class fmrisc.ProofNavigator.Semantics.Checking
-
Get canonical type INT
- getJudgement() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.Statement
-
Get command judgement.
- getJudgement() - Method in class fmrisc.ProgramExplorer.Syntax.Program.StatementBase
-
Get command judgement.
- getJudgement() - Method in class fmrisc.ProgramExplorer.Syntax.Program.VariableStatement
-
Get command judgement.
- getJustification() - Method in interface fmrisc.ProofNavigator.Proving.Answer
-
Return justification of answer suitable for printing.
- getJustification() - Method in class fmrisc.ProofNavigator.Proving.AnswerBase
-
Return justification of answer suitable for printing.
- getKeyword() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PostVariable
-
Get string representation of keyword.
- getKeyword() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PreVariable
-
Get string representation of keyword.
- getKeyword() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ProgramVariableBase
-
Get string representation of keyword.
- getKeyword() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ReadsOnlyFormula
-
Get string representation of keyword.
- getKeyword() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.WritesOnlyFormula
-
Get string representation of keyword.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.AssertionStatement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.AssignmentStatement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.BlockStatement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.BreakStatement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.CallStatement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ConditionalStatement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ContinueStatement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.EmptyStatement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ForLoopStatement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ReturnStatement
-
Get type of statement.
- getKind() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.Statement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.TryCatchStatement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.VariableStatement
-
Get type of statement.
- getKind() - Method in class fmrisc.ProgramExplorer.Syntax.Program.WhileLoopStatement
-
Get type of statement.
- getLabel() - Method in class fmrisc.ProofNavigator.Proving.Formula
-
get formula label
- getLabel() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
return label of proof state
- getLabels() - Static method in class fmrisc.ProofNavigator.State
-
ask whether lexer shall produce labels rather than idents
- getLastTCC() - Static method in class fmrisc.ProofNavigator.State
-
get last type checking condition
- getLength() - Method in class fmrisc.ProgramExplorer.InOut.Breaks.Info
-
Get the length of the linear representation (children included).
- getLength(int, int) - Method in class fmrisc.ProgramExplorer.InOut.Source
-
Get number of characters from current position to end of line.
- getLength() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotationPosition
-
Get number of characters from current position to end of line.
- getLength() - Method in interface fmrisc.ProgramExplorer.InOut.SourcePosition
-
Get number of characters from current position to end of line.
- getLength() - Method in class fmrisc.ProgramExplorer.InOut.SourcePositionClass
-
Get number of characters from current position to end of line.
- getLength() - Method in class fmrisc.ProgramExplorer.InOut.StringSourcePosition
-
Get number of characters from current position to end of line.
- getLength() - Method in class fmrisc.ProgramExplorer.Syntax.Name
-
Get the length of the name.
- getLength() - Method in class fmrisc.ProofNavigator.Communication.BreakInfo
-
Get the total length of the linear representation of the tree.
- getLexer() - Static method in class fmrisc.ProofNavigator.State
-
get lexer used by proof navigator
- getLine(int) - Method in class fmrisc.ProgramExplorer.InOut.Source
-
Get a line from the source.
- getLine(int) - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotation
-
Get a line from the annotation.
- getLine() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotationPosition
-
Get the line number of the position.
- getLine() - Method in interface fmrisc.ProgramExplorer.InOut.SourcePosition
-
Get the line number of the position.
- getLine() - Method in class fmrisc.ProgramExplorer.InOut.SourcePositionClass
-
Get the line number of the position.
- getLine() - Method in class fmrisc.ProgramExplorer.InOut.StringSourcePosition
-
Get the line number of the position.
- getLine(int) - Method in class fmrisc.ProgramExplorer.Parser.SpecLangParser
-
- getLines() - Method in class fmrisc.ProgramExplorer.InOut.Source
-
Get number of lines of source.
- getLines() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotation
-
Get the number of lines of the annotation.
- getListener() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
Get listener that is notified when proof state has changed.
- getLocalTheory() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get theory symbol holding the local declaration for this class.
- getLocalVariables() - Method in class fmrisc.ProofNavigator.Semantics.Environment
-
get local variables (all values with environment depth gt 0)
- getLogicBaseType() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.Selector
-
get logic type of expression to which selector is applied
- getLogicBaseType() - Method in class fmrisc.ProgramExplorer.Syntax.Program.SelectorBase
-
get type of expression to which selector is applied
- getLogicEnvironment() - Method in class fmrisc.ProgramExplorer.Semantics.LogicChecking
-
Get the environment for looking up logic symbols.
- getLogicReturnType() - Method in class fmrisc.ProgramExplorer.Semantics.MethodSymbol
-
Get logic return type of the method.
- getLogicType() - Method in interface fmrisc.ProgramExplorer.Semantics.VariableSymbol
-
Get logic type of symbol.
- getLogicType() - Method in class fmrisc.ProgramExplorer.Semantics.VariableSymbolBase
-
Get logic type of symbol.
- getLogicTypeTable() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get logic type table of package.
- getLogicTypeTable() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get type table of class.
- getLongName() - Method in interface fmrisc.ProgramExplorer.Semantics.GlobalSymbol
-
Get the unique long name by which the symbol can be referenced.
- getLongName() - Method in class fmrisc.ProgramExplorer.Semantics.GlobalSymbolBase
-
Get the unique long name by which the symbol can be referenced.
- getLongName() - Method in class fmrisc.ProgramExplorer.Semantics.GlobalVariableSymbolBase
-
Get the unique long name by which the symbol can be referenced.
- getLoopAnnotation() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.LoopStatement
-
Get the loop annotation for this item.
- getLoopAnnotation() - Method in class fmrisc.ProgramExplorer.Syntax.Program.LoopStatementBase
-
Get the loop annotation for this item.
- getLoopInvariant() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.LoopSpec
-
Get loop invariant.
- getLoops() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get the loops.
- getMask(Expression) - Method in class fmrisc.ProofNavigator.Proving.CVCL.CVCLFormulaMask
-
Mask a formula.
- getMethod(CallStatement, TypeExpression[]) - Method in class fmrisc.ProgramExplorer.Semantics.Environment
-
Return symbol for a method called with arguments of denoted types
in current environment and annotate call with symbol.
- getMethodSymbol() - Method in class fmrisc.ProgramExplorer.Syntax.Program.CallStatement
-
Get symbol of called method.
- getName() - Method in interface fmrisc.ProgramExplorer.Semantics.Symbol
-
Get name associated to symbol.
- getName() - Method in class fmrisc.ProgramExplorer.Semantics.SymbolBase
-
Get name associated to symbol.
- getName() - Method in interface fmrisc.ProgramExplorer.Syntax.Declaration
-
Get the name of the declared entity.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.AtomicType
-
Get type name.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BitFalse
-
Get name of constant.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BitTrue
-
Get name of constant.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BitType
-
Get name of constant.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BooleanType
-
Get name of constant.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.Constant
-
Get name of constant.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.DeclarationBase
-
Get the name of the declared entity.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.False
-
Get name of constant.
- getName() - Method in interface fmrisc.ProgramExplorer.Syntax.Logic.ProgramVariable
-
Get name of variable.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ProgramVariableBase
-
Get name of variable.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.Reference
-
Get name of the variable.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.True
-
Get name of constant.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TypedIdentifier
-
Get identifier.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Program.DeclarationBase
-
Get the name of the declared entity.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Program.DeclCallStatement
-
Get the name of the declared entity.
- getName() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.Import
-
Get the name denoted by the import statement.
- getName() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ImportBase
-
Get the name denoted by the import statement.
- getName() - Method in interface fmrisc.ProgramExplorer.Tasks.Task
-
Get the name of the task.
- getName() - Method in class fmrisc.ProgramExplorer.Tasks.TaskBase
-
Get name of task.
- getName() - Method in class fmrisc.ProofNavigator.Commands.CommandBase
-
get name of command
- getName() - Method in class fmrisc.ProofNavigator.Syntax.AtomicType
-
returns name of identifier
- getName() - Method in class fmrisc.ProofNavigator.Syntax.Identifier
-
returns name of identifier
- getNames(Collection<TheorySymbol>) - Static method in class fmrisc.ProgramExplorer.Syntax.NameUtils
-
Get names of symbols.
- getNamespacePrefix() - Method in class fmrisc.External.NewOMDOMWriter
-
Get the namespace prefix.
- getNatType() - Static method in class fmrisc.ProofNavigator.Semantics.Checking
-
Get canonical type NAT
- getNumber() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.SelectorNumber
-
Get identifier.
- getNumber() - Method in class fmrisc.ProofNavigator.Syntax.SelectorNumber
-
get the base number
- getObjectMethodImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get object method image.
- getObjectMethods() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get set of object methods of this class.
- getObjectMethodSet() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get set of object methods of this class.
- getObjectVariables() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get set of object values of this class.
- getObjectVariables() - Method in class fmrisc.ProgramExplorer.Semantics.Environment
-
Get currently visible object variables.
- getObjectVariableSet() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get set of object values of this class.
- getObjectVarImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get object variable image.
- getObligations() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get the other proof obligations.
- getOffset(int, int) - Method in class fmrisc.ProgramExplorer.InOut.Source
-
Get offset of denoted position
- getOffset() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotationPosition
-
Get offset of the position.
- getOffset() - Method in interface fmrisc.ProgramExplorer.InOut.SourcePosition
-
Get offset of denoted position
- getOffset() - Method in class fmrisc.ProgramExplorer.InOut.SourcePositionClass
-
Get offset of denoted position
- getOffset() - Method in class fmrisc.ProgramExplorer.InOut.StringSourcePosition
-
Get offset of denoted position
- getOkayImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get image for okay buttons.
- getOpenColor() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get color for open tasks.
- getOpenColor() - Static method in class fmrisc.ProofNavigator.SWT.MainSWT
-
Get color for open proof tree nodes.
- getOpenGoal() - Method in class fmrisc.ProofNavigator.Proving.Proof
-
get open leaf goal
- getOpenGoals() - Method in class fmrisc.ProofNavigator.Proving.Proof
-
get open leaf goals
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.AndFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BinaryExpression
-
Get string representation of (outmost) operator the expression.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BitAndTerm
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BitNegationTerm
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BitOrTerm
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.DividesTerm
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.EqualsFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.EquivalentFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.GreaterEqualFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.GreaterFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ImpliesFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LessEqualFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LessFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.MinusTerm
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.NegationTerm
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.NotEqualsFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.NotEquivalentFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.NotFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.OrFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PlusTerm
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PowerTerm
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.SimilarFormula
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TimesTerm
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.UnaryExpression
-
Get string representation of (outmost) operator the expression.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.AndExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.BinaryValueExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.DividesExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.EqualsExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.GreaterEqualExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.GreaterExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.LessEqualExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.LessExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.MinusExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.NegationExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.NotEqualsExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.NotExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.OrExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.PercentExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.PlusExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.TimesExpression
-
Get textual representation of operator.
- getOperator() - Method in class fmrisc.ProgramExplorer.Syntax.Program.UnaryValueExpression
-
Get textual representation of operator.
- getOptional() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get the optional conditions.
- getOriginalName(String) - Method in class fmrisc.ProofNavigator.Proving.CVCL.CVCL
-
Get original name from external CVCL name.
- getPackage() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get package of class.
- getPackage(Name) - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Return symbol for package denoted by name in current package;
an error message is printed if the lookup fails.
- getPackage(Name, boolean) - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Return symbol for package denoted by name in current package.
- getPackage() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get package of theory.
- getPackage() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.CompilationUnit
-
Get package name of unit
- getPackage() - Method in class fmrisc.ProgramExplorer.Syntax.Program.CompilationUnitBase
-
Get package name of unit
- getPackageImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get package image.
- getPackages() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get set of packages held by package.
- getPackageSet() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get set of packages held by package as collection.
- getParameterArray() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get array of parameters of this object.
- getParameterImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get parameter image.
- getParams() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get the method's parameter set.
- getParams() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.ParamDeclaration
-
Get parameters of declaration.
- getParams() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ParamDeclarationBase
-
Get parameters of declaration.
- getParamSymbol() - Method in class fmrisc.ProgramExplorer.Semantics.ParameterSymbol
-
Get the entity to which the variable belongs.
- getParent() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get parent package.
- getParent() - Method in interface fmrisc.ProgramExplorer.Tasks.Task
-
Get folder containing current task.
- getParent() - Method in class fmrisc.ProgramExplorer.Tasks.TaskBase
-
Get parent folder
- getParent() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
get parent of proof state
- getParentDirectory() - Method in class fmrisc.ProgramExplorer.Tasks.TaskBase
-
Get parent directory
- getPath() - Static method in class fmrisc.ProgramExplorer.Main
-
Get path for looking up source files.
- getPath() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
get path of proof state
- getPortNumber() - Method in class fmrisc.ProgramExplorer.InOut.CommandServer
-
Get port number on which server is listening.
- getPortNumber() - Method in class fmrisc.ProgramExplorer.InOut.VirtualDirectoryServer
-
Get port number on which server is listening.
- getPortNumber() - Method in class fmrisc.ProofNavigator.Communication.CommandServer
-
Get port number on which server is listening.
- getPosition() - Method in class fmrisc.ProgramExplorer.InOut.ErrorStream
-
Get current source position.
- getPosition() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotation
-
Get the source position of the annotation.
- getPosition() - Method in class fmrisc.ProgramExplorer.Parser.MiniJavaParser
-
- getPosition(Token) - Method in class fmrisc.ProgramExplorer.Parser.SpecLangParser
-
- getPosition() - Method in class fmrisc.ProgramExplorer.Parser.SpecLangParser
-
- getPosition() - Method in interface fmrisc.ProgramExplorer.Syntax.ASTSource
-
Get the position of this statement in the source code.
- getPosition() - Method in class fmrisc.ProgramExplorer.Syntax.ASTSourceBase
-
Get the position of this node in the source code (may be null).
- getPosition() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.DeclarationBase
-
Get the position of this node in the source code (may be null).
- getPosition() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ExpressionBase
-
Get the position of this node in the source code (may be null).
- getPosition() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TypedIdentifier
-
Get the position of this node in the source code (may be null).
- getPosition() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ProgramAnnotationBase
-
Get the position of this node in the source code (may be null).
- getPosition() - Method in interface fmrisc.ProgramExplorer.Tasks.Task
-
Get source code position linked to this task (null, if none)
- getPosition() - Method in class fmrisc.ProgramExplorer.Tasks.TaskBase
-
Get source code position linked to this task (null, if none)
- getPositions() - Method in class fmrisc.ProgramExplorer.InOut.Source
-
Get positions for this source.
- getPostCondition() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.MethodSpec
-
Get method postcondition.
- getPostfix() - Method in class fmrisc.ProgramExplorer.Syntax.Name
-
Get the postfix of the name.
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.AndFormula
-
Get precedence value of the formula operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ArrayType
-
Get precedence value of the type operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.AtomicFormula
-
Get precedence value of the formula operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BinaryAtomicFormula
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BitAndTerm
-
Get precedence value of the term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BitNegationTerm
-
Get precedence value of the term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BitOrTerm
-
Get precedence value of the term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.DividesTerm
-
Get precedence value of the term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.EquivalentFormula
-
Get precedence value of the formula operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in interface fmrisc.ProgramExplorer.Syntax.Logic.Expression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ExpressionBase
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.FunctionApplication
-
Get precedence value of the formula operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.FunctionType
-
Get precedence value of the type operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseFormula
-
Get precedence value of the operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseTerm
-
Get precedence value of the term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ImpliesFormula
-
Get precedence value of the formula operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LetExpression
-
Get precedence value of the formula operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.MinusTerm
-
Get precedence value of the term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.NegationTerm
-
Get precedence value of the Term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.NotEquivalentFormula
-
Get precedence value of the formula operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.NotFormula
-
Get precedence value of the term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.OrFormula
-
Get precedence value of the formula operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PlusTerm
-
Get precedence value of the term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PostfixFormula
-
Get precedence value of the formula operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PowerTerm
-
Get precedence value of the term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ProgramVariableBase
-
Get precedence value of the term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.QuantifiedExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.QuantifiedTerm
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.SelectionTerm
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.StateMessage
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.StateValue
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TimesTerm
-
Get precedence value of the term operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.UpdateTerm
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.AndExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.BooleanLiteral
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.CharLiteral
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.DividesExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.EqualsExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.GreaterEqualExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.GreaterExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.IntLiteral
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.LessEqualExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.LessExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.MinusExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.NegationExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.NewArrayExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.NotEqualsExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.NotExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.NullLiteral
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.OrExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.PercentExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.PlusExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.SelectorExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.StringLiteral
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.TimesExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.ValueExpression
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecedence() - Method in class fmrisc.ProgramExplorer.Syntax.Program.VariableValue
-
Get precedence value of the expression operator
(higher precedence value means higher binding power)
- getPrecondition() - Method in class fmrisc.ProgramExplorer.Judgements.StatJudgement
-
Get the precondition formula.
- getPrecondition() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ForLoopStatement
-
Get for-loop precondition.
- getPreCondition() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.MethodSpec
-
Get method precondition.
- getPreconditions() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get the preconditions.
- getPredicate() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.SubType
-
Get predicate type.
- getPredicate() - Method in class fmrisc.ProofNavigator.Syntax.SubType
-
returns predicate
- getPrefix() - Method in class fmrisc.ProgramExplorer.Syntax.Name
-
Get the prefix of the name.
- getPrefix(int) - Method in class fmrisc.ProgramExplorer.Syntax.Name
-
Get prefix of first n identifiers of name.
- getPreMap() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get mapping of body statements to prestate knowledge.
- getPresenter() - Static method in class fmrisc.ProofNavigator.State
-
Get current presenter.
- getPrintParens() - Static method in class fmrisc.ProofNavigator.Syntax.ASTUtil
-
show whether every (sub)expression is to be printed with
enclosing parentheses
- getPrintUnique() - Static method in class fmrisc.ProofNavigator.Syntax.ASTUtil
-
show whether every identifier is printed with its unique name
- getPrintVarNumber() - Static method in class fmrisc.ProofNavigator.Syntax.ASTUtil
-
show whether every local variable is printed with its variable number
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.AndFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.ApplicationExpression
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.BitAndTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.BitLogical
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.BitNotTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.BitOrTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.DividesTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.EqualsFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.EquivalentFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in interface fmrisc.ProofNavigator.Syntax.Expression
-
Get Priority of expression (higher values mean less binding power).
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.ExpressionBase
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.GreaterEqualFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.GreaterFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.IfThenElseExpression
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.ImpliesFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.LessEqualFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.LessFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.LetExpression
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.Logical
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.MinusTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.NegationTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.NotEqualsFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.NotEquivalentFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.NotFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.Number
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.OrFormula
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.PlusTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.PowerTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.QuantifiedExpression
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.RecordTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.Reference
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.SelectionTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.TimesTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.TupleTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getPriority() - Method in class fmrisc.ProofNavigator.Syntax.UpdateTerm
-
get binding level for printing (lower numbers mean greater binding power)
- getProof() - Method in class fmrisc.ProgramExplorer.Proving.ProofNavigatorProblem
-
Get current proof, possibly load it from file.
- getProof() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
get proof to which proof state belong
- getProof() - Method in class fmrisc.ProofNavigator.Semantics.FormulaSymbol
-
Return proof of symbol.
- getProof() - Static method in class fmrisc.ProofNavigator.State
-
get current proof
- getProofColor() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get color for open tasks with a closed proof.
- getProperties() - Static method in class fmrisc.ProgramExplorer.Main
-
Get the system properties.
- getProver() - Static method in class fmrisc.ProofNavigator.State
-
get prover currently in use
- getProverLog() - Static method in class fmrisc.ProofNavigator.State
-
Get prover log
- getProverVersion() - Static method in class fmrisc.ProofNavigator.State
-
get version of prover currently in use
- getQuantifier() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ArrayTerm
-
Get string representation of quantifier.
- getQuantifier() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ExistsFormula
-
Get string representation of quantifier.
- getQuantifier() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ForallFormula
-
Get string representation of quantifier.
- getQuantifier() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LambdaFormula
-
Get string representation of quantifier.
- getQuantifier() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LambdaTerm
-
Get string representation of quantifier.
- getQuantifier() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.QuantifiedExpression
-
Get string representation of quantifier.
- getRange() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.FunctionType
-
Get range type.
- getRange() - Method in class fmrisc.ProofNavigator.Syntax.FunctionType
-
returns range of type
- getReaderStack() - Static method in class fmrisc.ProofNavigator.State
-
Get reader stack.
- getRealType() - Static method in class fmrisc.ProofNavigator.Semantics.Checking
-
Get canonical type REAL
- getReason() - Method in class fmrisc.ProofNavigator.Commands.Proved
-
get reason why state has been proved
- getRecursion() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get the set of methods (directly or indirectly) recursively called
by this method.
- getReferenced(Collection<Symbol>, Environment) - Static method in class fmrisc.ProofNavigator.Commands.DeclarationC
-
Get value symbols from collection that are contained in environment.
- getReferenced() - Method in class fmrisc.ProofNavigator.Proving.Proof
-
Get collection of symbols of those entities referenced
in the last call of toNode().
- getReferencedSymbols() - Static method in class fmrisc.ProofNavigator.Semantics.Checking
-
get collection of referenced symbols
- getReferencedUnits() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get symbols of units referenced by this unit.
- getReferencedUnits() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get symbols of units referenced by this unit.
- getRefreshImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get refresh image.
- getReplayChildren() - Static method in class fmrisc.ProofNavigator.State
-
Set children of current proof state during proof replay.
- getResult() - Method in class fmrisc.ProgramExplorer.Semantics.ReferencedExcs
-
Get the result of the computation.
- getResult() - Method in class fmrisc.ProgramExplorer.Semantics.ReferencedVars
-
Get the result of the computation.
- getReturn() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.StateType
-
Get return type.
- getReturnType() - Method in class fmrisc.ProgramExplorer.Semantics.MethodSymbol
-
Get return type of the method.
- getRoot(Document) - Method in class fmrisc.ProofNavigator.Communication.Presenter
-
Get root node of document to which new nodes should be appended.
- getRoot() - Method in class fmrisc.ProofNavigator.Proving.Proof
-
get root of proof
- getRunImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get run image.
- getRunningProver() - Static method in class fmrisc.ProofNavigator.State
-
Get prover currently running.
- getSatisfies() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get judgement processor for this method.
- getSecond() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BinaryAtomicFormula
-
Get second subterm.
- getSecond() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BinaryExpression
-
Get second subexpression.
- getSecond() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BinaryFormula
-
Get second subformula.
- getSecond() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BinaryTerm
-
Get second subterm.
- getSecond() - Method in class fmrisc.ProofNavigator.Syntax.BinaryExpression
-
Returns second subexpression
- getSelection() - Method in class fmrisc.ProgramExplorer.SWT.SymbolTree
-
Get symbols selected in tree.
- getSelector() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.SelectionTerm
-
Get selector.
- getSelector() - Method in class fmrisc.ProofNavigator.Syntax.SelectionTerm
-
get selector
- getSelectors() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.UpdateTerm
-
Get selectors.
- getSelectors() - Method in class fmrisc.ProofNavigator.Syntax.UpdateTerm
-
get the selectors
- getServerPort() - Static method in class fmrisc.ProofNavigator.State
-
Get server port.
- getSize() - Method in class fmrisc.ProgramExplorer.InOut.Source
-
Get size of source.
- getSkolemTable() - Method in class fmrisc.ProofNavigator.Proving.ProofState
-
Get unique name table to be used for creating skolemization constants.
- getSource() - Method in class fmrisc.ProgramExplorer.InOut.ClassReader
-
Get source for class reader.
- getSource() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotationPosition
-
Get the source file.
- getSource() - Method in interface fmrisc.ProgramExplorer.InOut.SourcePosition
-
Get the source file.
- getSource() - Method in class fmrisc.ProgramExplorer.InOut.SourcePositionClass
-
Get the source file.
- getSource() - Method in class fmrisc.ProgramExplorer.InOut.StringSourcePosition
-
Get the source file.
- getSource() - Method in class fmrisc.ProgramExplorer.InOut.TheoryReader
-
Get source for class reader.
- getSource() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get source of class.
- getSource() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get source of theory (respectively of associated class).
- getSourceImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get image for source files.
- getSourceLine() - Method in class fmrisc.ProgramExplorer.InOut.SourceAnnotationPosition
-
Get source line corresponding to position.
- getSourceLine() - Method in interface fmrisc.ProgramExplorer.InOut.SourcePosition
-
Get source line corresponding to position.
- getSourceLine() - Method in class fmrisc.ProgramExplorer.InOut.SourcePositionClass
-
Get source line corresponding to position.
- getSourceLine() - Method in class fmrisc.ProgramExplorer.InOut.StringSourcePosition
-
Get source line corresponding to position.
- getSpecification() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get method specification.
- getState() - Method in class fmrisc.ProofNavigator.Proving.Formula
-
Get proof state of formula.
- getState(String) - Method in class fmrisc.ProofNavigator.Proving.Proof
-
Get proof state with denoted tag.
- getState() - Method in class fmrisc.ProofNavigator.SWT.ProofTreeItem
-
Return proof state associated to item.
- getStateType() - Method in class fmrisc.ProgramExplorer.Judgements.Satisfies
-
Get the state type of this judgement processor
- getStatus() - Method in interface fmrisc.ProgramExplorer.Tasks.Task
-
Get status of task.
- getStatus() - Method in class fmrisc.ProgramExplorer.Tasks.TaskBase
-
Get status of task.
- getStatus() - Method in class fmrisc.ProofNavigator.Proving.Proof
-
Get status of proof.
- getStore() - Static method in class fmrisc.ProofNavigator.State
-
Get current store.
- getString() - Method in class fmrisc.ProgramExplorer.Syntax.Identifier
-
Get string representation of identifier.
- getStringClass() - Method in class fmrisc.ProgramExplorer.Semantics.TypeTable
-
Get string class.
- getStringClass() - Method in class fmrisc.ProgramExplorer.Syntax.Program.StringLiteral
-
Get the string class.
- getStringClass() - Method in class fmrisc.ProgramExplorer.Syntax.Program.StringType
-
Get the string class.
- getStringTheory() - Method in class fmrisc.ProgramExplorer.Semantics.TypeTranslator
-
Get the current string theory
- getStringType() - Method in class fmrisc.ProgramExplorer.Judgements.Satisfies
-
Get the string type of this judgement processor
- getStringType() - Method in class fmrisc.ProgramExplorer.Semantics.TypeTable
-
Get string type.
- getStringType() - Method in class fmrisc.ProgramExplorer.Semantics.TypeTranslator
-
Get the current string type.
- getSubstitution() - Method in class fmrisc.ProofNavigator.Syntax.TypeDeclIdentifier
-
returns substitution identifier for instantiation
- getSubstitution() - Method in class fmrisc.ProofNavigator.Syntax.ValueDeclIdentifier
-
returns substitution identifier for instantiation
- getSymbol() - Method in class fmrisc.ProgramExplorer.Syntax.Identifier
-
Get symbol denoted by identifier.
- getSymbol() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.AxiomDefinition
-
Get symbol introduced by declaration.
- getSymbol() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.FormulaDefinition
-
Get symbol introduced by declaration.
- getSymbol() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TypeDeclaration
-
Get symbol introduced by declaration.
- getSymbol() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ValueDeclarationClass
-
Get symbol introduced by declaration.
- getSymbol() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ValueDefinitionClass
-
Get symbol introduced by declaration.
- getSymbol() - Method in class fmrisc.ProgramExplorer.Syntax.Name
-
Get symbol identified by (last part of) name.
- getSymbol() - Method in class fmrisc.ProgramExplorer.Syntax.Program.NamedType
-
Get symbol of class denoted by name.
- getSymbol() - Method in class fmrisc.ProgramExplorer.Tasks.TaskFolder
-
Get the symbol associated to the folder.
- getSymbol() - Method in class fmrisc.ProofNavigator.Proving.Proof
-
get symbol of formula proved
- getSymbol(Identifier) - Method in class fmrisc.ProofNavigator.Semantics.FormulaTable
-
returns symbol associated to name (null, if none)
- getSymbol(Identifier) - Method in class fmrisc.ProofNavigator.Semantics.TypeTable
-
returns symbol associated to name (null, if none)
- getSymbol(Identifier) - Method in class fmrisc.ProofNavigator.Semantics.ValueTable
-
returns symbol associated to name (null, if none)
- getSymbol() - Method in interface fmrisc.ProofNavigator.Syntax.Declaration
-
Returns symbol.
- getSymbol() - Method in class fmrisc.ProofNavigator.Syntax.FormulaDeclaration
-
returns symbol
- getSymbol() - Method in class fmrisc.ProofNavigator.Syntax.FormulaDeclIdentifier
-
returns formula symbol
- getSymbol() - Method in class fmrisc.ProofNavigator.Syntax.Reference
-
returns symbol associated to reference
- getSymbol() - Method in class fmrisc.ProofNavigator.Syntax.TypeDeclaration
-
returns symbol
- getSymbol() - Method in class fmrisc.ProofNavigator.Syntax.TypeDeclIdentifier
-
returns type symbol
- getSymbol() - Method in class fmrisc.ProofNavigator.Syntax.ValueDeclaration
-
returns symbol
- getSymbol() - Method in class fmrisc.ProofNavigator.Syntax.ValueDeclIdentifier
-
returns value symbol
- getSymbols() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbols
-
Return collection of symbols in table.
- getSymbols() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbolTable
-
Return collection of symbols in table.
- getSymbols() - Method in class fmrisc.ProgramExplorer.Semantics.SymbolTable
-
Return collection of symbols in table.
- getSymbols(Environment) - Method in class fmrisc.ProofNavigator.Commands.Lemma
-
Return symbols of formulas referenced in lemma.
- getSymbols() - Method in class fmrisc.ProofNavigator.Proving.CVCL.CVCLFormulaMask
-
Return mask symbols generated since last call of resetSymbols().
- getSymbols() - Method in class fmrisc.ProofNavigator.Semantics.SymbolTable
-
Get all symbols.
- getSystemIn() - Static method in class fmrisc.ProofNavigator.State
-
get standard input stream
- getSystemOut() - Static method in class fmrisc.ProofNavigator.State
-
get standard output stream
- getTaskDoneImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get done task image.
- getTaskFailedImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get failed task image.
- getTaskNewImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get new task image.
- getTaskOpenImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get open task image.
- getTasks() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get the folder of tasks related to this class.
- getTasks() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get the folder of tasks related to this package.
- getTasks() - Method in class fmrisc.ProgramExplorer.Tasks.TaskFolder
-
Get tasks appropriately sorted for display
- getTCCGenerator() - Method in class fmrisc.ProgramExplorer.Semantics.LogicChecking
-
Get the generator for producing type checking conditions
- getTCCs() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get the type checking conditions.
- getTCCs() - Method in class fmrisc.ProgramExplorer.Semantics.ParamSymbol
-
Get the type checking conditions.
- getTCCs() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get the type checking conditions.
- getTCCs() - Method in class fmrisc.ProofNavigator.Semantics.Environment
-
Get type checking conditions of current scope (not of all scopes).
- getTerm() - Method in class fmrisc.ProofNavigator.Syntax.ArrayTerm
-
Get replacement term
- getTermination() - Method in class fmrisc.ProgramExplorer.Judgements.StatJudgement
-
Get the termination formula.
- getTerminationTerm() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.LoopSpec
-
Get termination term vector.
- getTerminationTerm() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.MethodSpec
-
Get termination term vector.
- getText() - Method in class fmrisc.ProgramExplorer.InOut.Source
-
Get the text of the source.
- getText() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ProgramAnnotationBase
-
Get annotation text.
- getThenBranch() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseExpression
-
Get "then" branch.
- getThenBranch() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseFormula
-
Get "then" branch.
- getThenBranch() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseTerm
-
Get "then" branch.
- getThenBranch() - Method in class fmrisc.ProofNavigator.Syntax.IfThenElseExpression
-
get then branch of expression
- getTheories() - Method in class fmrisc.ProgramExplorer.Semantics.LogicEnvironment
-
Get theories that may be referenced in environment in dependence order.
- getTheories() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get set of theories held by package.
- getTheories() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.TheoryDeclaration
-
Get theories on which unit depends.
- getTheories() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.UnitSpec
-
Get theories referenced by unit.
- getTheoryImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get theory image.
- getTheorySet() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get set of theories held by package as collection.
- getTheorySymbols(Name[]) - Static method in class fmrisc.ProgramExplorer.Syntax.NameUtils
-
Get vector of theory symbols denoted by names.
- getThisSymbol() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get "this" symbol for this class.
- getThread() - Static method in class fmrisc.ProofNavigator.SWT.MainSWT
-
Get interpreter thread
- getTimeStamp() - Static method in class fmrisc.ProgramExplorer.Main
-
Get time stamp of current program execution.
- getTo() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.SubrangeType
-
Get upper bound.
- getTo() - Method in class fmrisc.ProofNavigator.Syntax.SubrangeType
-
returns to bound
- getTokenNames() - Method in class fmrisc.ProgramExplorer.Parser.MiniJavaParser
-
- getTokenNames() - Method in class fmrisc.ProgramExplorer.Parser.SpecLangParser
-
- getTokenNames() - Method in class fmrisc.ProofNavigator.PN2Parser
-
- getTopPackage() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get top-level package of package
- getTopPackage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get top package.
- getTree() - Method in class fmrisc.ProgramExplorer.SWT.FileTree
-
Get visual representation of tree.
- getTree() - Method in class fmrisc.ProgramExplorer.SWT.SymbolTree
-
Get visual representation of tree.
- getTree() - Method in class fmrisc.ProgramExplorer.SWT.TaskList
-
Get the underlying tree representation.
- getTree() - Method in class fmrisc.ProgramExplorer.SWT.TaskTree
-
Get visual representation of tree.
- getTree() - Method in class fmrisc.ProofNavigator.Communication.BreakInfo
-
Get the tree to which this break information belongs.
- getTreeItem() - Method in class fmrisc.ProofNavigator.SWT.ProofTreeItem
-
Return tree item associated to item.
- getType() - Method in class fmrisc.ProgramExplorer.Semantics.ClassSymbol
-
Get type for for this class.
- getType() - Method in class fmrisc.ProgramExplorer.Semantics.TypeSymbol
-
Get type.
- getType() - Method in class fmrisc.ProgramExplorer.Semantics.ValueSymbol
-
Get type.
- getType() - Method in interface fmrisc.ProgramExplorer.Semantics.VariableSymbol
-
Get type of symbol.
- getType() - Method in class fmrisc.ProgramExplorer.Semantics.VariableSymbolBase
-
Get type of symbol.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.BinaryTerm
-
Set type annotation of term.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.Constant
-
Set type annotation of term.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.FunctionApplication
-
Set type annotation of term.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseTerm
-
Set type annotation of term.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.LetTerm
-
Set type annotation of term.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.PostfixTerm
-
Set type annotation of term.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.QuantifiedTerm
-
Set type annotation of term.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.Reference
-
Get type annotation of term.
- getType() - Method in interface fmrisc.ProgramExplorer.Syntax.Logic.Term
-
Get type annotation of term.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TermBase
-
Set type annotation of term.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TypedIdentifier
-
Get type.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.UnaryTerm
-
Set type annotation of term.
- getType() - Method in interface fmrisc.ProgramExplorer.Syntax.Logic.ValueDeclaration
-
Get type of value.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ValueDeclarationClass
-
Get type of the declaration.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Program.DeclCallStatement
-
Get the type of the declared entity.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Program.GlobalVariableDeclaration
-
Get the type of the declared entity.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Program.NullLiteral
-
Get type of objects/arrays to which this null reference belongs.
- getType() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.Selector
-
get type of expression after selection
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Program.SelectorBase
-
set type of expression after selection
- getType() - Method in interface fmrisc.ProgramExplorer.Syntax.Program.VariableDeclaration
-
Get the type of the declared entity.
- getType() - Method in class fmrisc.ProgramExplorer.Syntax.Program.VariableDeclarationBase
-
Get the type of the declared entity.
- getType(Identifier) - Method in class fmrisc.ProofNavigator.Semantics.Environment
-
returns canonical type associated to key
type equality implies pointer equality of types.
- getType() - Method in class fmrisc.ProofNavigator.Semantics.TypeExpression
-
get type
- getType() - Method in class fmrisc.ProofNavigator.Semantics.TypeSymbol
-
Return type of symbol.
- getType(Identifier) - Method in class fmrisc.ProofNavigator.Semantics.TypeTable
-
returns canonical type associated to key
type equality implies pointer equality of types.
- getType() - Method in class fmrisc.ProofNavigator.Semantics.ValueSymbol
-
Return type of symbol.
- getType() - Method in class fmrisc.ProofNavigator.Syntax.PowerTerm
-
get result type
- getType() - Method in class fmrisc.ProofNavigator.Syntax.TimesTerm
-
get result type
- getType() - Method in class fmrisc.ProofNavigator.Syntax.TypeDeclaration
-
returns declaration type
- getType() - Method in class fmrisc.ProofNavigator.Syntax.TypedIdentifier
-
returns identifier type
- getType() - Method in class fmrisc.ProofNavigator.Syntax.ValueDeclaration
-
returns declaration type
- getTypeDeclIdentifier() - Method in class fmrisc.ProofNavigator.Semantics.TypeSymbol
-
Return identifier of symbol.
- getTypeDeclIdentifier() - Method in class fmrisc.ProofNavigator.Syntax.TypeDeclaration
-
returns declaration name
- getTypeImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get type image.
- getTypes() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get set of types of this theory.
- getTypeSymbol(Identifier) - Method in class fmrisc.ProgramExplorer.Semantics.LogicEnvironment
-
Returns type symbol associated to name.
- getTypeSymbol(Reference) - Method in class fmrisc.ProgramExplorer.Semantics.LogicEnvironment
-
Get type denoted by reference in current environment
- getTypeSymbol(Identifier) - Method in class fmrisc.ProofNavigator.Semantics.Environment
-
returns type symbol associated to key
- getTypeSymbols() - Method in class fmrisc.ProgramExplorer.Semantics.LogicEnvironment
-
Get all type symbols.
- getTypeSymbols() - Method in class fmrisc.ProofNavigator.Semantics.Environment
-
Get all type symbols.
- getTypeTable() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get type table of package.
- getTypeTable() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get type table of theory.
- getTypeTranslator() - Method in class fmrisc.ProgramExplorer.Semantics.PackageSymbol
-
Get type translator of package.
- getUniqueName(String) - Static method in class fmrisc.ProofNavigator.Syntax.ASTUtil
-
Create unique identifier name from given name.
- getUniqueName(String) - Method in class fmrisc.ProofNavigator.Syntax.UniqueNameTable
-
Create unique identifier name from given name.
- getUniqueName() - Method in class fmrisc.ProofNavigator.Syntax.ValueDeclIdentifier
-
returns unique name of identifier
- getUnit(PackageSymbol, String, boolean) - Static method in class fmrisc.ProgramExplorer.Main
-
Get symbol of unit denoted by qualified name in top-level package.
- getUnitSymbols() - Method in class fmrisc.ProgramExplorer.SWT.SymbolTree
-
Get all symbols in symbol tree denoting units (classes/theories).
- getUpdate() - Method in class fmrisc.ProofNavigator.Syntax.UpdateTerm
-
get the update value
- getValue() - Method in interface fmrisc.ProgramExplorer.Syntax.Logic.Definition
-
Get the value of the defined entity.
- getValue() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.FormulaDefinition
-
Get the formula value.
- getValue() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.TypeDefinition
-
Get the type value.
- getValue() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.UpdateTerm
-
Get update value.
- getValue() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ValueDeclarationInitialized
-
Get value of the declaration.
- getValue() - Method in interface fmrisc.ProgramExplorer.Syntax.Logic.ValueDefinition
-
Get value.
- getValue() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ValueDefinitionClass
-
Get value of the definition.
- getValue() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.ValuedIdentifier
-
Get value.
- getValue() - Method in class fmrisc.ProgramExplorer.Syntax.Program.ThrowStatement
-
Get the exception value.
- getValue() - Method in class fmrisc.ProofNavigator.Semantics.ValueSymbol
-
Return value of symbol
- getValue() - Method in class fmrisc.ProofNavigator.Syntax.BitLogical
-
get value of constant
- getValue() - Method in class fmrisc.ProofNavigator.Syntax.Logical
-
get value of constant
- getValue() - Method in class fmrisc.ProofNavigator.Syntax.ValueDeclaration
-
returns declaration value
- getValue() - Method in class fmrisc.ProofNavigator.Syntax.ValuedIdentifier
-
returns identifier value
- getValueDeclIdentifier() - Method in class fmrisc.ProofNavigator.Semantics.ValueSymbol
-
Return identifier of symbol.
- getValueDeclIdentifier() - Method in class fmrisc.ProofNavigator.Syntax.ValueDeclaration
-
returns declaration name
- getValueImage() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get value image.
- getValues() - Method in class fmrisc.ProgramExplorer.Semantics.TheorySymbol
-
Get set of values of this theory.
- getValueSymbol(Identifier) - Method in class fmrisc.ProgramExplorer.Semantics.LogicEnvironment
-
Returns value symbol associated to name.
- getValueSymbol(Reference) - Method in class fmrisc.ProgramExplorer.Semantics.LogicEnvironment
-
Get value denoted by reference in current environment
- getValueSymbol(Identifier) - Method in class fmrisc.ProofNavigator.Semantics.Environment
-
returns symbol associated to name (null, if none)
- getValueSymbols() - Method in class fmrisc.ProgramExplorer.Semantics.LogicEnvironment
-
Get all value symbols.
- getValueSymbols() - Method in class fmrisc.ProofNavigator.Semantics.Environment
-
Get all value symbols.
- getVariable(Identifier) - Method in class fmrisc.ProgramExplorer.Semantics.Environment
-
Return symbol for variable denoted by identifier in current environment.
- getVariable(Name) - Method in class fmrisc.ProgramExplorer.Semantics.Environment
-
Return symbol for variable denoted by name in current environment.
- getVariable(Name, boolean) - Method in class fmrisc.ProgramExplorer.Semantics.Environment
-
Return symbol for variable denoted by name in current environment.
- getVariable(Name) - Static method in class fmrisc.ProgramExplorer.Syntax.NameUtils
-
Determine variable prefix of name.
- getVariablePosition(Name) - Static method in class fmrisc.ProgramExplorer.Syntax.NameUtils
-
Determine variable prefix of name.
- getVariablePrefixSymbol(Name) - Static method in class fmrisc.ProgramExplorer.Syntax.NameUtils
-
Determine variable prefix symbol of name.
- getVariablePrefixSymbols(Name[]) - Static method in class fmrisc.ProgramExplorer.Syntax.NameUtils
-
Get set of variable symbols denoted by name.
- getVariables() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.QuantifiedExpression
-
Get bound variables of the expression.
- getVariables() - Method in class fmrisc.ProgramExplorer.Syntax.Logic.WritesOnlyFormula
-
Get names of variables that are allowed to change.
- getVariables() - Method in class fmrisc.ProgramExplorer.Syntax.Spec.MethodSpec
-
Get method frame i.e.
- getVariables() - Method in class fmrisc.ProofNavigator.Syntax.QuantifiedExpression
-
get quantified variables
- getVarNumber() - Method in class fmrisc.ProofNavigator.Semantics.ValueSymbol
-
Return variable number of symbol.
- getVarNumber() - Static method in class fmrisc.ProofNavigator.Syntax.ASTUtil
-
get current variable number for printing
- getVersion() - Static method in class fmrisc.ProgramExplorer.Main
-
Return version string.
- getVersion() - Static method in class fmrisc.ProofNavigator.Main
-
Return version string.
- getVersion() - Method in class fmrisc.ProofNavigator.Proving.CVCL.CVCL
-
Get version of checker.
- getVirtualDirectoryPort() - Method in class fmrisc.ProgramExplorer.SWT.MainSWT
-
Get port number of virtual directory server.
- getWhiteColor() - Method in class fmrisc.ProgramExplorer.SWT.TopWindow
-
Get color white.
- GlobalSymbol - Interface in fmrisc.ProgramExplorer.Semantics
-
The interface to a symbol that can be globally referenced.
- GlobalSymbolBase - Class in fmrisc.ProgramExplorer.Semantics
-
The base class of a symbol that can be globally referenced.
- GlobalSymbolBase(Identifier, Name) - Constructor for class fmrisc.ProgramExplorer.Semantics.GlobalSymbolBase
-
Construct a symbol that can be externally referenced.
- GlobalSymbolBase(GlobalSymbol, Identifier) - Constructor for class fmrisc.ProgramExplorer.Semantics.GlobalSymbolBase
-
Construct a symbol that can be externally referenced.
- GlobalVariableDeclaration - Class in fmrisc.ProgramExplorer.Syntax.Program
-
A global variable declaration.
- GlobalVariableSymbolBase - Class in fmrisc.ProgramExplorer.Semantics
-
The base class of a variable symbol that can be externally referenced.
- goal - Variable in class fmrisc.ProgramExplorer.Tasks.FlattenDeclarations.Result
-
- Goal - Class in fmrisc.ProofNavigator.Commands
-
Command "goal": let a formula become the single goal.
- Goal(String) - Constructor for class fmrisc.ProofNavigator.Commands.Goal
-
Create a "goal" command.
- Goto - Class in fmrisc.ProofNavigator.Commands
-
The "goto" command: goto an open proof state.
- Goto(String) - Constructor for class fmrisc.ProofNavigator.Commands.Goto
-
create a "goto" command
- GREATER - Static variable in class fmrisc.ProgramExplorer.Parser.SpecLangLexer
-
- GREATER - Static variable in class fmrisc.ProgramExplorer.Parser.SpecLangParser
-
- GREATER - Static variable in class fmrisc.ProofNavigator.PN2Lexer
-
- GREATER - Static variable in class fmrisc.ProofNavigator.PN2Parser
-
- GREATER - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes
-
- GREATER - Static variable in interface fmrisc.ProofNavigator.Proving.CVCL.CVCLParserTokenTypes
-
- GREATEREQ - Static variable in class fmrisc.ProgramExplorer.Parser.SpecLangLexer
-
- GREATEREQ - Static variable in class fmrisc.ProgramExplorer.Parser.SpecLangParser
-
- GREATEREQ - Static variable in class fmrisc.ProofNavigator.PN2Lexer
-
- GREATEREQ - Static variable in class fmrisc.ProofNavigator.PN2Parser
-
- GREATEREQ - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes
-
- GREATEREQ - Static variable in interface fmrisc.ProofNavigator.Proving.CVCL.CVCLParserTokenTypes
-
- GreaterEqualExpression - Class in fmrisc.ProgramExplorer.Syntax.Program
-
An is-greater-than-or-equal formula.
- GreaterEqualFormula - Class in fmrisc.ProgramExplorer.Syntax.Logic
-
An is-greater-than-or-equal formula.
- greaterEqualFormula(Expression, Expression) - Static method in class fmrisc.ProofNavigator.Syntax.Construct
-
construct greater-than-or-equal formula with components base1 and base2
- GreaterEqualFormula - Class in fmrisc.ProofNavigator.Syntax
-
Handling of greater-than-or-equal formulas.
- GreaterEqualFormula(Expression, Expression) - Constructor for class fmrisc.ProofNavigator.Syntax.GreaterEqualFormula
-
construct greater-than-or-equal formula with components base1 and base2
- GreaterExpression - Class in fmrisc.ProgramExplorer.Syntax.Program
-
An is-greater-than formula.
- GreaterFormula - Class in fmrisc.ProgramExplorer.Syntax.Logic
-
An is-greater-than formula.
- greaterFormula(Expression, Expression) - Static method in class fmrisc.ProofNavigator.Syntax.Construct
-
construct greater-than formula with components base1 and base2
- GreaterFormula - Class in fmrisc.ProofNavigator.Syntax
-
Handling of greater-than formulas.
- GreaterFormula(Expression, Expression) - Constructor for class fmrisc.ProofNavigator.Syntax.GreaterFormula
-
construct greater-than formula with components base1 and base2
- GroundExpressions - Class in fmrisc.ProofNavigator.Proving
-
Compute ground (sub)expressions.
- GroundExpressions() - Constructor for class fmrisc.ProofNavigator.Proving.GroundExpressions
-