de.uka.ilkd.key.logic.op

Class Transformer

java.lang.Object

de.uka.ilkd.key.logic.op.AbstractOperator

de.uka.ilkd.key.logic.op.AbstractSortedOperator

de.uka.ilkd.key.logic.op.Function

de.uka.ilkd.key.logic.op.Transformer

All Implemented Interfaces:

Named, Operator, SortedOperator, SVSubstitute, Sorted

public class Transformer
extends Function

Functions with a restricted/special rule set only applicable for the top level of the term transformer and not directly for its arguments, prohibiting any rule applications to sub arguments as well as applications from outside such as update applications. They work similar to the idea of 'Predicate Transformer Semantics' as introduced by Dijkstra in "Guarded commands, nondeterminacy and formal derivation of programs". Note that in the taclets, arguments such as "a -> b" need to be written as "(a -> b)", in order to let the parser know that the argument is "a -> b" and not "a" followed by a syntactic error.

Author:

Michael Kirsten

Constructor Summary

Constructors

Constructor and Description
Transformer(Name name, Sort argSort)
Transformer(Name name, Sort sort, ImmutableArray<Sort> argSorts)

Method Summary

Modifier and Type	Method and Description
static Transformer	getTransformer(Name name, Sort sort, ImmutableArray<Sort> argSorts, TermServices services) Looks up the function namespace for a term transformer with the given attributes, assuming it to be uniquely defined by its name.
static Transformer	getTransformer(PosInOccurrence pio) Examines a position for whether it is inside a term transformer.
static Transformer	getTransformer(Transformer t, TermServices services) Takes a template for a term transformer and checks in the function namespace, whether an equivalent already exists.
static boolean	inTransformer(PosInOccurrence pio) Examines a position for whether it is inside a term transformer.

Methods inherited from class de.uka.ilkd.key.logic.op.Function

isSkolemConstant, isUnique, proofToString, rename, toString

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractSortedOperator

additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractOperator

arity, bindVarsAt, isRigid, name, validTopLevel, whereToBind

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.logic.op.Operator

arity, bindVarsAt, isRigid, validTopLevel

Methods inherited from interface de.uka.ilkd.key.logic.Named

name

Constructor Detail

Transformer

public Transformer(Name name,
                   Sort sort,
                   ImmutableArray<Sort> argSorts)

Transformer

public Transformer(Name name,
                   Sort argSort)

Method Detail

getTransformer

public static Transformer getTransformer(Name name,
                                         Sort sort,
                                         ImmutableArray<Sort> argSorts,
                                         TermServices services)

Looks up the function namespace for a term transformer with the given attributes, assuming it to be uniquely defined by its name. If none is found, a new term transformer is created.

Parameters:

name - name of the term transformer

sort - sort of the term transformer

argSorts - array of the transformer's argument sorts

services -

Returns:

the term transformer of interest

getTransformer

public static Transformer getTransformer(Transformer t,
                                         TermServices services)

Takes a template for a term transformer and checks in the function namespace, whether an equivalent already exists. If this is the case, it returns the found transformer, otherwise it creates a new one.

Parameters:

t - the template for a term transformer

services -

Returns:

the term transformer to be used

inTransformer

public static boolean inTransformer(PosInOccurrence pio)

Examines a position for whether it is inside a term transformer.

Parameters:

pio - A position in an occurrence of a term

Returns:

true if inside a term transformer, false otherwise

getTransformer

public static Transformer getTransformer(PosInOccurrence pio)

Examines a position for whether it is inside a term transformer. If this is the case, the found term transformer is returned.

Parameters:

pio - A position in an occurrence of a term

Returns:

the term transformer the position is in, null otherwise