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

S

Scatter - Class in fmrisc.ProofNavigator.Commands

command "scatter": scatter proof state by repeated decomposition and goalsplitting.

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

create a "scatter" command

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

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

construct component selection from base1 and base2

SelectionTerm - Class in fmrisc.Syntax

Handling of component access by index selections.

SelectionTerm(Expression, Selector) - Constructor for class fmrisc.Syntax.SelectionTerm

construct component selection from base1 and base2

Selector - Interface in fmrisc.Syntax

Interface to selectors.

SelectorBase - Class in fmrisc.Syntax

Base class of selector expressions.

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

selectorIdentifier(Reference) - Static method in class fmrisc.Syntax.Construct

make selector from identifier base

SelectorIdentifier - Class in fmrisc.Syntax

Identifier as selector.

SelectorIdentifier(Reference) - Constructor for class fmrisc.Syntax.SelectorIdentifier

make selector from identifier base

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

make selector from index expression base

SelectorIndex - Class in fmrisc.Syntax

General index expression as selector.

SelectorIndex(Expression) - Constructor for class fmrisc.Syntax.SelectorIndex

make selector from general index expression

selectorNumber(Number) - Static method in class fmrisc.Syntax.Construct

make selector from number base

SelectorNumber - Class in fmrisc.Syntax

Number as selector.

SelectorNumber(Number) - Constructor for class fmrisc.Syntax.SelectorNumber

make selector from number base

SEMICOLON - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

setAborted(boolean) - Static method in class fmrisc.ProofNavigator.State

Set prover abort state.

setAbsolute(boolean) - Method in class fmrisc.Proving.Proof

Signal whether proof is closed.

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

set assumptions of proof state

setAutoSimplify(boolean) - Static method in class fmrisc.ProofNavigator.State

Turn on/off automatic simplification

setAutoSimplify(boolean) - Method in class fmrisc.Proving.ProofState

Set automatic simplification status of proof state

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

Set axiom status of formula to true.

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

Set axioms of proof state.

setBase(Type) - Method in class fmrisc.Syntax.SubType

set base type

setBigFont(boolean) - Static method in class fmrisc.ProofNavigator.State

Set font size.

setChildren(Command, ProofState[]) - Method in class fmrisc.Proving.ProofState

set children of proof state

setClearType(TypeExpression) - Method in class fmrisc.Semantics.ValueSymbol

Set clear type to typexp.

setClosed(boolean) - Method in class fmrisc.Proving.Proof

Signal whether proof is closed.

setCommand(Command) - Method in class fmrisc.Proving.ProofState

set command of proof state

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

Set context directory.

setCounterExample(Expression[]) - Method in class fmrisc.Proving.ProofState

Set counterexample for state.

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

set current open proof state

setDepth(int) - Method in class fmrisc.Semantics.ValueSymbol

Set environment depth of symbol.

setEnvironment(Environment) - Static method in class fmrisc.ProofNavigator.State

set environment used by proof navigator

setEnvironment(Environment) - Method in class fmrisc.Proving.ProofState

set environment of proof state

setEnvironment(Environment) - Method in class fmrisc.Semantics.FormulaSymbol

Set environment of symbol (up to the point where the symbol was decld).

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

set error message, does not override previously set message

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

set error message

setExpression(Expression) - Method in class fmrisc.Proving.Formula

Set formula expression.

setExpression(Expression) - Method in class fmrisc.Semantics.TypeExpression

set exp

setFormula(Expression) - Method in class fmrisc.Semantics.FormulaSymbol

Set formula of symbol.

setFormulaMask(CVCLFormulaMask) - Static method in class fmrisc.ProofNavigator.State

Set formula mask.

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

set goals of proof state

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

Set focus to input field.

setInputFocus() - Method in class fmrisc.ProofNavigator.SWT.Top

Set focus to input field.

setLabels(boolean) - Static method in class fmrisc.ProofNavigator.State

signal that lexer shall produce labels rather than idents

setLastTCC(Expression) - Static method in class fmrisc.ProofNavigator.State

set last type checking condition

setLexer(PNLexer) - Static method in class fmrisc.ProofNavigator.State

set lexer used by proof navigator

setListener(ProofStateListener) - Method in class fmrisc.Proving.ProofState

Set listener that is notified when proof state has changed.

setName(String) - Method in class fmrisc.Syntax.Identifier

set name of identifier

setNamespacePrefix(String) - Method in class fmrisc.External.NewOMDOMWriter

Set the namespace prefix.

setNodes(Tree, ProofState) - Static method in class fmrisc.ProofNavigator.SWT.ProofTreeItem

Set tree to visualize the state tree with the denoted root state.

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

set parent of proof state

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

set path of proof state

setPrintParens(boolean) - Static method in class fmrisc.Syntax.ASTUtil

signal whether every (sub)expression is to be printed with enclosing parentheses

setPrintUnique(boolean) - Static method in class fmrisc.Syntax.ASTUtil

signal whether every identifier is printed with its unique name

setPrintVarNumber(boolean) - Static method in class fmrisc.Syntax.ASTUtil

signal whether every identifier is printed with its variable number

setProof(Proof) - Static method in class fmrisc.ProofNavigator.Main

Signal current proof.

setProof(Proof) - Static method in class fmrisc.ProofNavigator.State

set current proof

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

Set current proof.

setProof(Proof) - Method in class fmrisc.ProofNavigator.SWT.ProofTree

