| java.lang.Object
 de.uka.ilkd.key.rule.CheckPrgTransfSoundness
| CheckPrgTransfSoundness | | public class CheckPrgTransfSoundness (Code) | | Automated use to prove sets of taclets
To actually use all this on a set of taclets you have to do the
following: Put the taclets you are interested in into a
``.key'' file, e.g.\ called ``rules.key''. You start the generation of
the Maude input in this case by running ``bin/runJava
de.uka.ilkd.key.rule.CheckPrgTransfSoundness rules.key input.maude''
where the result gets put into the file ``input.maude''. Then you start
Maude with the output written directly to a file, say ``result.txt'' by
running your version of maude, in linux e.g.\ with ``maude-linux >
result.txt''. Then you load the modified Maude Java Semantics which you
can get from my homepage ``i12www.ira.uka.de/~rsasse'' with ``load
java-es-m-modified.maude'' and will get some warnings printed on the
monitor which you can safely ignore. When those are complete you load
the input by typing ``load input.maude'' and then wait for around a
minute to be on the safe side, or take a look at whether the processor
is working, if not it is probably done. Then end Maude by typing ``q''.
|
| Method Summary | |
| public static void | createAllPossibilities(Term find, Term replaceWith, Object[] allSVs, int svarrindex, int svarrsize, String addString, Map svToMaude)
| | public static void | createFindCode(Term find, Map svToMaude)
| | public static void | createNewVarsAddString(Map svToMaude)
| | public static void | createReplaceWithCode(Term replaceWith, Map svToMaude)
| | public static String | createStringCurrObjEnv(String svName)
| | public static String | createStringLocalEnv(String svName)
| | public static String | createStringMemoryBool(String svName)
| | public static String | createStringMemoryInt(String svName)
| | public static String | createStringMemoryObj(String svName)
| | public static String | createStringMemoryObjWAtt(String svName, String svAttName)
| | public static String | createStringMemoryVal(String svName)
| | public static String | createStringNewVarAtt(String svName, String svPeerName)
| | public static String | createStringNewVarBool(String svName)
| | public static String | createStringNewVarInt(String svName)
| | public static String | createStringNewVarVal(String svName)
| | public static String | createStringStaticEnv(String svName)
| | public static void | finishRecurse(NonTerminalProgramElement findStat, String indent, Restriction restri)
| | public static void | main(String args)
| | public static SetOfTaclet | parseTaclets()
| | public static void | preProcessFindPart(Term find)
| | public static void | processAllTaclets(SetOfTaclet taclets)
| | public static void | processTaclet(Taclet taclet)
| | public static void | putStringTogetherWriteToFile(String addString, Map svToMaude)
| | public static void | recurse(NonTerminalProgramElement findStat, String indent, Restriction restri)
| | public static String | recurseFindRepl(ProgramElement pE, Map svToMaude)
|
| createAllPossibilities | | public static void createAllPossibilities(Term find, Term replaceWith, Object[] allSVs, int svarrindex, int svarrsize, String addString, Map svToMaude)(Code) | | |
| createFindCode | | public static void createFindCode(Term find, Map svToMaude)(Code) | | |
| createNewVarsAddString | | public static void createNewVarsAddString(Map svToMaude)(Code) | | |
| createReplaceWithCode | | public static void createReplaceWithCode(Term replaceWith, Map svToMaude)(Code) | | |
| parseTaclets | | public static SetOfTaclet parseTaclets()(Code) | | |
| preProcessFindPart | | public static void preProcessFindPart(Term find)(Code) | | |
| processAllTaclets | | public static void processAllTaclets(SetOfTaclet taclets)(Code) | | |
| processTaclet | | public static void processTaclet(Taclet taclet)(Code) | | |
| putStringTogetherWriteToFile | | public static void putStringTogetherWriteToFile(String addString, Map svToMaude)(Code) | | |
|
|