de.uka.ilkd.key.logic

Class Semisequent.Empty

java.lang.Object

de.uka.ilkd.key.logic.Semisequent

de.uka.ilkd.key.logic.Semisequent.Empty

All Implemented Interfaces:

java.lang.Iterable<SequentFormula>

Enclosing class:

Semisequent

private static class Semisequent.Empty
extends Semisequent

Field Summary

Fields inherited from class de.uka.ilkd.key.logic.Semisequent

EMPTY_SEMISEQUENT

Constructor Summary

Constructors

Modifier	Constructor and Description
private	Empty()

Method Summary

Modifier and Type	Method and Description
boolean	contains(SequentFormula sequentFormula) checks if a SequentFormula is in this Semisequent
boolean	equals(java.lang.Object o)
SequentFormula	get(int idx) gets the element at a specific index
SequentFormula	getFirst()
int	hashCode()
int	indexOf(SequentFormula sequentFormula) returns index of a SequentFormula
SemisequentChangeInfo	insert(int idx, SequentFormula sequentFormula) inserts the element always at index 0 ignores the first argument
SemisequentChangeInfo	insertFirst(SequentFormula sequentFormula) inserts the element at index 0
SemisequentChangeInfo	insertLast(SequentFormula sequentFormula) inserts the element at the end of the semisequent
boolean	isEmpty() is this a semisequent that contains no formulas
SemisequentChangeInfo	remove(int idx) removes an element
SemisequentChangeInfo	replace(int idx, SequentFormula sequentFormula) replaces the element at place idx with sequentFormula
int	size()
java.lang.String	toString()

Methods inherited from class de.uka.ilkd.key.logic.Semisequent

asList, containsEqual, insert, insertFirst, insertLast, iterator, replace, replace, replace

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Constructor Detail

Empty

private Empty()

Method Detail

insert

public SemisequentChangeInfo insert(int idx,
                                    SequentFormula sequentFormula)

inserts the element always at index 0 ignores the first argument

Overrides:

insert in class Semisequent

Parameters:

idx - int encoding the place the element has to be put

sequentFormula - SequentFormula to be inserted

Returns:

semisequent change information object with new semisequent with sequentFormula at place idx

insertFirst

public SemisequentChangeInfo insertFirst(SequentFormula sequentFormula)

inserts the element at index 0

Overrides:

insertFirst in class Semisequent

Parameters:

sequentFormula - SequentFormula to be inserted

Returns:

semisequent change information object with new semisequent with sequentFormula at place idx

insertLast

public SemisequentChangeInfo insertLast(SequentFormula sequentFormula)

inserts the element at the end of the semisequent

Overrides:

insertLast in class Semisequent

Parameters:

sequentFormula - SequentFormula to be inserted

Returns:

semisequent change information object with new semisequent with sequentFormula at place idx

isEmpty

public boolean isEmpty()

is this a semisequent that contains no formulas

Overrides:

isEmpty in class Semisequent

Returns:

true if the semisequent contains no formulas

replace

public SemisequentChangeInfo replace(int idx,
                                     SequentFormula sequentFormula)

replaces the element at place idx with sequentFormula

Overrides:

replace in class Semisequent

Parameters:

idx - an int specifying the index of the element that has to be replaced

sequentFormula - the SequentFormula replacing the old element at index idx

Returns:

semisequent change information object with new semisequent with sequentFormula at place idx

size

public int size()

Overrides:

size in class Semisequent

Returns:

int counting the elements of this semisequent

remove

public SemisequentChangeInfo remove(int idx)

removes an element

Overrides:

remove in class Semisequent

Parameters:

idx - int being the index of the element that has to be removed

Returns:

semisequent change information object with an empty semisequent as result

indexOf

public int indexOf(SequentFormula sequentFormula)

returns index of a SequentFormula

Overrides:

indexOf in class Semisequent

Parameters:

sequentFormula - the SequentFormula the index want to be determined

Returns:

index of sequentFormula

get

public SequentFormula get(int idx)

gets the element at a specific index

Overrides:

get in class Semisequent

Parameters:

idx - int representing the index of the element we want to have

Returns:

SequentFormula found at index idx

getFirst

public SequentFormula getFirst()

Overrides:

getFirst in class Semisequent

Returns:

the first SequentFormula of this Semisequent

contains

public boolean contains(SequentFormula sequentFormula)

checks if a SequentFormula is in this Semisequent

Overrides:

contains in class Semisequent

Parameters:

sequentFormula - the SequentFormula to look for

Returns:

true iff. sequentFormula has been found in this Semisequent

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class Semisequent

hashCode

public int hashCode()

Overrides:

hashCode in class Semisequent

toString

public java.lang.String toString()

Overrides:

toString in class Semisequent

Returns:

String representation of this Semisequent