A B C D E F G H I J K L M N O P Q R S T U V W X _

G

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

generateCounterExamples(boolean) - Method in class fmrisc.Proving.CVCL.CVCL

generate counterexamples, if possible.

generateCounterExamples(boolean) - Method in interface fmrisc.Proving.Prover

generate counterexamples, if possible.

getArguments() - Method in class fmrisc.Syntax.ApplicationExpression

get arguments

getAssumption(String) - Method in class fmrisc.Proving.ProofState

returns assumption with denoted label

getAssumptions() - Method in class fmrisc.Proving.ProofState

get assumptions of proof state

getAxioms() - Method in class fmrisc.Proving.ProofState

get axioms of proof state

getBackgroundColor() - Static method in class fmrisc.ProofNavigator.SWT.MainSWT

Get background color.

getBase() - Method in class fmrisc.Syntax.ArrayType

returns base type

getBase() - Method in class fmrisc.Syntax.LetExpression

get base expression

getBase() - Method in class fmrisc.Syntax.LetType

get base type

getBase() - Method in class fmrisc.Syntax.QuantifiedExpression

get base expression

getBase() - Method in class fmrisc.Syntax.RecordTerm

returns base terms

getBase() - Method in class fmrisc.Syntax.RecordType

returns base types

getBase() - Method in class fmrisc.Syntax.SelectionTerm

get base expression

getBase() - Method in class fmrisc.Syntax.SubType

returns base type

getBase() - Method in class fmrisc.Syntax.TupleTerm

get base expressions

getBase() - Method in class fmrisc.Syntax.TupleType

returns base types

getBase() - Method in class fmrisc.Syntax.UnaryExpression

Returns base expression

getBase() - Method in class fmrisc.Syntax.UpdateTerm

get the base expression

getBaseName(String) - Static method in class fmrisc.Syntax.ASTUtil

Get base name from name.

getBaseName(String) - Static method in class fmrisc.Syntax.UniqueNameTable

Get base name from name.

getBooleanType() - Static method in class fmrisc.Semantics.Checking

Get canonical type BOOLEAN

getChildren() - Method in class fmrisc.Communication.BreakInfo

Get the children of this node.

getChildren() - Method in class fmrisc.Proving.ProofState

get children of proof state

getClearType() - Method in class fmrisc.Semantics.ValueSymbol

Get clear type.

getClosedColor() - Static method in class fmrisc.ProofNavigator.SWT.MainSWT

Get color for closed proof tree nodes.

getCommand() - Method in class fmrisc.Proving.ProofState

get command of proof state

getCondition() - Method in class fmrisc.Syntax.IfThenElseExpression

get condition of expression

getContext() - Static method in class fmrisc.ProofNavigator.State

get context used by proof navigator

getCounterExample() - Method in class fmrisc.Proving.CVCL.InvalidAnswerCVCL

Interpret justification as a counterexample.

getCounterExample() - Method in class fmrisc.Proving.InvalidAnswer

Interpret justification as a counterexample.

getCounterExample() - Method in class fmrisc.Proving.ProofState

Get counterexample for state.

getCurrent() - Method in class fmrisc.Proving.Proof

get current open proof state

getCurrentColor() - Static method in class fmrisc.ProofNavigator.SWT.MainSWT

Get color for current proof node.

getDeclarations() - Method in class fmrisc.Syntax.LetExpression

get declarations

getDeclarations() - Method in class fmrisc.Syntax.LetType

get declarations

getDeclFile() - Method in class fmrisc.Communication.Presenter

Get file where all declarations are stored

getDepth() - Method in class fmrisc.Semantics.ValueSymbol

Return environment depth of symbol.

getDigits() - Method in class fmrisc.Syntax.Number

get digit representation of number

getDomain() - Method in class fmrisc.Syntax.FunctionType

returns domain of type

getElseBranch() - Method in class fmrisc.Syntax.IfThenElseExpression

get else branch of expression

getEnvironment() - Static method in class fmrisc.ProofNavigator.State

get environment used by proof navigator

getEnvironment() - Method in class fmrisc.Proving.ProofState

