Skip navigation links
KeY 2.6.1_b7dc5338bd4d2c41d019616407d79ac6dec9efa4

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

Skip navigation links
KeY 2.6.1_b7dc5338bd4d2c41d019616407d79ac6dec9efa4