|
| |
|
| java.lang.Object
 junit.framework.TestCase
de.uka.ilkd.key.rule.TestApplyTaclet
| TestApplyTaclet | | public class TestApplyTaclet extends TestCase (Code) | | class tests the apply methods in Taclet
|
| setUp | | public void setUp()(Code) | | |
| tearDown | | public void tearDown()(Code) | | |
| testAddingRule | | public void testAddingRule()(Code) | | |
| testAntecTacletWithoutIf | | public void testAntecTacletWithoutIf()(Code) | | |
| testBugBrokenApply | | public void testBugBrokenApply()(Code) | | |
| testBugEmptyBlock | | public void testBugEmptyBlock()(Code) | | |
| testBugID176 | | public void testBugID176()(Code) | | |
| testBugID177 | | public void testBugID177()(Code) | | |
| testBugID188 | | public void testBugID188()(Code) | | |
| testCatchList | | public void testCatchList()(Code) | | |
| testCompleteContextAddBug | | public void testCompleteContextAddBug()(Code) | | tests a bug, which causedthe first statement in a context block to be discarded
in cases where the complete program has been matched by the prefix and suffix of the context
block i.e.
a rule like
\find ( <.. ...>\forall u; post )
\replacewith (\forall u;<.. ..>post)
applied on
< method-frame():{ while (...) {...} } >\forall int i; i>0
created the goal
\forall int i;< method-frame():{ } >i>0
which is of course incorrect.
|
| testConstraintApplication | | public void testConstraintApplication()(Code) | | |
| testContextAdding | | public void testContextAdding()(Code) | | |
| testIncompleteNoFindTacletApp | | public void testIncompleteNoFindTacletApp()(Code) | | |
| testIncompleteSuccTacletApp | | public void testIncompleteSuccTacletApp()(Code) | | |
| testModalityLevel0 | | public void testModalityLevel0()(Code) | | |
| testModalityLevel1 | | public void testModalityLevel1()(Code) | | |
| testModalityLevel2 | | public void testModalityLevel2()(Code) | | |
| testNoFindTacletWithoutIf | | public void testNoFindTacletWithoutIf()(Code) | | |
| testPrgTacletApp | | public void testPrgTacletApp()(Code) | | |
| testRemoveEmptyBlock | | public void testRemoveEmptyBlock()(Code) | | this test is different from the other empty block removal test
|
| testRewriteTacletWithoutIf | | public void testRewriteTacletWithoutIf()(Code) | | |
| testSetTaclets0 | | public void testSetTaclets0()(Code) | | |
| testShadowedUpdateLocation | | public void testShadowedUpdateLocation()(Code) | | |
| testSuccTacletAllRight | | public void testSuccTacletAllRight()(Code) | | |
| testSuccTacletWithoutIf | | public void testSuccTacletWithoutIf()(Code) | | |
| testTacletVariableCollector | | public void testTacletVariableCollector()(Code) | | tests if the variable sv collector pays attention to schema variables
occuring as part of attributes and/or updates (there was a bug where
this has been forgotten, and as a result after applying a method contract
schemavariables have been introduces into a goal sequent)
|
| testTacletWithIf | | public void testTacletWithIf()(Code) | | |
|
|
|