Skip navigation links
KeY 2.6.0_3b928241d3c6497f2bf3626bad48a3118b304db1

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.0_3b928241d3c6497f2bf3626bad48a3118b304db1