|
|
Unit checking for Java IDE
Kebrt, Michal ; Šerý, Ondřej (advisor) ; Parízek, Pavel (referee)
Model checking programů představuje rychle se rozvíjejích oblast výzkumu. Bohužel tato technika zatím není kromě několika speciálních případů (např. veri fikace ovladačů pomocí nástroje SLAM) příliš rozšířena ve standardním procesu vývoje software. Věříme ovšem, že by mohla nastat změna, pokud by vývojáři měli možnost používat nástroje z oblasti techniky model checking podobným způsobem jako používají nástroje pro testování. Tato práce prezentuje nátroj UnitCheck, který doplňuje standardní testování Java tříd (unit testing) o metodu model checking. Vývojáři, kteří běžně využívají unit testování, mohou tento nástroj aplikovat na standardní testovací scénáře a díky části provádějící model checking (model checker) integrované v nástroji UnitCheck tak využít možnost průchodu celým stavovým prostorem daného testu. UnitCheck v sobě integruje dva dobře známé nástroje z oblasti programování v jazyce Java. JUnit je použit jako testovací framework, zatímco Java PathFinder umožňuje provádět model checking vstupních testů. Součástí celého nástroje je plugin pro prostředí Eclipse, který přehledně zobrazuje výsledky testů způsobem známým z unit testování a pokročilým uživatelům zároveň umožňuje prohlédnout si podrobnšjší informace. UnitCheck je také integrován do nástroje Ant, což umožňuje spouštět kontrolu testů (unit...
|
|
|
Unit checking for Java IDE
Kebrt, Michal ; Parízek, Pavel (referee) ; Šerý, Ondřej (advisor)
Model checking programů představuje rychle se rozvíjejích oblast výzkumu. Bohužel tato technika zatím není kromě několika speciálních případů (např. veri fikace ovladačů pomocí nástroje SLAM) příliš rozšířena ve standardním procesu vývoje software. Věříme ovšem, že by mohla nastat změna, pokud by vývojáři měli možnost používat nástroje z oblasti techniky model checking podobným způsobem jako používají nástroje pro testování. Tato práce prezentuje nátroj UnitCheck, který doplňuje standardní testování Java tříd (unit testing) o metodu model checking. Vývojáři, kteří běžně využívají unit testování, mohou tento nástroj aplikovat na standardní testovací scénáře a díky části provádějící model checking (model checker) integrované v nástroji UnitCheck tak využít možnost průchodu celým stavovým prostorem daného testu. UnitCheck v sobě integruje dva dobře známé nástroje z oblasti programování v jazyce Java. JUnit je použit jako testovací framework, zatímco Java PathFinder umožňuje provádět model checking vstupních testů. Součástí celého nástroje je plugin pro prostředí Eclipse, který přehledně zobrazuje výsledky testů způsobem známým z unit testování a pokročilým uživatelům zároveň umožňuje prohlédnout si podrobnšjší informace. UnitCheck je také integrován do nástroje Ant, což umožňuje spouštět kontrolu testů (unit...
|
|
|
Konvertor Word-to-LaTeX
Kebrt, Michal ; Kopecký, Michal (referee) ; Skopal, Tomáš (advisor)
This work is devoted to Word-to-LATEX program that converts documents written in Microsoft Word into LATEX format which is suitable for typesetting books, manuscripts, scientiffic articles, etc. The program can be customized so much that it enables to produce completely different output formats (e.g. XML). In this work I also tried to compare text processors and LATEX format and emphasise their pros and cons. The Microsoft Word object model is briefly described, its problems and limitations are also covered. Finally, the way of improving performance of applications that automate Word is suggested.
|
guest ::
