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

A

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

Abort current prover activity.

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

Abort current prover activity.

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

return to the parent context discarding all the formulas that were added to the subcontext since the last call of open().

accept(ASTVisitor) - Method in class fmrisc.Syntax.ApplicationExpression

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.ArrayType

Accept visitor for a visit.

accept(ASTVisitor) - Method in interface fmrisc.Syntax.AST

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.AtomicType

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.AxiomDeclaration

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.BinaryExpression

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.FormulaDeclaration

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.FormulaDeclIdentifier

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.FunctionType

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.IfThenElseExpression

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.LetExpression

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.LetType

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.Logical

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.Number

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.QuantifiedExpression

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.RecordTerm

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.RecordType

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.Reference

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.SelectionTerm

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.SelectorIdentifier

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.SelectorIndex

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.SelectorNumber

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.SubrangeType

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.SubType

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.TupleTerm

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.TupleType

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.TypeDeclaration

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.TypeDeclIdentifier

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.TypedIdentifier

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.UnaryExpression

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.UpdateTerm

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.ValueDeclaration

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.ValueDeclIdentifier

Accept visitor for a visit.

accept(ASTVisitor) - Method in class fmrisc.Syntax.ValuedIdentifier

Accept visitor for a visit.

add(Formula[], Formula) - Method in class fmrisc.Proving.ProofState

Adds a formula to a sequence of formulas in this state.

add(Formula[], Formula[]) - Method in class fmrisc.Proving.ProofState

Adds a sequence of formulas to a sequence of formulas in this state.

addDeclaration(Declaration) - Method in class fmrisc.Proving.CVCL.CVCL

Add declaration.

addDeclaration(Declaration) - Method in interface fmrisc.Proving.Prover

add declaration

addOpen(Vector) - Method in class fmrisc.Proving.ProofState

Add open state and all open children recursively to vector.

addTCC(Expression) - Method in class fmrisc.Semantics.Environment

Add type checking condition to environment.

AndFormula - Class in fmrisc.Syntax

Handling of conjunctions.

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

construct conjunction with components base1 and base2

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

construct conjunction with components base1 and base2

Answer - Interface in fmrisc.Proving

Interface to prover answers.

AnswerBase - Class in fmrisc.Proving

Base class of prover answers.

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

Create answer with denoted justification.

APHash(String) - Static method in class fmrisc.External.GeneralHashFunctionLibrary

append(String) - Method in class fmrisc.ProofNavigator.SWT.TextInputStream

Append text to buffer and notify waiting reader.

append(Expression, Vector) - Static method in class fmrisc.Semantics.FreeVariables

Compute free variables of expression.

appendDecl(Node, Declaration) - Method in class fmrisc.Communication.MathML

Convert declaration to DOM representation of HTML/MathML markup.

appendDecl(Node, Declaration) - Method in class fmrisc.Communication.PrettyMathML

Convert declaration to DOM representation of HTML/MathML markup.

appendExp(Node, Expression) - Method in class fmrisc.Communication.MathML

Convert expression to DOM representation of HTML/MathML markup.

appendExp(Node, Expression) - Method in class fmrisc.Communication.PrettyMathML

Convert expression to DOM representation of HTML/MathML markup.

appendIdentifier(Node, Identifier) - Method in class fmrisc.Communication.MathML

Convert identifier to DOM representation of HTML/MathML markup.

appendPunctuation(Node, String) - Method in class fmrisc.Communication.MathML

Append to parent operator node with denoted text.

appendType(Node, Type) - Method in class fmrisc.Communication.MathML

Convert type to DOM representation of HTML/MathML markup.

appendTypedIdentifier(Node, TypedIdentifier) - Method in class fmrisc.Communication.MathML

Convert typed identifier to DOM representation of HTML/MathML markup.

appendTypedIdentifier(Node, TypedIdentifier) - Method in class fmrisc.Communication.PrettyMathML

