|
|
Unit checking for Java IDE
Kebrt, Michal ; Šerý, Ondřej (vedoucí práce) ; Parízek, Pavel (oponent)
Code model checking is a rapidly advancing research topic. However, apart from very constrained scenarios (e.g., veri cation of device drivers by SLAM), the code model checking tools are not widely used in general software development process. We believe that this could be changed if the developers could use the tools in the same way they already use testing tools. In this work, we present the UnitCheck tool, which enhances the standard unit testing of Java code with model checking. A developer familiar with unit testing can apply the tool on standard unit test scenarios and bene t from the exhaustive traversal performed by a code model checker, which is employed inside UnitCheck. Two well-known Java tools are integrated in UnitCheck. JUnit is used as a testing framework and Java PathFinder provides the model checking capability. The UnitCheck plugin for Eclipse presents the checking results in a convenient way known from unit testing, while providing also a verbose output for the expert users. The UnitCheck Ant task allows to incorporate unit checking in the standard Java development and build process.
|
|
|
Unit checking for Java IDE
Kebrt, Michal ; Parízek, Pavel (oponent) ; Šerý, Ondřej (vedoucí práce)
Code model checking is a rapidly advancing research topic. However, apart from very constrained scenarios (e.g., veri cation of device drivers by SLAM), the code model checking tools are not widely used in general software development process. We believe that this could be changed if the developers could use the tools in the same way they already use testing tools. In this work, we present the UnitCheck tool, which enhances the standard unit testing of Java code with model checking. A developer familiar with unit testing can apply the tool on standard unit test scenarios and bene t from the exhaustive traversal performed by a code model checker, which is employed inside UnitCheck. Two well-known Java tools are integrated in UnitCheck. JUnit is used as a testing framework and Java PathFinder provides the model checking capability. The UnitCheck plugin for Eclipse presents the checking results in a convenient way known from unit testing, while providing also a verbose output for the expert users. The UnitCheck Ant task allows to incorporate unit checking in the standard Java development and build process.
|
|
|
Konvertor Word-to-LaTeX
Kebrt, Michal ; Kopecký, Michal (oponent) ; Skopal, Tomáš (vedoucí práce)
V předložené práci popisuji program Word-to-LATEX - konvertor převádějící dokumenty ve formátu Microsoft Word do formátu LATEX, který je vhodný pro sazbu knih, skript, vědeckých článků atp. Program je však konfigurovatelný do té míry, že umožňuje převádět dokumenty i do zcela odlišných formátů (např. XML). Součástí práce je srovnání textových procesorů a formátu LATEX, vyzdvižení jejich výhod a nevýhod. Stručně jsou popsány základy objektového modelu programu Microsoft Word, možnosti jeho použití, několik jeho problémů a omezení a způsob jak urychlit aplikace, které jej využívají.
|
host ::
RSS.