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

F

Flatten - Class in fmrisc.ProofNavigator.Commands

Command "flatten": decompose compound formulas without splitting the state.

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

create a "flatten" command

Flip - Class in fmrisc.ProofNavigator.Commands

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

create a "flip" command

fmrisc.Communication - package fmrisc.Communication

fmrisc.External - package fmrisc.External

fmrisc.ProofNavigator - package fmrisc.ProofNavigator

fmrisc.ProofNavigator.Commands - package fmrisc.ProofNavigator.Commands

fmrisc.ProofNavigator.SWT - package fmrisc.ProofNavigator.SWT

fmrisc.Proving - package fmrisc.Proving

fmrisc.Proving.CVCL - package fmrisc.Proving.CVCL

fmrisc.Semantics - package fmrisc.Semantics

fmrisc.Syntax - package fmrisc.Syntax

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

construct universally quantifed formula of variables and base formula

ForallFormula - Class in fmrisc.Syntax

Handling of universally quantified formulas.

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

construct forall formula of variables and base formula

Formula - Class in fmrisc.Proving

A formula occuring in a proof state.

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

construct a formula from an expression

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

construct a copy of the given formula in the denoted state

FormulaC - Class in fmrisc.ProofNavigator.Commands

Command "formula": print value of formula identifier.

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

Create a "formula" command.

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

construct formula declaration with denoted name and formula.

FormulaDeclaration - Class in fmrisc.Syntax

Handling of type declarations.

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

construct formula declaration with denoted name and formula

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

construct formula declaration identifier with denoted name.

FormulaDeclIdentifier - Class in fmrisc.Syntax

Handling of identifiers used in type declarations

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

construct identifier from name

FormulaSymbol - Class in fmrisc.Semantics

Entries in FormulaTable.

FormulaSymbol(FormulaDeclIdentifier) - Constructor for class fmrisc.Semantics.FormulaSymbol

Construct formula symbol from ident (type is set to null).

FormulaTable - Class in fmrisc.Semantics

Symbol table for formulas.

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

FreeVariables - Class in fmrisc.Semantics

Compute the free variables of an expression.

functionType(Type[], Type) - Static method in class fmrisc.Syntax.Construct

construct function type from types domain and range.

FunctionType - Class in fmrisc.Syntax

Handling of function type expressions

FunctionType(Type[], Type) - Constructor for class fmrisc.Syntax.FunctionType

construct function type from domain and range.