de.uka.ilkd.key.rule.match

Class TacletMatcherKit

java.lang.Object

de.uka.ilkd.key.rule.match.TacletMatcherKit

Direct Known Subclasses:

TacletMatcherKit.LegacyTacletMatcherKit, TacletMatcherKit.VMTacletMatcherKit

public abstract class TacletMatcherKit
extends java.lang.Object

Abstract factory for the creation of taclet matcher. Use method getKit() to get the concrete factory and call createTacletMatcher(Taclet) to create a matcher for a Taclet The active factory is chosen at runtime by passing a value for the system property taclet.match Currently supported values are: legacy and vm. The legacy matching algorithm is the one used since the beginning of KeY. It will soon become deprecated and replaced y vm as default.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	TacletMatcherKit.LegacyTacletMatcherKit The concrete factory for the legacy taclet matcher.
private static class	TacletMatcherKit.VMTacletMatcherKit The concrete factory for the vm based taclet matcher.

Field Summary

Fields

Modifier and Type	Field and Description
private static TacletMatcherKit	ACTIVE_TACLET_MATCHER_KIT
private static java.lang.String	TACLET_MATCHER_SELECTION_VALUE sets up the concrete factory to use depending on the provided system property or the given default if no property is set

Constructor Summary

Constructors

Constructor and Description
TacletMatcherKit()

Method Summary

Modifier and Type	Method and Description
abstract TacletMatcher	createTacletMatcher(Taclet taclet) the creator method returning the matcher for the specified taclet
static TacletMatcherKit	getKit() returns the currently enabled factory

Methods inherited from class java.lang.Object

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

Field Detail

TACLET_MATCHER_SELECTION_VALUE

private static final java.lang.String TACLET_MATCHER_SELECTION_VALUE

sets up the concrete factory to use depending on the provided system property or the given default if no property is set

ACTIVE_TACLET_MATCHER_KIT

private static final TacletMatcherKit ACTIVE_TACLET_MATCHER_KIT

Constructor Detail

TacletMatcherKit

public TacletMatcherKit()

Method Detail

getKit

public static TacletMatcherKit getKit()

returns the currently enabled factory

Returns:

the concrete factory to create taclet matchers

createTacletMatcher

public abstract TacletMatcher createTacletMatcher(Taclet taclet)

the creator method returning the matcher for the specified taclet

Parameters:

taclet - the Taclet for which to create a matcher

Returns:

the matcher for the given taclet