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

I

IDENT - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

Identifier - Class in fmrisc.Syntax

Handling of identifiers.

Identifier(String) - Constructor for class fmrisc.Syntax.Identifier

construct identifier from name

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

construct if-then-else expressions from condition, thenbranch, elsebranch.

IfThenElseExpression - Class in fmrisc.Syntax

Handling of if-then-else expressions.

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

construct if-then-else expressions from condition, thenbranch, elsebranch.

IGNORE - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

IMPLIES - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

implies(Expression) - Method in class fmrisc.Semantics.Context

conjoin formula to the current formula on the top of the stack

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

construct implication with components base1 and base2

ImpliesFormula - Class in fmrisc.Syntax

Handling of implications

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

construct conjunction with components base1 and base2

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

increase the current variable number for printing by one

Induction - Class in fmrisc.ProofNavigator.Commands

Command "induction": induction on a univerally quantified NAT/INT variable.

Induction(Identifier, String) - Constructor for class fmrisc.ProofNavigator.Commands.Induction

Create an "induction" command.

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

Initialize the system state.

init(String, String) - Static method in class fmrisc.ProofNavigator.State

Initialize prover state using denoted context.

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

Initialize checking state

Instantiate - Class in fmrisc.ProofNavigator.Commands

The "instantiate" command: instantiate a quantified formula.

Instantiate(String, Expression[]) - Constructor for class fmrisc.ProofNavigator.Commands.Instantiate

Create an "instantiate" command.

instantiate(ProofState) - Static method in class fmrisc.Proving.Instantiating

Extend given proof state by instantiations of quantified formulas.

instantiate(Formula) - Static method in class fmrisc.Proving.Instantiating

Extend proof state by instantiations of given formula

instantiate(Formula[]) - Static method in class fmrisc.Proving.Instantiating

Extend proof state by instantiations of given formulas

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

create instantiated copy of type expression

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

Instantiate symbol with copy of denoted symbol.

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

Instantiate symbol with copy of denoted symbol.

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

instantiate() - Method in interface fmrisc.Syntax.Selector

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

create instantiated copy of declaration

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

returns instantiated copy of identifier

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

create instantiated copy of identifier

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

create instantiated copy of declaration

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

returns instantiated copy of identifier

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

instantiateType() - Method in interface fmrisc.Syntax.Type

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

Instantiating - Class in fmrisc.Proving

Extending a proof state by instantiating quantified formulas.

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

InvalidAnswer - Class in fmrisc.Proving

Answer that formula is invalid.

InvalidAnswer(String) - Constructor for class fmrisc.Proving.InvalidAnswer

Create answer that formula is valid with denoted justification.

InvalidAnswerCVCL - Class in fmrisc.Proving.CVCL

Answer that formula is invalid.

InvalidAnswerCVCL(CVCL, String) - Constructor for class fmrisc.Proving.CVCL.InvalidAnswerCVCL

Create answer that formula is valid with denoted justification.

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

Get prover abort state.

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

Is proof absolute?

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

Return axiom status of formula.

isBoolean(Type) - Static method in class fmrisc.Semantics.Checking

checks if type equals BOOLEAN

isCloned() - Method in class fmrisc.Proving.Rewriting

Visitor functions.

isCloned() - Method in class fmrisc.Proving.Substitute

Signal that visitor shall clone tree.

isCloned() - Method in interface fmrisc.Syntax.ASTVisitor

Signal whether tree is to be cloned.

isCloned() - Method in class fmrisc.Syntax.ASTVisitorBase

Signal whether tree is to be cloned.

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

Is proof closed?

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

check whether proof state is closed

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

get formula isGoal

isInt(Type) - Static method in class fmrisc.Semantics.Checking

checks if type equals INT

isNat(Type) - Static method in class fmrisc.Semantics.Checking

checks if type equals NAT

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

true iff CVCL instance is okay

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

true iff prover is okay after creation

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

check whether substitution was referenced

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

Check whether program is to be restarted.

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

Signal whether command is being processed.

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

Is proof skeleton?

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

Is proof trusted?