KeY-TechTips (02.12.2001) ------------------------- Content ------- I) What are the KeY-TechTips? ---------------------------- II) Tips ------- a) Loading Resources - The KeYResourceManager b) Debugging mechanisms ------------------------------------------------------------------------ I) What are the KeY-TechTips? ------------------------------ The aim of the KeY-TechTips is to create a KeY-implementation description step-by-step. Instead of writing one large document at once that would be partially out-of-date before it is finished, the KeY-TechTips follow an approach comparable to the one of the JDC-TechTips for Java. It is thought to have one TT every second (or third) week. Each covering several aspects of the KeY-system enriched with a few small examples that clarify how to use or extend the KeY-API. These documents can then be (easily) integrated into a KeY-Developer documentation. Other advantages would be * basic changes of the API could be communicated faster * the different parts could be used in the package descriptions used by javadoc. Some topics that are thought to be covered are: * KeYResourceManager, Debugging (in this KeY-TechTips) * How to write and add tests * How to use the term framework of KeY (Term, TermFactory) * Extending Together * Translation OCL <-> DL * MGTP * How to create design patterns * STSR match algorithm, application * GUI framework * Java structures in KeY (Compost, Conversion, etc.) Feel free to suggest topics and/or write an article. Mail to: bubel@mail.informatik.kit.edu II) Tips -------- How to checkout and compile KeY see the document: How to open a door - Part One: Building KeY (http://i12www.iti.kit.edu/~bubel/KeYBuild.ps a) Loading Resources - The KeYResourceManager --------------------------------------------- First some words about resources. Resources are files that are part of the KeY-system e.g. icons or the files with the standard rules of the calculus. To load these kinds of files the KeYResourceManager from the package "de.uka.ilkd.key.util" is used instead of the standard java mechanisms. There are two reasons why it is wise to do so: 1) The KeY-system is distributed as a jar file and therefore we need to load the resources from inside the jar package 2) The compiled code of the KeY-system, this means the '.class' files, is copied to a separate directory (system/binary) that is created by the Makefile and not part of the PRCS repository. So you cannot add the resources in the same directories like the source files and also not into the corresponding binary directory as it will not be checked in and further a call of 'gmake clean' or 'gmake realclean' will delete the binary directory. OK, I stop now telling you want not to do and face on how to add and access resources. I will go along an example showing how to add and load an icon accessing another file e.g. a text file is quite similar using slightly different methods of the KeYResourceManager. Problem description: The class "TestLoadIcon" in package "de.uka.ilkd.key.test" needs to load an icon called "TestIcon.gif" Step One: Add the icon to the project -------------------------------------- All resources of the KeY-projects are found in directories starting at the directory "system/resources". The exact location where to put the resource depends on the class that needs the resource, more exact on the package the class belongs to. Copy the resource into a subdirectory starting at "system/resources/" where package is the directory path you achieve by replacing the dots with '/', if the directory does not exist, create it. Examples: --------- 1) class A in package de.uka.ilkd.key.logicdata wants to load the resource "AIcon.gif" therefore copy the resource to "system/resources/de/uka/ilkd/key/logicdata/" 2) class B in package de.uka.ilkd.key.logicdata wants to load the resource "icons/BIcon.gif" therefore copy the resource to "system/resources/de/uka/ilkd/key/logicdata/icons/" In our case the icon is loaded from the class "TestLoadIcon" of the package "de.uka.ilkd.key.test" has to be copied into the subdirectory of "system/resources/de/uka/ilkd/key/test/". As we want to collect all icons needed by this package in the subdirectory "icons/" we copy the file "TestIcon.gif" to "system/resources/de/uka/ilkd/key/test/icons/". cp TestIcon.gif system/resources/de/uka/ilkd/key/test/icons/ Notice: You do not need to edit the Makefile for adding a resource as the whole resource directory hierarchy will be copied to the right location, but only if you make a "gmake clean" before. Remember also that you have to add the resource file to the PRCS project file "key.prj" before you checkin. Step Two: Loading the resource ------------------------------ Therefore we use the KeYResourceManager that can be found in the package "de.uka.ilkd.key.util". It offers two methods for loading an image: public ImageIcon createImageIcon(Object o, String filename) and public ImageIcon createImageIcon(Class cl, String filename) So if we want to load an image we have to call one of the methods handing over the object loading the image or the class it belongs to. From this one the KeYResourceManager will determine just the package where the class (of the object) is declared. Together with the second parameter it calculates the position of the resource. Remember that if you have copied to subdirectory you have to handover the relative position together with the filename. Examples: * class A from above has to call createImageIcon(this, "AIcon.gif") or equivalent createImageIcon(A.class, "AIcon.gif") * class B from above has to call createImageIcon(this, "icons/BIcon.gif") or equivalent createImageIcon(B.class, "icons/BIcon.gif") As the KeYResourceManager is a Singleton this means only one instanceof the class exists we can get this instance using the static method KeYResourceManager.getManager() returning the unique instance of the KeYResourceManager. With this information we can now implement our class TestLoadIcon package de.uka.ilkd.key.test; import de.uka.ilkd.key.util.KeYResourceManager; import java.awt.*; import javax.swing.*; public class TestLoadIcon { private Image test; public TestLoadIcon() { KeYResourceManager manager = KeYResourceManager.getManager(); ImageIcon icon = manager.createImageIcon(this, "icons/TestIcon.gif"); test = icon.getImage(); } } b) Debugging mechanisms ------------------------ The class "Debug" in the package "de.uka.ilkd.key.util" supports you writing debug code. There class offers methods for textual output and assertions. The advantage to use the methods of this class is that they can be turned on/off by setting the class fields ENABLE_DEBUG and ENABLE_ASSERTION to "true" or "false". ENABLE_ASSERTION turns on the assertion methods and ENABLE_DEBUG the textual output methods. ****************** * Output methods * ****************** I will introduce two of the output methods as an example the use of the other is quite similar. The first method is public static void out(String msg) it is the simples one and has nearly the same effect as a conventional System.out.println(msg) The only difference is that it adds a "DEBUG::" before msg and that you can get rid off these messages by setting the field ENABLE_DEBUG to "false". The second method is public static void outIfEqual(String msg, Object obj1, Object obj2) this method prints the String msg if and both objects are equal this means if obj1.equals(obj2) returns "true". The justification for this method is, that evaluating the equality of two object could be an expensive operation e.g. for lists (or strings) we may have as worst case O(n), and as Java evaluates the parameters of a method before calling the method. This means that we may have to pay high costs for a code like if (obj1.equals(obj2)) { Debug.out(msg); } instead of Debug.outIfEqual(msg, obj1, obj2); even if ENABLE_DEBUG has been set to false. *************** * Assertions * *************** You may want to use assertions e.g. to ensure that some postconditions are true, e.g. an object is not the null object or uncovered cases in if-else cascades. Therefore the class Debug offers the methods public static void assert(boolean isOK) and public static void assert(boolean isOK, String message) If the boolean "isOk" has value false an AssertFailure is thrown. The class AssertionFailure extends RuntimeException and therefore these failures need not to be caught by a 'try-catch' statement. The second method prints the text given in "message" if the assertion fails. Example: -------- Debug.assert(obj != null, "Object is null"); prints "Object is null" if the variable 'obj' has a 'null' reference and throws an AssertionFailure To turn off the assertions set the ENABLE_ASSERTION to false. Future enhancements: -------------------- It may be useful to have different debug levels like e.g. PRINS so that e.g. a message is only printed if the priority level is higher or equal than the current debug level.