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

P

param(Vector) - Method in class fmrisc.ProofNavigator.PNParser

param(Vector) - Method in class fmrisc.Proving.CVCL.CVCLParser

paramList() - Method in class fmrisc.ProofNavigator.PNParser

paramList() - Method in class fmrisc.Proving.CVCL.CVCLParser

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

Parse next command.

parseExpression(String) - Method in class fmrisc.Proving.CVCL.CVCL

Parse CVCL String as an expression.

parseInt(String) - Static method in class fmrisc.Semantics.Checking

get number from digit representation

PERIOD - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

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

PLUS - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

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

construct binary sum with components base1 and base2

PlusTerm - Class in fmrisc.Syntax

Handling of binary sums.

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

construct binary sum with components base1 and base2

PNLexer - Class in fmrisc.ProofNavigator

PNLexer(InputStream) - Constructor for class fmrisc.ProofNavigator.PNLexer

PNLexer(Reader) - Constructor for class fmrisc.ProofNavigator.PNLexer

PNLexer(InputBuffer) - Constructor for class fmrisc.ProofNavigator.PNLexer

PNLexer(LexerSharedInputState) - Constructor for class fmrisc.ProofNavigator.PNLexer

PNParser - Class in fmrisc.ProofNavigator

PNParser(TokenBuffer) - Constructor for class fmrisc.ProofNavigator.PNParser

PNParser(TokenStream) - Constructor for class fmrisc.ProofNavigator.PNParser

PNParser(ParserSharedInputState) - Constructor for class fmrisc.ProofNavigator.PNParser

PNParserTokenTypes - Interface in fmrisc.ProofNavigator

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

End subcontext for formula assertions.

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

End subcontext for formula assertions.

POWER - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

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

construct power term with components base1 and base2

PowerTerm - Class in fmrisc.Syntax

Handling of power terms.

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

construct power term with components base1 and base2

Presenter - Class in fmrisc.Communication

Interface to visual presentation of declarations and proof states.

Presenter(File) - Constructor for class fmrisc.Communication.Presenter

Create instance of presenter with files in denoted directory.

PrettyMathML - Class in fmrisc.Communication

Conversion of AST to HTML/MathML presentation markup (pretty-printed).

PrettyMathML(Document, int) - Constructor for class fmrisc.Communication.PrettyMathML

Create converter that creates DOM nodes in the specified document.

PrettyMathML(Document) - Constructor for class fmrisc.Communication.PrettyMathML

Create converter that creates DOM nodes in the specified document.

PrettyPrinter - Class in fmrisc.Communication

Printing abstract syntax trees with appropriate line breaks.

PrettyPrinter(int, PrintWriter) - Constructor for class fmrisc.Communication.PrettyPrinter

Create pretty printer to print abstract syntax trees.

PrettyPrinter(PrintWriter) - Constructor for class fmrisc.Communication.PrettyPrinter

Create pretty printer for default width WIDTH.

Prev - Class in fmrisc.ProofNavigator.Commands

The "prev" command: goto previous open proof state.

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

Create a "prev" command.

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

switch current state to previous open state in sequence.

print(Declaration) - Method in class fmrisc.Communication.PrettyPrinter

Pretty-print declaration.

print(Expression) - Method in class fmrisc.Communication.PrettyPrinter

Pretty-print expression.

print(Type) - Method in class fmrisc.Communication.PrettyPrinter

Pretty-print type.

print(String) - Method in class fmrisc.Communication.PrettyPrinter

Print text.

print(AST, PrintWriter) - Static method in class fmrisc.Proving.CVCL.CVCLPrinter

Print abstract syntax tree in CVCL syntax.

print(PrintWriter) - Method in class fmrisc.Proving.Formula

print formula on output stream as "[label] formula"

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

Print proof.

print(PrintWriter) - Method in class fmrisc.Proving.ProofState

print proof state on output stream

print(PrintWriter, int) - Method in class fmrisc.Proving.ProofState

Print proof state including children.

print(PrintWriter) - Method in class fmrisc.Syntax.ApplicationExpression

Prints text representation on out (without new line termination).

print(PrintWriter) - Method in interface fmrisc.Syntax.AST

Prints text representation of tree on out (without new line termination).

print(PrintWriter) - Method in class fmrisc.Syntax.ASTBase

Prints text representation on out (without new line termination).

print(PrintWriter) - Method in class fmrisc.Syntax.DeclarationBase

Prints text representation of declaration.

print(PrintWriter) - Method in class fmrisc.Syntax.FormulaDeclIdentifier

Prints text representation on out (without new line termination).

print(PrintWriter) - Method in class fmrisc.Syntax.Identifier

Prints text representation on out (without new line termination).

print(PrintWriter) - Method in class fmrisc.Syntax.Logical

Prints text representation on out (without new line termination).

