de.uka.ilkd.key.taclettranslation.assumptions

Class AssumptionFormula

java.lang.Object

de.uka.ilkd.key.taclettranslation.assumptions.AssumptionFormula

All Implemented Interfaces:

TacletFormula

public class AssumptionFormula
extends java.lang.Object
implements TacletFormula

Field Summary

Fields

Modifier and Type	Field and Description
(package private) TacletConditions	conditions
(package private) java.util.Collection<Term>	formula
(package private) java.lang.String	status
(package private) Taclet	taclet

Constructor Summary

Constructors

Constructor and Description
AssumptionFormula(Taclet taclet, java.util.Collection<Term> formula, java.lang.String status)
AssumptionFormula(Taclet taclet, java.util.Collection<Term> formula, java.lang.String status, TacletConditions conditions)

Method Summary

Modifier and Type	Method and Description
TacletConditions	getConditions()
Term	getFormula(TermServices services)
java.util.Collection<Term>	getInstantiations() It can be that a taclet is translated into several formulas, i.e. in the case that the generics are instantiated.
java.lang.String	getStatus()
Taclet	getTaclet()

Methods inherited from class java.lang.Object

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

Field Detail

taclet

Taclet taclet

formula

java.util.Collection<Term> formula

status

java.lang.String status

conditions

TacletConditions conditions

Constructor Detail

AssumptionFormula

public AssumptionFormula(Taclet taclet,
                         java.util.Collection<Term> formula,
                         java.lang.String status)

AssumptionFormula

public AssumptionFormula(Taclet taclet,
                         java.util.Collection<Term> formula,
                         java.lang.String status,
                         TacletConditions conditions)
                  throws IllegalTacletException

Throws:

IllegalTacletException

Method Detail

getConditions

public TacletConditions getConditions()

getFormula

public Term getFormula(TermServices services)

Specified by:

getFormula in interface TacletFormula

Parameters:

services - TODO

Returns:

the formula of the instance if the taclet is translatable otherwise null. If the translation of the taclet consists of several instantiations (e.g. the taclet has some generic sorts) the returned term is a conjunction of these instantiations.

getTaclet

public Taclet getTaclet()

Specified by:

getTaclet in interface TacletFormula

Returns:

the taclet of the instance.

getStatus

public java.lang.String getStatus()

Specified by:

getStatus in interface TacletFormula

Returns:

if the taclet can not be translated the reason why. Otherwise a empty string.

getInstantiations

public java.util.Collection<Term> getInstantiations()

Description copied from interface: TacletFormula

It can be that a taclet is translated into several formulas, i.e. in the case that the generics are instantiated. This method returns the set of resulting formulas.

Specified by:

getInstantiations in interface TacletFormula