|
||||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectRules
AlgSimp
Eine Instanz von AlgSimp stellt eine Reihe algebraischer Regeln zum Vereinfachen einer beliebigen Verifikationsbedingung bereit. Eine solche Regel besteht im Allgemeinen (je nach Typ) aus einem Muster, einem Vereinfachungsmuster und einer Bedingung, jeweils in Form eines Baumes (ein Objekt vom Typ SimpleNode), zusammengefasst zu einem Objekt vom Typ SimpRule.
Ein Beispiel einer algebraischen Regel:
Muster: int(_X) + int(_Y)
Vereinfachungsmuster: int(_Z)
Bedingung: _X + _Y = _Z
Passt die zu untersuchende Verifikationsbedingung auf das "Muster" und ist die "Bedingung"
erfüllt, wird sie zum "Vereinfachungsmuster" vereinfacht. In obigem Beispiel ist die
Bedingung immer erfüllt, denn es sind nur die Zahlen "_X" und "_Y" zu addieren, was
auf Grund des passenden "Musters" immer möglich ist.
Eine Beschreibung der verschiedenen Typen der Regeln findet sich in der Hilfe
zur Klasse "SimpRule".
SimpRule
,
SimpleNode
Constructor Summary | |
AlgSimp(boolean manual)
Erzeugt die Regeln und füllt damit das Feld "rules". |
Method Summary | |
SimpleNode |
getCondPattern(int i)
Liefert die "Bedingung" der i-ten Regel. |
short |
getCondType(int i)
Liefert den Typ der i-ten Regel. |
java.lang.String |
getIdNameOfSimplifiedCondPattern(int i)
Liefert den Bezeichner der freien Variablen in der "Bedingung" der i-ten Regel. |
int |
getNumberOfRules()
Liefert die Anzahl der Vereinfachungsregeln. |
SimpleNode |
getPattern(int i)
Liefert das "Muster" der i-ten Regel. |
SimpleNode |
getSimpPattern(int i)
Liefert das "Vereinfachungsmuster" der i-ten Regel. |
boolean |
hasCondPattern(int i)
Überprüft, ob die i-te Regel eine "Bedingung" benötigt. |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
public AlgSimp(boolean manual)
manual
- Die boolean Variable fragt ab, ob manuell oder automatisch bewiesen wird.Method Detail |
public int getNumberOfRules()
getNumberOfRules
in class Rules
public SimpleNode getPattern(int i)
getPattern
in class Rules
public SimpleNode getSimpPattern(int i)
getSimpPattern
in class Rules
public SimpleNode getCondPattern(int i)
getCondPattern
in class Rules
public boolean hasCondPattern(int i)
hasCondPattern
in class Rules
public short getCondType(int i)
getCondType
in class Rules
SimpRule
public java.lang.String getIdNameOfSimplifiedCondPattern(int i)
getIdNameOfSimplifiedCondPattern
in class Rules
|
||||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |