KeY 2.6.2_00c1abfd22b738afe24e89fecc2ee4eec2c38f4a

Package de.uka.ilkd.key.logic

provides a representation for the term and sequent structure.

See: Description

Package de.uka.ilkd.key.logic Description

provides a representation for the term and sequent structure. The structure of a term is defined in Term. Subclasses of Term provide representations for special kinds of terms. However, these subclasses are supposed to be not directly accessed. Instead, Term provides methods for all the methods of the subclasses. Moreover, Terms (or their subclasses) are supposed to be never constructed by constructors of their own, but by instances of TermFactory.

The function of Terms (e.g., if they represent a conjunction of subterms, a quantified formula,...) is only determined by an Operator that is assigned to a Term when the Term is constructed.

Sequents consist of two Semisequents which represent a duplicate-free list of a SequentFormulas. The latter consist of a de.uka.ilkd.key.logic.Constraint and a Term of a special sort Sort.FORMULA.

Sequents and Terms are immutable. Last modified: Wed Dec 4 15:11:14 MET 2002

KeY 2.6.2_00c1abfd22b738afe24e89fecc2ee4eec2c38f4a