de.uka.ilkd.key.taclettranslation

Class AbstractSkeletonGenerator

java.lang.Object

de.uka.ilkd.key.taclettranslation.AbstractSkeletonGenerator

All Implemented Interfaces:

SkeletonGenerator

Direct Known Subclasses:

DefaultTacletTranslator

abstract class AbstractSkeletonGenerator
extends java.lang.Object
implements SkeletonGenerator

Translates a taclet into a logical skeleton without instantiating the schema variables. This must be done by the user of this class.

Field Summary

Fields inherited from interface de.uka.ilkd.key.taclettranslation.SkeletonGenerator

DEFAULT_TACLET_TRANSLATOR

Constructor Summary

Constructors

Constructor and Description
AbstractSkeletonGenerator()

Method Summary

Modifier and Type	Method and Description
private ImmutableList<Term>	getFormulaeOfSemisequent(Semisequent s) Collects all formulae of a semisequent in a set.
protected Term	translate(Sequent s, TermServices services) Translates a sequent to a term by using the following translations rules: T ==> D is translated to: And(T)->Or(D).

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.taclettranslation.SkeletonGenerator

translate

Constructor Detail

AbstractSkeletonGenerator

AbstractSkeletonGenerator()

Method Detail

translate

protected Term translate(Sequent s,
                         TermServices services)

Translates a sequent to a term by using the following translations rules: T ==> D is translated to: And(T)->Or(D).
And(s): conjunction between all formulae in set s. Or(s): disjunction between all formulae in set s.

Parameters:

s - The sequent to be translated.

services - TODO

Returns:

the resulting term of the translation or null if both antecedent and succendent are empty.

getFormulaeOfSemisequent

private ImmutableList<Term> getFormulaeOfSemisequent(Semisequent s)

Collects all formulae of a semisequent in a set.

Parameters:

s - Semisequent.

Returns:

A list of all formulae of the semisequent s .