get environment of proof state

getEnvironment() - Method in class fmrisc.Semantics.FormulaSymbol

Return environment of symbol (up to the point where the symbol was decld).

getError() - Static method in class fmrisc.ProofNavigator.State

get error message set

getError() - Method in class fmrisc.Proving.CVCL.CVCL

error message, if CVCL instance is not okay

getError() - Method in interface fmrisc.Proving.Prover

error message, if last command signalled a problem

getExpression() - Method in class fmrisc.Proving.Formula

Get formula expression.

getExpression() - Method in class fmrisc.Semantics.TypeExpression

get exp

getExpressions() - Method in class fmrisc.Proving.GroundExpressions

Get the collection of ground expressions collected in this set.

getExternalName(ValueDeclIdentifier) - Static method in class fmrisc.Proving.CVCL.CVCL

create CVCL identifier from given name

getFile(ProofState) - Method in class fmrisc.Communication.Presenter

Construct file name for proof state

getFileStack() - Static method in class fmrisc.ProofNavigator.State

Get file stack.

getFirst() - Method in class fmrisc.Syntax.BinaryExpression

Returns first subexpression

getFormula(Identifier) - Method in class fmrisc.Proving.CVCL.CVCLFormulaMask

Get formula associated to mask identifier

getFormula(String) - Method in class fmrisc.Proving.ProofState

returns formula (assumption or goal) with denoted label

getFormula() - Method in class fmrisc.Semantics.Context

return the formula currently on the top of the stack

getFormula() - Method in class fmrisc.Semantics.FormulaSymbol

Return formula of symbol.

getFormula(Identifier) - Method in class fmrisc.Semantics.FormulaTable

returns formula associated to key

getFormula() - Method in class fmrisc.Syntax.FormulaDeclaration

returns declaration formula

getFormulaDeclIdentifier() - Method in class fmrisc.Semantics.FormulaSymbol

Return identifier of symbol.

getFormulaDeclIdentifier() - Method in class fmrisc.Syntax.FormulaDeclaration

returns declaration name

getFormulaMask() - Static method in class fmrisc.ProofNavigator.State

Get formula mask.

getFormulaSymbol(Identifier) - Method in class fmrisc.Semantics.Environment

returns symbol associated to name (null, if none)

getFormulaSymbols() - Method in class fmrisc.Semantics.Environment

Get all formula symbols.

getFrom() - Method in class fmrisc.Syntax.SubrangeType

returns lower bound

getFunction() - Method in class fmrisc.Syntax.ApplicationExpression

get function/predicate

getGlobal() - Static method in class fmrisc.ProofNavigator.State

get global environment of proof navigator

getGlobalValueSymbols() - Method in class fmrisc.Semantics.Environment

Get global value symbols in the order in which they were entered.

getGoal(String) - Method in class fmrisc.Proving.ProofState

returns goal with denoted label

getGoals() - Method in class fmrisc.Proving.ProofState

get goals of proof state

getIdent() - Method in class fmrisc.ProofNavigator.Commands.Prove

get name of formula to be proved

getIdentifier() - Method in interface fmrisc.Semantics.Symbol

Get identifier associated to symbol.

getIdentifier() - Method in class fmrisc.Semantics.SymbolBase

get identifier associated to symbol

getIdentifier() - Method in interface fmrisc.Syntax.Declaration

Returns declaration name.

getIdentifier() - Method in class fmrisc.Syntax.FormulaDeclaration

returns declaration name

getIdentifier() - Method in class fmrisc.Syntax.SelectorIdentifier

return identifier

getIdentifier() - Method in class fmrisc.Syntax.TypeDeclaration

returns declaration name

getIdentifier() - Method in class fmrisc.Syntax.TypedIdentifier

returns identifier name

getIdentifier() - Method in class fmrisc.Syntax.ValueDeclaration

returns declaration name

getIdentifier() - Method in class fmrisc.Syntax.ValuedIdentifier

returns identifier

getIndex() - Method in class fmrisc.Syntax.ArrayType

returns index type

getIndex() - Method in class fmrisc.Syntax.SelectorIndex

get index expression

