de.uka.ilkd.key.logic.op

Class Equality

java.lang.Object

de.uka.ilkd.key.logic.op.AbstractOperator

de.uka.ilkd.key.logic.op.AbstractSortedOperator

de.uka.ilkd.key.logic.op.Equality

All Implemented Interfaces:

Named, Operator, SortedOperator, SVSubstitute, Sorted

public final class Equality
extends AbstractSortedOperator

This class defines the equality operator "=". It is a binary predicate accepting arbitrary terms (sort "any") as arguments. It also defines the formula equivalence operator "<->" (which could alternatively be seen as a Junctor).

Field Summary

Fields

Modifier and Type	Field and Description
static Equality	EQUALS the usual 'equality' operator '='
static Equality	EQV the usual 'equivalence' operator '<->' (be A, B formulae then 'A <-> B' is true if and only if A and B have the same truth value

Constructor Summary

Constructors

Modifier	Constructor and Description
private	Equality(Name name, Sort targetSort)

Method Summary

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractSortedOperator

additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractOperator

arity, bindVarsAt, isRigid, name, toString, validTopLevel, whereToBind

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.logic.op.Operator

arity, bindVarsAt, isRigid, validTopLevel

Methods inherited from interface de.uka.ilkd.key.logic.Named

name

Field Detail

EQUALS

public static final Equality EQUALS

the usual 'equality' operator '='

EQV

public static final Equality EQV

the usual 'equivalence' operator '<->' (be A, B formulae then 'A <-> B' is true if and only if A and B have the same truth value

Constructor Detail

Equality

private Equality(Name name,
                 Sort targetSort)