fmrisc.ProofNavigator.Syntax

Class ForallFormula

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTBase

fmrisc.ProofNavigator.Syntax.ExpressionBase

fmrisc.ProofNavigator.Syntax.QuantifiedExpression

fmrisc.ProofNavigator.Syntax.ForallFormula

All Implemented Interfaces:

AST, Expression

public final class ForallFormula
extends QuantifiedExpression

Handling of universally quantified formulas.

Constructor Summary

Constructors

Constructor and Description
ForallFormula(TypedIdentifier[] variables, Expression base) construct forall formula of variables and base formula

Method Summary

Methods

Modifier and Type	Method and Description
QuantifiedExpression	construct(TypedIdentifier[] variables, Expression base) Construct quantified expression.
void	printCore(java.io.PrintWriter out) Prints text representation on out (without new line termination).

Methods inherited from class fmrisc.ProofNavigator.Syntax.QuantifiedExpression

accept, getBase, getPriority, getVariables, instantiate, substitution

Methods inherited from class fmrisc.ProofNavigator.Syntax.ExpressionBase

printPriority

Methods inherited from class fmrisc.ProofNavigator.Syntax.ASTBase

print, printParens, toString

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface fmrisc.ProofNavigator.Syntax.AST

print, printParens, toString

Constructor Detail

ForallFormula

public ForallFormula(TypedIdentifier[] variables,
             Expression base)

construct forall formula of variables and base formula

Parameters:

variables - the quantified variables

base - the base formula

Method Detail

construct

public QuantifiedExpression construct(TypedIdentifier[] variables,
                             Expression base)

Construct quantified expression.

Specified by:

construct in class QuantifiedExpression

Parameters:

variables - typed variables.

base - an expression.

Returns:

a quantified expression of the same kind as this expression with the denoted variables and base expression.

printCore

public void printCore(java.io.PrintWriter out)

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

Specified by:

printCore in interface AST

Overrides:

printCore in class QuantifiedExpression

Parameters:

out - the stream on which the text is written