de.uka.ilkd.key.logic.op

Class UpdateJunctor

java.lang.Object

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

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

de.uka.ilkd.key.logic.op.UpdateJunctor

All Implemented Interfaces:

Named, Operator, SortedOperator, SVSubstitute, Sorted

public final class UpdateJunctor
extends AbstractSortedOperator

Class of update junctor operators, i.e., operators connecting a given number of updates to create another update. There are currently two such operators: the empty update "skip" and the parallel update connector "|".

Field Summary

Fields

Modifier and Type	Field and Description
static UpdateJunctor	PARALLEL_UPDATE
static UpdateJunctor	SKIP

Constructor Summary

Constructors

Modifier	Constructor and Description
private	UpdateJunctor(Name name, int arity)

Method Summary

Modifier and Type	Method and Description
private static Sort[]	createUpdateSortArray(int arity)

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

SKIP

public static final UpdateJunctor SKIP

PARALLEL_UPDATE

public static final UpdateJunctor PARALLEL_UPDATE

Constructor Detail

UpdateJunctor

private UpdateJunctor(Name name,
                      int arity)

Method Detail

createUpdateSortArray

private static Sort[] createUpdateSortArray(int arity)