print(PrintWriter) - Method in class fmrisc.Syntax.Number

Prints text representation of tree on out (without new line termination).

print(PrintWriter) - Method in class fmrisc.Syntax.Reference

Prints text representation on out (without new line termination).

print(PrintWriter) - Method in class fmrisc.Syntax.SelectorBase

Prints text representation of selector expression.

print(PrintWriter) - Method in class fmrisc.Syntax.TupleTerm

Prints text representation on out (without new line termination).

print(PrintWriter) - Method in class fmrisc.Syntax.TypeBase

Prints text representation of type expression.

print(PrintWriter) - Method in class fmrisc.Syntax.TypeDeclIdentifier

Prints text representation on out (without new line termination).

print(PrintWriter) - Method in class fmrisc.Syntax.TypedIdentifier

Prints text representation.

print(PrintWriter) - Method in class fmrisc.Syntax.ValueDeclIdentifier

Prints text representation on out (without new line termination).

print(PrintWriter) - Method in class fmrisc.Syntax.ValuedIdentifier

Prints text representation.

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Assume

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Auto

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.AutoStar

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Case

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.CommandBase

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.ContextC

print command

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.CounterExample

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.DeclarationC

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Decompose

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Empty

print command

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.EnvironmentC

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Expand

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Flatten

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Flip

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.FormulaC

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Goal

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Goto

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Induction

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Instantiate

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Lemma

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Next

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Open

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Option

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Prev

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.ProofC

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Prove

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Proved

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Quit

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Read

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Redo

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Scatter

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Simplify

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Skolemize

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Split

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.StateC

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.TCC

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.TypeAxiom

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.TypeC

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.Undo

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.ProofNavigator.Commands.ValueC

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.ApplicationExpression

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.ArrayType

Prints text representation of type on out (without new line termination).

printCore(PrintWriter) - Method in interface fmrisc.Syntax.AST

Like print, but parentheses around outer expression are not printed.

printCore(PrintWriter) - Method in class fmrisc.Syntax.ASTBase

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.AtomicType

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.AxiomDeclaration

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.BinaryExpression

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.DividesTerm

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.EquivalentFormula

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.ExistsFormula

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.ForallFormula

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.FormulaDeclaration

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.FormulaDeclIdentifier

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.FunctionType

Prints text representation of type on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.Identifier

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.IfThenElseExpression

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.ImpliesFormula

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.LetExpression

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.LetType

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.Logical

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.NotEquivalentFormula

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.Number

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.PowerTerm

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.QuantifiedExpression

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.RecordTerm

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.RecordType

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.Reference

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.SelectionTerm

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.SelectorIdentifier

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.SelectorIndex

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.SelectorNumber

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.SubrangeType

Prints text representation of type on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.SubType

Prints text representation of type on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.TupleTerm

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.TupleType

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.TypeDeclaration

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.TypeDeclIdentifier

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.TypedIdentifier

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.UnaryExpression

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.UpdateTerm

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.ValueDeclaration

Prints text representation of tree on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.ValueDeclIdentifier

Prints text representation on out (without new line termination).

printCore(PrintWriter) - Method in class fmrisc.Syntax.ValuedIdentifier

Prints text representation on out (without new line termination).

printParens(PrintWriter) - Method in interface fmrisc.Syntax.AST

Like print, but parentheses around outer expression are always printed.

printParens(PrintWriter) - Method in class fmrisc.Syntax.ASTBase

Prints text representation on out (without new line termination) with parentheses around the whole expression.

printPriority(int, PrintWriter) - Method in interface fmrisc.Syntax.Expression

print expression, use parentheses if priority is greater than treshold

printPriority(int, PrintWriter) - Method in class fmrisc.Syntax.ExpressionBase

print expression, use parentheses if priority is greater than treshold

printPriority(int, PrintWriter) - Method in class fmrisc.Syntax.Identifier

print expression, use parentheses if priority is greater than treshold

printPriority(int, PrintWriter) - Method in class fmrisc.Syntax.Number

print expression, use parentheses if priority is greater than treshold

printStatus(PrintWriter) - Method in class fmrisc.Proving.Proof

Print status of proof to out

process() - Method in interface fmrisc.ProofNavigator.Commands.Command

process command

process() - Method in class fmrisc.ProofNavigator.Commands.ContextC

Process command "newcontext": only executed in declaration mode.

process() - Method in class fmrisc.ProofNavigator.Commands.DeclarationC

Process declaration.

process() - Method in class fmrisc.ProofNavigator.Commands.Empty

Process command "empty": do nothing.

process() - Method in class fmrisc.ProofNavigator.Commands.EnvironmentC

Process command "environment": show environment (global or of current state).

process() - Method in class fmrisc.ProofNavigator.Commands.FormulaC

Process command "formula": print value of formula identifier.

process() - Method in class fmrisc.ProofNavigator.Commands.Option

