|
||||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectRules
OrdSimp
Eine Instanz von OrdSimp stellt eine Reihe relationaler 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 relationalen Regel:
Muster: int(_X) < int(_Y)
Vereinfachungsmuster: true
Bedingung: _X < _Y
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 erfüllt, wenn die ganze Zahl "_X" kleiner als die ganze Zahl "_Y" ist. Der
Vergleich ist möglich auf Grund des passenden "Musters".
Eine Beschreibung der verschiedenen Typen der Regeln findet sich in der Hilfe
zur Klasse "SimpRule".
SimpRule
,
SimpleNode
Constructor Summary | |
OrdSimp(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 OrdSimp(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 |