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

C

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

Returns canonical version of type (equality of two types implies the equality of the canonical version of the types).

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

Returns canonical version of type (equality of two types implies the equality of the canonical version of the types).

canonicalText(AST) - Static method in class fmrisc.Syntax.ASTUtil

get canonical text of expression (variable names replaced by numbers).

Case - Class in fmrisc.ProofNavigator.Commands

The "case" command: split state into multiple cases.

Case(Expression[]) - Constructor for class fmrisc.ProofNavigator.Commands.Case

Create a "case" command.

changeLevel(boolean, PrettyMathML.Parent) - Method in class fmrisc.Communication.PrettyMathML

Change indentation level.

changeLevel(boolean) - Method in class fmrisc.Communication.PrettyPrinter

Change indentation level.

Checking - Class in fmrisc.Semantics

type checking routines

Checking() - Constructor for class fmrisc.Semantics.Checking

clearSubtypes(Type, Expression) - Static method in class fmrisc.Semantics.Checking

return version of type where subtypes and subranges (including NAT) are replaced by their base types; the corresponding constraints are returned as a formula which a corresponding expression exp has to fulfill

cloneFormulaTable() - Method in class fmrisc.Semantics.FormulaTable

creates a clone of the symbol table, the clone is a shallow copy (the symbols in the table are not cloned)

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

Create clone of global part of environment; the clone is a shallow copy (the symbols in the environment are not cloned).

cloneTable(SymbolTable) - Method in class fmrisc.Semantics.SymbolTable

makes s a clone of the symbol table, the clone is a shallow copy (the symbols in the table are not cloned)

cloneTypeTable() - Method in class fmrisc.Semantics.TypeTable

creates a clone of the symbol table, the clone is a shallow copy (the symbols in the table are not cloned)

cloneValueTable() - Method in class fmrisc.Semantics.ValueTable

creates a clone of the symbol table, the clone is a shallow copy (the symbols in the table are not cloned)

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

close stream

close(ProofState) - Method in class fmrisc.Proving.Proof

Inform proof that state was closed.

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

close the state.

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

close formula on top of formula stack with respect to current scope.

COLON - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

COMMA - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

Command - Interface in fmrisc.ProofNavigator.Commands

Interface to commands.

CommandBase - Class in fmrisc.ProofNavigator.Commands

Base class of commands.

CommandBase(String) - Constructor for class fmrisc.ProofNavigator.Commands.CommandBase

construct command with denoted name

CommandServer - Class in fmrisc.Communication

Server handling commands received as HTTP requests.

CommandServer() - Constructor for class fmrisc.Communication.CommandServer

Creates a new command server (which is already started).

COMMENT - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

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

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

compute(AST, boolean) - Static method in class fmrisc.Communication.BreakInfo

Construct the line break information for the denoted tree.

compute(Expression) - Static method in class fmrisc.Proving.GroundExpressions

Compute collection of all ground subexpressions of an expression.

compute(ProofState) - Static method in class fmrisc.Proving.GroundExpressions

Compute collection of ground subexpressions of a proof state.

compute(Expression) - Static method in class fmrisc.Semantics.BoundVariables

Compute variables bound some quantifier within an expression.

compute(Expression) - Static method in class fmrisc.Semantics.FreeVariables

Compute free variables of expression.

compute(Type) - Static method in class fmrisc.Semantics.FreeVariables

Compute free variables of type.

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

The status of this proof or of the proof of a formula on which this proof depends may has changed.

construct(Expression, Expression) - Method in class fmrisc.Syntax.AndFormula

Construct binary expression of the same kind as this expression.

construct(TypedIdentifier[], Expression) - Method in class fmrisc.Syntax.ArrayTerm

Construct quantified expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.BinaryExpression

Construct binary expression of the same kind as this expression.

Construct - Class in fmrisc.Syntax

Construct abstract syntax trees.

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

construct(Expression, Expression) - Method in class fmrisc.Syntax.DividesTerm

Construct binary expression of the same kind as this expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.EqualsFormula