override method to allow command also to be processed when not in proof

process() - Method in class fmrisc.ProofNavigator.Commands.ProofC

Process command: print proof of formula respectively current proof

process(ProofState) - Method in interface fmrisc.ProofNavigator.Commands.ProofCommand

process proof state.

process(ProofState) - Method in class fmrisc.ProofNavigator.Commands.ProofCommandBase

process proof state (in environment denoted by that state).

process() - Method in class fmrisc.ProofNavigator.Commands.ProofCommandBase

apply command to current state of current proof.

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

process command "prove f": start proof of formula denoted by identifier f.

process() - Method in class fmrisc.ProofNavigator.Commands.Quit

process command "quit".

process() - Method in class fmrisc.ProofNavigator.Commands.Read

Process command "read": only executed in declaration mode.

process() - Method in class fmrisc.ProofNavigator.Commands.StateC

Process command "state": show denoted state.

process() - Method in class fmrisc.ProofNavigator.Commands.TCC

process command "tcc".

process() - Method in class fmrisc.ProofNavigator.Commands.TypeC

Process command "type": print value of type identifier.

process() - Method in class fmrisc.ProofNavigator.Commands.ValueC

Process command "value": print value of value identifier.

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

Process command denoted by string.

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

Process command.

process(String) - Method in class fmrisc.ProofNavigator.SWT.Top

Process command denoted by command string.

process(Expression) - Static method in class fmrisc.Semantics.Checking

type check value

Proof - Class in fmrisc.Proving

ProofC - Class in fmrisc.ProofNavigator.Commands

Command "proof": print proof tree.

ProofC(Identifier) - Constructor for class fmrisc.ProofNavigator.Commands.ProofC

Create a "proof" command.

ProofCommand - Interface in fmrisc.ProofNavigator.Commands

Interface to proof commands.

ProofCommandBase - Class in fmrisc.ProofNavigator.Commands

Base class of proof commands.

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

construct proof command with denoted name.

ProofState - Class in fmrisc.Proving

The state of a proof.

ProofState(Proof, Environment, Expression, boolean) - Constructor for class fmrisc.Proving.ProofState

construct a root state from a single goal and without assumptions

ProofState(ProofState, Environment) - Constructor for class fmrisc.Proving.ProofState

construct a proof state without path and formulas yet

ProofState(Proof) - Constructor for class fmrisc.Proving.ProofState

Construct a skeleton proof state (all fields but the proof remain uninitialized).

ProofStateListener - Interface in fmrisc.Proving

ProofTree - Class in fmrisc.ProofNavigator.SWT

Graphical representation of proof.

ProofTree(Composite) - Constructor for class fmrisc.ProofNavigator.SWT.ProofTree

Construct proof tree for denoted parent component and with denoted style..

ProofTreeItem - Class in fmrisc.ProofNavigator.SWT

Graphical representation of proof state.

ProofUtil - Class in fmrisc.Proving

Proving utilities.

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

Prove - Class in fmrisc.ProofNavigator.Commands

"prove": prove goal formula.

Prove(Identifier) - Constructor for class fmrisc.ProofNavigator.Commands.Prove

create a prove command

Proved - Class in fmrisc.ProofNavigator.Commands

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

create a "proved" command.

Prover - Interface in fmrisc.Proving

ProverReasoning - Class in fmrisc.Proving

Reasoning with the help of an external prover.

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

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

Start a new subcontext for formula assertions.

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

Start a new subcontext for formula assertions.

put(ValueDeclIdentifier) - Method in class fmrisc.Semantics.Environment

add the symbol associated to ident to current environment

put(FormulaDeclIdentifier, Expression, boolean, Environment) - Method in class fmrisc.Semantics.FormulaTable

put formula in formula table

put(TypeDeclIdentifier, Type) - Method in class fmrisc.Semantics.TypeTable

put type in type table

put(ValueDeclIdentifier, Type, Expression, int) - Method in class fmrisc.Semantics.ValueTable

put named value in value table

putFormula(FormulaDeclIdentifier, Expression, boolean) - Method in class fmrisc.Semantics.Environment

put formula in environment

putFormulaDeclaration(FormulaDeclaration) - Method in class fmrisc.Semantics.Environment

put formula declaration into environment

putType(TypeDeclIdentifier, Type) - Method in class fmrisc.Semantics.Environment

put type in type table

putTypeDeclaration(TypeDeclaration) - Method in class fmrisc.Semantics.Environment

put type declaration into environment

putValue(ValueDeclIdentifier, Type, Expression) - Method in class fmrisc.Semantics.Environment

put named value in value table

putValueDeclaration(ValueDeclaration) - Method in class fmrisc.Semantics.Environment

put value declaration into environment

putVariables(TypedIdentifier[]) - Method in class fmrisc.Semantics.Environment

put variables into environment