getIntType() - Static method in class fmrisc.Semantics.Checking

Get canonical type INT

getJustification() - Method in interface fmrisc.Proving.Answer

Return justification of answer suitable for printing.

getJustification() - Method in class fmrisc.Proving.AnswerBase

Return justification of answer suitable for printing.

getLabel() - Method in class fmrisc.Proving.Formula

get formula label

getLabel() - Method in class fmrisc.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.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

getListener() - Method in class fmrisc.Proving.ProofState

Get listener that is notified when proof state has changed.

getLocalVariables() - Method in class fmrisc.Semantics.Environment

get local variables (all values with environment depth > 0)

getMask(Expression) - Method in class fmrisc.Proving.CVCL.CVCLFormulaMask

Mask a formula.

getName() - Method in class fmrisc.ProofNavigator.Commands.CommandBase

get name of command

getName() - Method in class fmrisc.Syntax.AtomicType

returns name of identifier

getName() - Method in class fmrisc.Syntax.Identifier

returns name of identifier

getNamespacePrefix() - Method in class fmrisc.External.NewOMDOMWriter

Get the namespace prefix.

getNatType() - Static method in class fmrisc.Semantics.Checking

Get canonical type NAT

getNumber() - Method in class fmrisc.Syntax.SelectorNumber

get the base number

getOpenColor() - Static method in class fmrisc.ProofNavigator.SWT.MainSWT

Get color for open proof tree nodes.

getOpenGoal() - Method in class fmrisc.Proving.Proof

get open leaf goal

getOpenGoals() - Method in class fmrisc.Proving.Proof

get open leaf goals

getOriginalName(String) - Static method in class fmrisc.Proving.CVCL.CVCL

Get original name from external CVCL name.

getParent() - Method in class fmrisc.Proving.ProofState

get parent of proof state

getPath() - Method in class fmrisc.Proving.ProofState

get path of proof state

getPortNumber() - Method in class fmrisc.Communication.CommandServer

Get port number on which server is listening.

getPredicate() - Method in class fmrisc.Syntax.SubType

returns predicate

getPresenter() - Static method in class fmrisc.ProofNavigator.State

Get current presenter.

getPrintParens() - Static method in class fmrisc.Syntax.ASTUtil

show whether every (sub)expression is to be printed with enclosing parentheses

getPrintUnique() - Static method in class fmrisc.Syntax.ASTUtil

show whether every identifier is printed with its unique name

getPrintVarNumber() - Static method in class fmrisc.Syntax.ASTUtil

show whether every local variable is printed with its variable number

getPriority() - Method in class fmrisc.Syntax.AndFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.ApplicationExpression

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.DividesTerm

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.EqualsFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.EquivalentFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in interface fmrisc.Syntax.Expression

Get Priority of expression (higher values mean less binding power).

getPriority() - Method in class fmrisc.Syntax.ExpressionBase

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.GreaterEqualFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.GreaterFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.IfThenElseExpression

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.ImpliesFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.LessEqualFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.LessFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.LetExpression

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.Logical

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.MinusTerm

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.NegationTerm

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.NotEqualsFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.NotEquivalentFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.NotFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.Number

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.OrFormula

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.PlusTerm

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.PowerTerm

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.QuantifiedExpression

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.RecordTerm

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.Reference

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.SelectionTerm

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.TimesTerm

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.TupleTerm

get binding level for printing (lower numbers mean greater binding power)

getPriority() - Method in class fmrisc.Syntax.UpdateTerm

get binding level for printing (lower numbers mean greater binding power)

getProof() - Static method in class fmrisc.ProofNavigator.State

get current proof

getProof() - Method in class fmrisc.Proving.ProofState

get proof to which proof state belong

getProof() - Method in class fmrisc.Semantics.FormulaSymbol

Return proof of symbol.

getProver() - Static method in class fmrisc.ProofNavigator.State

get prover currently in use

getProverLog() - Static method in class fmrisc.ProofNavigator.State

Get prover log

getRange() - Method in class fmrisc.Syntax.FunctionType

returns range of type

getReaderStack() - Static method in class fmrisc.ProofNavigator.State

