de.uka.ilkd.key.ldt

Class PermissionLDT

java.lang.Object

de.uka.ilkd.key.ldt.LDT

de.uka.ilkd.key.ldt.PermissionLDT

All Implemented Interfaces:

Named

public class PermissionLDT
extends LDT

Field Summary

Fields

Modifier and Type	Field and Description
static Name	NAME
private Function	permissionsFor

Constructor Summary

Constructors

Constructor and Description
PermissionLDT(Services services)

Method Summary

Modifier and Type	Method and Description
Function	getFunctionFor(Operator op, Services services, ExecutionContext ec) returns the function symbol for the given operation
Function	getPermissionsFor()
Type	getType(Term t)
boolean	hasLiteralFunction(Function f)
boolean	isResponsible(Operator op, Term[] subs, Services services, ExecutionContext ec) returns true if the LDT offers an operation for the given java operator and the logic subterms
boolean	isResponsible(Operator op, Term sub, TermServices services, ExecutionContext ec) returns true if the LDT offers an operation for the given unary java operator and the logic subterms
boolean	isResponsible(Operator op, Term left, Term right, Services services, ExecutionContext ec) returns true if the LDT offers an operation for the given binary java operator and the logic subterms
Term	translateLiteral(Literal lit, Services services) translates a given literal to its logic counterpart
Expression	translateTerm(Term t, ExtList children, Services services) Is called whenever hasLiteralFunction() returns true.

Methods inherited from class de.uka.ilkd.key.ldt.LDT

addFunction, addFunction, addSortDependingFunction, containsFunction, functions, getNewLDTInstances, name, targetSort, toString

Methods inherited from class java.lang.Object

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

Field Detail

NAME

public static final Name NAME

permissionsFor

private final Function permissionsFor

Constructor Detail

PermissionLDT

public PermissionLDT(Services services)

Method Detail

getPermissionsFor

public Function getPermissionsFor()

isResponsible

public boolean isResponsible(Operator op,
                             Term[] subs,
                             Services services,
                             ExecutionContext ec)

Description copied from class: LDT

returns true if the LDT offers an operation for the given java operator and the logic subterms

Specified by:

isResponsible in class LDT

Parameters:

op - the de.uka.ilkd.key.java.expression.Operator to translate

subs - the logic subterms of the java operator

services - the Services

ec - the ExecutionContext in which the expression is evaluated

Returns:

true if the LDT offers an operation for the given java operator and the subterms

isResponsible

public boolean isResponsible(Operator op,
                             Term left,
                             Term right,
                             Services services,
                             ExecutionContext ec)

Description copied from class: LDT

returns true if the LDT offers an operation for the given binary java operator and the logic subterms

Specified by:

isResponsible in class LDT

Parameters:

op - the de.uka.ilkd.key.java.expression.Operator to translate

left - the left subterm of the java operator

right - the right subterm of the java operator

services - the Services

ec - the ExecutionContext in which the expression is evaluated

Returns:

true if the LDT offers an operation for the given java operator and the subterms

isResponsible

public boolean isResponsible(Operator op,
                             Term sub,
                             TermServices services,
                             ExecutionContext ec)

Description copied from class: LDT

returns true if the LDT offers an operation for the given unary java operator and the logic subterms

Specified by:

isResponsible in class LDT

Parameters:

op - the de.uka.ilkd.key.java.expression.Operator to translate

sub - the logic subterms of the java operator

services - the Services

ec - the ExecutionContext in which the expression is evaluated

Returns:

true if the LDT offers an operation for the given java operator and the subterm

translateLiteral

public Term translateLiteral(Literal lit,
                             Services services)

Description copied from class: LDT

translates a given literal to its logic counterpart

Specified by:

translateLiteral in class LDT

Parameters:

lit - the Literal to be translated

Returns:

the Term that represents the given literal in its logic form

getFunctionFor

public Function getFunctionFor(Operator op,
                               Services services,
                               ExecutionContext ec)

Description copied from class: LDT

returns the function symbol for the given operation

Specified by:

getFunctionFor in class LDT

Returns:

the function symbol for the given operation

hasLiteralFunction

public boolean hasLiteralFunction(Function f)

Specified by:

hasLiteralFunction in class LDT

translateTerm

public Expression translateTerm(Term t,
                                ExtList children,
                                Services services)

Description copied from class: LDT

Is called whenever hasLiteralFunction() returns true.

Specified by:

translateTerm in class LDT

getType

public Type getType(Term t)

Specified by:

getType in class LDT