Convert typed identifier to DOM representation of HTML/MathML markup.

ApplicationExpression - Class in fmrisc.Syntax

Handling of function and predicate applications.

ApplicationExpression(Expression, Expression[]) - Constructor for class fmrisc.Syntax.ApplicationExpression

construct application of fun to args

applicationExpression(Expression, Expression[]) - Static method in class fmrisc.Syntax.Construct

construct application of base1 to base2

ArrayTerm - Class in fmrisc.Syntax

Handling of array terms.

ArrayTerm(TypedIdentifier[], Expression) - Constructor for class fmrisc.Syntax.ArrayTerm

construct array term of variables and base term

arrayTerm(TypedIdentifier[], Expression) - Static method in class fmrisc.Syntax.Construct

construct array term of variables and base term

ArrayType - Class in fmrisc.Syntax

Handling of array types.

ArrayType(Type, Type) - Constructor for class fmrisc.Syntax.ArrayType

construct array type with denoted index type and base type.

arrayType(Type, Type) - Static method in class fmrisc.Syntax.Construct

construct array type with denoted index type and base type.

ARROW - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

ask(String) - Static method in class fmrisc.ProofNavigator.Main

Ask question to be answered by user with 'y' or 'n'

assertAxiom(Expression) - Method in class fmrisc.Proving.CVCL.CVCL

assert axiom about previously asserted declarations.

assertAxiom(Expression) - Method in interface fmrisc.Proving.Prover

assert axiom about previously asserted declarations.

assertFormula(Expression) - Method in class fmrisc.Proving.CVCL.CVCL

Assert truth of formula.

assertFormula(Expression) - Method in interface fmrisc.Proving.Prover

assert truth of formula.

ASSIGNMENT - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

Assume - Class in fmrisc.ProofNavigator.Commands

Commnand "assume": split proof state by an assumption and its proof.

Assume(Expression) - Constructor for class fmrisc.ProofNavigator.Commands.Assume

Create an "assume" command.

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

add an assumption to the current (sub)context

AST - Interface in fmrisc.Syntax

Interface to abstract syntax trees.

ASTBase - Class in fmrisc.Syntax

Base class of abstract syntax trees.

ASTBase() - Constructor for class fmrisc.Syntax.ASTBase

ASTUtil - Class in fmrisc.Syntax

Collect state related to handling of abstract syntax trees.

ASTUtil() - Constructor for class fmrisc.Syntax.ASTUtil

ASTVisitor - Interface in fmrisc.Syntax

Interface to visitor of abstract syntax trees.

ASTVisitorBase - Class in fmrisc.Syntax

Base class of visitors of abstract syntax trees.

ASTVisitorBase() - Constructor for class fmrisc.Syntax.ASTVisitorBase

AtomicType - Class in fmrisc.Syntax

Handling of atomic types.

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

construct atomic type with denoted name.

atomicType(String) - Static method in class fmrisc.Syntax.Construct

construct atomic type with denoted name.

Auto - Class in fmrisc.ProofNavigator.Commands

Command "auto": try to close state by automatic instantiation of quantified formulas.

Auto(String[]) - Constructor for class fmrisc.ProofNavigator.Commands.Auto

Create a "auto" command.

AutoStar - Class in fmrisc.ProofNavigator.Commands

command "autostar": apply auto to current node and its successor siblings.

AutoStar() - Constructor for class fmrisc.ProofNavigator.Commands.AutoStar

Create a "autostar" command.

available() - Method in class fmrisc.ProofNavigator.SWT.TextInputStream

Get number of bytes available on stream.

AxiomDeclaration - Class in fmrisc.Syntax

Handling of type declarations.

AxiomDeclaration(FormulaDeclIdentifier, Expression) - Constructor for class fmrisc.Syntax.AxiomDeclaration

Construct axiom declaration with denoted name and formula.

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

construct axiom declaration with denoted name and formula