Construct binary expression of the same kind as this expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.EquivalentFormula

Construct binary expression of the same kind as this expression.

construct(TypedIdentifier[], Expression) - Method in class fmrisc.Syntax.ExistsFormula

Construct quantified expression.

construct(TypedIdentifier[], Expression) - Method in class fmrisc.Syntax.ForallFormula

Construct quantified expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.GreaterEqualFormula

Construct binary expression of the same kind as this expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.GreaterFormula

Construct binary expression of the same kind as this expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.ImpliesFormula

Construct binary expression of the same kind as this expression.

construct(TypedIdentifier[], Expression) - Method in class fmrisc.Syntax.LambdaTerm

Construct quantified expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.LessEqualFormula

Construct binary expression of the same kind as this expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.LessFormula

Construct binary expression of the same kind as this expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.MinusTerm

Construct binary expression of the same kind as this expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.NotEqualsFormula

Construct binary expression of the same kind as this expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.NotEquivalentFormula

Construct binary expression of the same kind as this expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.OrFormula

Construct binary expression of the same kind as this expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.PlusTerm

Construct binary expression of the same kind as this expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.PowerTerm

Construct binary expression of the same kind as this expression.

construct(TypedIdentifier[], Expression) - Method in class fmrisc.Syntax.QuantifiedExpression

Construct quantified expression.

construct(Expression, Expression) - Method in class fmrisc.Syntax.TimesTerm

Construct binary expression of the same kind as this expression.

Context - Class in fmrisc.Semantics

handling of formula contexts

Context() - Constructor for class fmrisc.Semantics.Context

construct a new context empty of assumptions

ContextC - Class in fmrisc.ProofNavigator.Commands

Command "newcontext": change context to denoted path.

ContextC(String) - Constructor for class fmrisc.ProofNavigator.Commands.ContextC

Create a "newcontext" command.

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

Copy a sequence of formulas in this state.

CounterExample - Class in fmrisc.ProofNavigator.Commands

Command "counterexample": show potential counterexample for current state (may be time-consuming)

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

Create a "counterexample" command.

createMathNode(Document) - Static method in class fmrisc.Communication.MathML

Create MathML node in document.

cut(ProofState) - Method in class fmrisc.Proving.Proof

Cut proof at denoted state.

CVCL - Class in fmrisc.Proving.CVCL

CVC Lite interface

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

Create CVCL instance by call of command

CVCLFormulaMask - Class in fmrisc.Proving.CVCL

CVCLFormulaMask() - Constructor for class fmrisc.Proving.CVCL.CVCLFormulaMask

Create formula mask with initial context.

CVCLLexer - Class in fmrisc.Proving.CVCL

CVCLLexer(CVCL, Reader) - Constructor for class fmrisc.Proving.CVCL.CVCLLexer

CVCLLexer(InputStream) - Constructor for class fmrisc.Proving.CVCL.CVCLLexer

CVCLLexer(Reader) - Constructor for class fmrisc.Proving.CVCL.CVCLLexer

CVCLLexer(InputBuffer) - Constructor for class fmrisc.Proving.CVCL.CVCLLexer

CVCLLexer(LexerSharedInputState) - Constructor for class fmrisc.Proving.CVCL.CVCLLexer

CVCLParser - Class in fmrisc.Proving.CVCL

CVCLParser(CVCL, CVCLLexer) - Constructor for class fmrisc.Proving.CVCL.CVCLParser

CVCLParser(TokenBuffer) - Constructor for class fmrisc.Proving.CVCL.CVCLParser

CVCLParser(TokenStream) - Constructor for class fmrisc.Proving.CVCL.CVCLParser

CVCLParser(ParserSharedInputState) - Constructor for class fmrisc.Proving.CVCL.CVCLParser

CVCLParserTokenTypes - Interface in fmrisc.Proving.CVCL

CVCLPrinter - Class in fmrisc.Proving.CVCL

Printing abstract syntax trees in CVLC syntax.