Get reader stack.

getReason() - Method in class fmrisc.ProofNavigator.Commands.Proved

get reason why state has been proved

getReferenced() - Method in class fmrisc.Proving.Proof

Get collection of symbols of those entities referenced in the last call of toNode().

getReferencedSymbols() - Static method in class fmrisc.Semantics.Checking

get collection of referenced symbols

getReplayChildren() - Static method in class fmrisc.ProofNavigator.State

Set children of current proof state during proof replay.

getRoot(Document) - Method in class fmrisc.Communication.Presenter

Get root node of document to which new nodes should be appended.

getRoot() - Method in class fmrisc.Proving.Proof

get root of proof

getRunningProver() - Static method in class fmrisc.ProofNavigator.State

Get prover currently running.

getSecond() - Method in class fmrisc.Syntax.BinaryExpression

Returns second subexpression

getSelector() - Method in class fmrisc.Syntax.SelectionTerm

get selector

getSelectors() - Method in class fmrisc.Syntax.UpdateTerm

get the selectors

getServerPort() - Static method in class fmrisc.ProofNavigator.State

Get server port.

getSkolemTable() - Method in class fmrisc.Proving.ProofState

Get unique name table to be used for creating skolemization constants.

getState() - Method in class fmrisc.ProofNavigator.SWT.ProofTreeItem

Return proof state associated to item.

getState() - Method in class fmrisc.Proving.Formula

Get proof state of formula.

getState(String) - Method in class fmrisc.Proving.Proof

Get proof state with denoted tag.

getStatus() - Method in class fmrisc.Proving.Proof

Get status of proof.

getStore() - Static method in class fmrisc.ProofNavigator.State

Get current store.

getSubstitution() - Method in class fmrisc.Syntax.TypeDeclIdentifier

returns substitution identifier for instantiation

getSubstitution() - Method in class fmrisc.Syntax.ValueDeclIdentifier

returns substitution identifier for instantiation

getSymbol() - Method in class fmrisc.Proving.Proof

get symbol of formula proved

getSymbol(Identifier) - Method in class fmrisc.Semantics.FormulaTable

returns symbol associated to name (null, if none)

getSymbol(Identifier) - Method in class fmrisc.Semantics.TypeTable

returns symbol associated to name (null, if none)

getSymbol(Identifier) - Method in class fmrisc.Semantics.ValueTable

returns symbol associated to name (null, if none)

getSymbol() - Method in interface fmrisc.Syntax.Declaration

Returns symbol.

getSymbol() - Method in class fmrisc.Syntax.FormulaDeclaration

returns symbol

getSymbol() - Method in class fmrisc.Syntax.FormulaDeclIdentifier

returns formula symbol

getSymbol() - Method in class fmrisc.Syntax.Reference

returns symbol associated to reference

getSymbol() - Method in class fmrisc.Syntax.TypeDeclaration

returns symbol

getSymbol() - Method in class fmrisc.Syntax.TypeDeclIdentifier

returns type symbol

getSymbol() - Method in class fmrisc.Syntax.ValueDeclaration

returns symbol

getSymbol() - Method in class fmrisc.Syntax.ValueDeclIdentifier

returns value symbol

getSymbols(Environment) - Method in class fmrisc.ProofNavigator.Commands.Lemma

Return symbols of formulas referenced in lemma.

getSymbols() - Method in class fmrisc.Proving.CVCL.CVCLFormulaMask

Return mask symbols generated since last call of resetSymbols().

getSymbols() - Method in class fmrisc.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

getTCCs() - Method in class fmrisc.Semantics.Environment

Get type checking conditions of current scope (not of all scopes).

getThenBranch() - Method in class fmrisc.Syntax.IfThenElseExpression

get then branch of expression

getThread() - Static method in class fmrisc.ProofNavigator.SWT.MainSWT

Get interpreter thread

getTo() - Method in class fmrisc.Syntax.SubrangeType

returns to bound

getTree() - Method in class fmrisc.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(Identifier) - Method in class fmrisc.Semantics.Environment

returns canonical type associated to key type equality implies pointer equality of types.