Change tree to visualize denoted proof.

setProof(Proof) - Method in class fmrisc.ProofNavigator.SWT.Top

Set the current proof.

setProof(Proof) - Method in class fmrisc.Semantics.FormulaSymbol

Set proof of symbol.

setProofState(ProofState) - Static method in class fmrisc.ProofNavigator.Main

Signal current proof state.

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

Signal current proof state.

setProofState(ProofState) - Method in class fmrisc.ProofNavigator.SWT.Top

Signal current proof state.

setReplayChildren(ProofState[]) - Static method in class fmrisc.ProofNavigator.State

Set children of current proof state during proof replay.

setRunning(boolean) - Method in class fmrisc.ProofNavigator.SWT.ProofTree

Signal run status of background process.

setRunningProver(Prover) - Static method in class fmrisc.ProofNavigator.State

Set prover currently running.

setServerPort(int) - Static method in class fmrisc.ProofNavigator.State

Set server port.

setSkeleton(boolean) - Method in class fmrisc.Proving.Proof

Signal whether proof is skeleton.

setStrongerTypes(boolean) - Static method in class fmrisc.Semantics.Checking

signals whether stronger type discipline is to be preserved

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

set substitution type for instantiation

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

set substitution expression for instantiation

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

set substitution expression for instantiation

setSymbol(Symbol) - Method in class fmrisc.Syntax.Reference

sets symbol associated to reference

setSystemIn(BufferedReader) - Static method in class fmrisc.ProofNavigator.State

set standard input stream

setSystemOut(PrintWriter) - Static method in class fmrisc.ProofNavigator.State

set standard output stream

setTrusted(boolean) - Method in class fmrisc.Proving.Proof

Signal whether proof is trusted.

setType(Type) - Method in class fmrisc.Semantics.TypeExpression

set type

setType(Type) - Method in class fmrisc.Semantics.TypeSymbol

Set type of symbol to type.

setType(Type) - Method in class fmrisc.Semantics.ValueSymbol

Set type of symbol.

setUnselected() - Method in class fmrisc.ProofNavigator.SWT.ProofTree

Set all states in tree widget to unselected.

setValue(Expression) - Method in class fmrisc.Semantics.ValueSymbol

Set value of symbol.

setVarNumber(int) - Method in class fmrisc.Semantics.ValueSymbol

Set variable number of symbol.

setVarNumber(int) - Static method in class fmrisc.Syntax.ASTUtil

set the current variable number for printing

setWeakerTypes(boolean) - Static method in class fmrisc.Semantics.Checking

signals whether weaker type discipline is to be preserved

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

Signals that prover is running in the background.

signalRunning(boolean) - Method in class fmrisc.ProofNavigator.SWT.Top

Signal run status of background process.

Simplify - Class in fmrisc.ProofNavigator.Commands

Command "simplify": simplify a proof state.

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

Create a "simplify" command.

simplify(boolean) - Method in class fmrisc.Proving.ProofState

simplify the current proof state and potentially close it.

simplify(ProofState, Formula, boolean) - Static method in class fmrisc.Proving.ProverReasoning

Simplify a single formula in some proof state.

simplify(ProofState, boolean, boolean) - Static method in class fmrisc.Proving.ProverReasoning

Simplify the current proof state and potentially close it.

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

Simplify expression.

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

simplify expression

simplifyNames(TypedIdentifier[], Environment, Expression) - Static method in class fmrisc.Semantics.Checking

Simplify names of local variables to their base names if no name capture can occur.

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

Skip new line from input stream

Skolemize - Class in fmrisc.ProofNavigator.Commands

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

create a "skolemize" command

space() - Method in class fmrisc.Communication.PrettyPrinter

Insert a space (or a newline at the end of the line).

Split - Class in fmrisc.ProofNavigator.Commands

Command "split": split a proof state.

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

Create a "split" command.

State - Class in fmrisc.ProofNavigator

Execution context for the proof navigator.

State() - Constructor for class fmrisc.ProofNavigator.State

StateC - Class in fmrisc.ProofNavigator.Commands

Command "state": print denoted state.

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

Create a "state" command

Store - Class in fmrisc.Communication

Persistent store of declarations and proofs.

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

Create instance of store for denoted directory.

STRING - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

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

construct subrangetype with denoted bounds.

SubrangeType - Class in fmrisc.Syntax

Subranges of integers.

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

construct subrangetype with denoted bounds

Substitute - Class in fmrisc.Proving

Substitute in an expression all free occurences of denoted variables.

substitute(Expression, ValueDeclIdentifier[], Expression[], boolean) - Static method in class fmrisc.Proving.Substitute

Return expression with simultaneous variable substitutions performed.

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

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

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

return greatest subtype of type0 and type1 (null, if none exists) does not generate tccs.

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

construct subtype with denoted predicate.

SubType - Class in fmrisc.Syntax

Predicated subtypes.

SubType(Expression) - Constructor for class fmrisc.Syntax.SubType

construct subtype with denoted predicate.

Symbol - Interface in fmrisc.Semantics

Interface to symbols.

SymbolBase - Class in fmrisc.Semantics

Base class of symbols.

SymbolBase(Identifier) - Constructor for class fmrisc.Semantics.SymbolBase

construct symbol with given identifier

SymbolTable - Class in fmrisc.Semantics

Base class of symbol tables.

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