de.uni_tuebingen.sfb.lichtenstein.formulas
Class FirstOrderVariable

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.Variable
      de.uni_tuebingen.sfb.lichtenstein.formulas.FirstOrderVariable

All Implemented Interfaces:

Serializable

public class FirstOrderVariable
extends Variable

A class representing first order variables in the monadic second order logic.

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

FirstOrderVariable()
Initialize a new first order variable.

FirstOrderVariable(String name)
Initialize a first order variable with the given name.

Method Summary

Dominance	dominates(FirstOrderVariable that) Return the formula that says this variable dominates that variable.
FirstOrderExistentialQuantification	exists(Formula form) Returns the existential quantification of the given formula over this variable.
FirstOrderUniversalQuantification	forAll(Formula form) Returns the universal quantification of the given formula over this variable.
ImmediateDominance	immediatelyDominates(FirstOrderVariable that) Return the formula that says this variable immediately dominates that variable.
Inclusion	in(SetDenotator that) Return the formula that says this variable is an element of that set.
FirstOrderEquality	logicalEquals(FirstOrderVariable that) Return the formula that says this variable is equal to that variable.
Precedence	precedes(FirstOrderVariable that) Return the formula that says this variable precedes that variable.
ProperDominance	properlyDominates(FirstOrderVariable that) Return the formula that says this variable immediately dominates that variable.

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.Variable

getName, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

FirstOrderVariable

public FirstOrderVariable()

Initialize a new first order variable. Its name is composed of the letter 'v' and a number.

FirstOrderVariable

public FirstOrderVariable(String name)

Initialize a first order variable with the given name.

Parameters:

name - The name of the variable.

Postcondition:

The name is set to the given name.

| new.getName() == name

Method Detail

forAll

public FirstOrderUniversalQuantification forAll(Formula form)

Returns the universal quantification of the given formula over this variable.

Parameters:

form - The formula to be quantified.

Precondition:

The given formula should be effective.

| form != null

Precondition:

This variable has to be free in the given formula.

| !form.containsVariable(this) ||
      form.isFreeVariable(this);

Returns:

The universal quantification of the given formula over this variable.

| result.getBoundVariable() == this && |
         result.getArgument() == form

exists

public FirstOrderExistentialQuantification exists(Formula form)

Returns the existential quantification of the given formula over this variable.

Parameters:

form - The formula to be quantified.

Precondition:

The given formula should be effective.

| form != null

Precondition:

This variable has to be free in the given formula.

| !form.containsVariable(this) ||
      form.isFreeVariable(this);

Returns:

The existential quantification of the given formula over this variable.

| result.getBoundVariable() ==
         this &&
| result.getArgument() == form

logicalEquals

public FirstOrderEquality logicalEquals(FirstOrderVariable that)

Return the formula that says this variable is equal to that variable.

Parameters:

that - The other variable. That is a mnemonic for this.logicalEquals(that).

Returns:

The atomic formula claiming this variable is equal to that variable.

| result.getFirstVariable() == this && |
         result.getSecondVariable() == that

in

public Inclusion in(SetDenotator that)

Return the formula that says this variable is an element of that set.

Parameters:

that - The other variable. That is a mnemonic for this.in(that).

Returns:

The atomic formula claiming this variable is an element of that set.

| result.getIncludedVariable() ==
         this &&
| result.getContainingVariable() == that

dominates

public Dominance dominates(FirstOrderVariable that)

Return the formula that says this variable dominates that variable.

Parameters:

that - The other variable. That is a mnemonic for this.dominates(that).

Returns:

The atomic formula claiming this variable dominates that variable.

| result.getDominatingVariable() ==
         this &&
| result.getDominatedVariable() == that

immediatelyDominates

public ImmediateDominance immediatelyDominates(FirstOrderVariable that)

Return the formula that says this variable immediately dominates that variable.

Parameters:

that - The other variable. That is a mnemonic for this.immediatelyDominates(that).

Returns:

The atomic formula claiming this variable immediately dominates that variable.

|
         result.getDominatingVariable() == this &&
| result.getDominatedVariable() == that

properlyDominates

public ProperDominance properlyDominates(FirstOrderVariable that)

Return the formula that says this variable immediately dominates that variable.

Parameters:

that - The other variable. That is a mnemonic for this.immediatelyDominates(that).

Returns:

The atomic formula claiming this variable immediately dominates that variable.

|
         result.getDominatingVariable() == this &&
| result.getDominatedVariable() == that

precedes

public Precedence precedes(FirstOrderVariable that)

Return the formula that says this variable precedes that variable.

Parameters:

that - The other variable. That is a mnemonic for this.precedes(that).

Returns:

The atomic formula claiming this variable precedes that variable.

| result.getPrecedingVariable() == this && |
         result.getPrecededVariable() == that