getType() - Method in class fmrisc.Semantics.TypeExpression

get type

getType() - Method in class fmrisc.Semantics.TypeSymbol

Return type of symbol.

getType(Identifier) - Method in class fmrisc.Semantics.TypeTable

returns canonical type associated to key type equality implies pointer equality of types.

getType() - Method in class fmrisc.Semantics.ValueSymbol

Return type of symbol.

getType() - Method in class fmrisc.Syntax.TypeDeclaration

returns declaration type

getType() - Method in class fmrisc.Syntax.TypedIdentifier

returns identifier type

getType() - Method in class fmrisc.Syntax.ValueDeclaration

returns declaration type

getTypeDeclIdentifier() - Method in class fmrisc.Semantics.TypeSymbol

Return identifier of symbol.

getTypeDeclIdentifier() - Method in class fmrisc.Syntax.TypeDeclaration

returns declaration name

getTypeSymbol(Identifier) - Method in class fmrisc.Semantics.Environment

returns type symbol associated to key

getTypeSymbols() - Method in class fmrisc.Semantics.Environment

Get all type symbols.

getUniqueName(String) - Static method in class fmrisc.Syntax.ASTUtil

Create unique identifier name from given name.

getUniqueName(String) - Method in class fmrisc.Syntax.UniqueNameTable

Create unique identifier name from given name.

getUniqueName() - Method in class fmrisc.Syntax.ValueDeclIdentifier

returns unique name of identifier

getUpdate() - Method in class fmrisc.Syntax.UpdateTerm

get the update value

getValue() - Method in class fmrisc.Semantics.ValueSymbol

Return value of symbol

getValue() - Method in class fmrisc.Syntax.Logical

get value of constant

getValue() - Method in class fmrisc.Syntax.ValueDeclaration

returns declaration value

getValue() - Method in class fmrisc.Syntax.ValuedIdentifier

returns identifier value

getValueDeclIdentifier() - Method in class fmrisc.Semantics.ValueSymbol

Return identifier of symbol.

getValueDeclIdentifier() - Method in class fmrisc.Syntax.ValueDeclaration

returns declaration name

getValueSymbol(Identifier) - Method in class fmrisc.Semantics.Environment

returns symbol associated to name (null, if none)

getValueSymbols() - Method in class fmrisc.Semantics.Environment

Get all value symbols.

getVariables() - Method in class fmrisc.Syntax.QuantifiedExpression

get quantified variables

getVarNumber() - Method in class fmrisc.Semantics.ValueSymbol

Return variable number of symbol.

getVarNumber() - Static method in class fmrisc.Syntax.ASTUtil

get current variable number for printing

getVersion() - Static method in class fmrisc.ProofNavigator.Main

Return version string.

Goal - Class in fmrisc.ProofNavigator.Commands

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 interface fmrisc.ProofNavigator.PNParserTokenTypes

GREATER - Static variable in interface fmrisc.Proving.CVCL.CVCLParserTokenTypes

GREATEREQ - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

GREATEREQ - Static variable in interface fmrisc.Proving.CVCL.CVCLParserTokenTypes

greaterEqualFormula(Expression, Expression) - Static method in class fmrisc.Syntax.Construct

construct greater-than-or-equal formula with components base1 and base2

GreaterEqualFormula - Class in fmrisc.Syntax

Handling of greater-than-or-equal formulas.

GreaterEqualFormula(Expression, Expression) - Constructor for class fmrisc.Syntax.GreaterEqualFormula

construct greater-than-or-equal formula with components base1 and base2

greaterFormula(Expression, Expression) - Static method in class fmrisc.Syntax.Construct

construct greater-than formula with components base1 and base2

GreaterFormula - Class in fmrisc.Syntax

Handling of greater-than formulas.

GreaterFormula(Expression, Expression) - Constructor for class fmrisc.Syntax.GreaterFormula

construct greater-than formula with components base1 and base2

GroundExpressions - Class in fmrisc.Proving

Compute ground (sub)expressions.

GroundExpressions() - Constructor for class fmrisc.Proving.GroundExpressions