{"id":723,"date":"2016-08-31T17:45:51","date_gmt":"2016-08-31T15:45:51","guid":{"rendered":"http:\/\/hudecekpetr.cz\/?p=723"},"modified":"2016-08-31T17:45:51","modified_gmt":"2016-08-31T15:45:51","slug":"java-pathfinder-inspector","status":"publish","type":"post","link":"https:\/\/hudecekpetr.cz\/cs\/java-pathfinder-inspector\/","title":{"rendered":"Java Pathfinder Inspector"},"content":{"rendered":"<p>P\u0159es l\u00e9to 2016 jsem se \u00fa\u010dastnil\u00a0<a href=\"https:\/\/en.wikipedia.org\/wiki\/Google_Summer_of_Code\">programu Google Summer of Code<\/a>, b\u011bhem n\u011bj\u017e jsem aktualizoval a zna\u010dn\u011b vylep\u0161il aplikaci zvanou\u00a0Java Pathfinder Inspector.<\/p>\n<p><strong>Java Pathfinder<\/strong> (JPF) is framework pro form\u00e1ln\u00ed kontrolu program\u016f napsan\u00fdch v Jav\u011b. Jeho j\u00e1dro sest\u00e1v\u00e1 z virtu\u00e1ln\u00edho stroje pro bajtk\u00f3d, kter\u00fd s\u00e1m b\u011b\u017e\u00ed v Jav\u011b; to umo\u017en\u00ed, aby JPF instrumentoval k\u00f3d a nahradil kritick\u00e9 instrukce sv\u00fdmi vlastn\u00edmi variantami. JPF je velmi roz\u0161i\u0159iteln\u00fd a existuje mnoh modul\u016f pro r\u016fzn\u00e9 druhy verifikace jako nap\u0159\u00edklad modul pro symbolickou exekuci. JPF Inspector je jedn\u00edm takov\u00fdm modulem a soust\u0159ed\u00ed se na mo\u017enost lad\u011bn\u00ed.<\/p>\n<p><strong>JPF Inspector<\/strong>\u00a0je n\u00e1stroj pro pozorov\u00e1n\u00ed a kontrolu b\u011bhu programu spu\u0161t\u011bn\u00e9ho na virtu\u00e1ln\u00edm stroji\u00a0<a href=\"http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/\">Java Pathfinder<\/a>. Podporuje breakpoiny, krokov\u00e1n\u00ed (dop\u0159edu i dozadu), a to na n\u011bkolika \u00farovn\u00edch granularity, a umo\u017e\u0148uje u\u017eivateli pozastavit program a prozkoumat jeho sou\u010dasn\u00fd stav (vl\u00e1kna, z\u00e1sobn\u00edky, prom\u011bnn\u00e9, objekty na hald\u011b). Oproti standartn\u00edm debugger\u016fm jako GDB tak\u00e9 umo\u017e\u0148uje explicitn\u00ed pl\u00e1nov\u00e1n\u00ed vl\u00e1ken.<\/p>\n<p>Toto je prvn\u00ed softwarov\u00fd projekt, za kter\u00fd jsem dostal skute\u010dn\u00e9 pen\u00edze.<\/p>\n<p>Je naprogramovan\u00fd v Jav\u011b.<\/p>\n<p>Na tomto projektu jsem pracoval ve v\u011bku 23 let, v roce 2016.<\/p>\n<div id='gallery-2' class='gallery galleryid-723 gallery-columns-2 gallery-size-medium'><figure class='gallery-item'>\n\t\t\t<div class='gallery-icon landscape'>\n\t\t\t\t<a href='https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/EmptyConsole.png'><img loading=\"lazy\" decoding=\"async\" width=\"300\" height=\"180\" src=\"https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/EmptyConsole-300x180.png\" class=\"attachment-medium size-medium\" alt=\"\" aria-describedby=\"gallery-2-724\" srcset=\"https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/EmptyConsole-300x180.png 300w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/EmptyConsole-768x462.png 768w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/EmptyConsole-800x481.png 800w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/EmptyConsole-600x361.png 600w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/EmptyConsole.png 986w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a>\n\t\t\t<\/div>\n\t\t\t\t<figcaption class='wp-caption-text gallery-caption' id='gallery-2-724'>\n\t\t\t\tThe console is the primary input\/ouput method.\n\t\t\t\t<\/figcaption><\/figure><figure class='gallery-item'>\n\t\t\t<div class='gallery-icon landscape'>\n\t\t\t\t<a href='https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/Explorer.png'><img loading=\"lazy\" decoding=\"async\" width=\"300\" height=\"180\" src=\"https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/Explorer-300x180.png\" class=\"attachment-medium size-medium\" alt=\"\" aria-describedby=\"gallery-2-725\" srcset=\"https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/Explorer-300x180.png 300w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/Explorer-768x462.png 768w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/Explorer-800x481.png 800w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/Explorer-600x361.png 600w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/Explorer.png 986w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a>\n\t\t\t<\/div>\n\t\t\t\t<figcaption class='wp-caption-text gallery-caption' id='gallery-2-725'>\n\t\t\t\tIn the Explorer, the user may view values of all variables.\n\t\t\t\t<\/figcaption><\/figure><figure class='gallery-item'>\n\t\t\t<div class='gallery-icon landscape'>\n\t\t\t\t<a href='https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/SourceView.png'><img loading=\"lazy\" decoding=\"async\" width=\"300\" height=\"180\" src=\"https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/SourceView-300x180.png\" class=\"attachment-medium size-medium\" alt=\"\" aria-describedby=\"gallery-2-726\" srcset=\"https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/SourceView-300x180.png 300w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/SourceView-768x462.png 768w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/SourceView-800x481.png 800w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/SourceView-600x361.png 600w, https:\/\/hudecekpetr.cz\/wp-content\/uploads\/2016\/08\/SourceView.png 986w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a>\n\t\t\t<\/div>\n\t\t\t\t<figcaption class='wp-caption-text gallery-caption' id='gallery-2-726'>\n\t\t\t\tThe source code view shows the line that is about to be executed.\n\t\t\t\t<\/figcaption><\/figure>\n\t\t<\/div>\n\n<p><!--more--><\/p>\n<p><strong>Odkazy:<\/strong><\/p>\n<ul>\n<li><a href=\"https:\/\/github.com\/d3sformal\/jpf-inspector\"><strong>Hlavn\u00ed repozit\u00e1\u0159 na GitHubu<\/strong><\/a><\/li>\n<li><a href=\"https:\/\/github.com\/d3sformal\/jpf-inspector\/wiki\">Hlavn\u00ed dokumentace<\/a><\/li>\n<li><a href=\"https:\/\/github.com\/Soothsilver\/gsoc-inspector\">Repozit\u00ed\u00e1\u0159 na GitHubu, kter\u00fd jsem pou\u017e\u00edval b\u011bhem l\u00e9ta 2016<\/a><\/li>\n<li><a href=\"https:\/\/github.com\/Soothsilver\/gsoc-inspector\/wiki\/2016-Changelog\">Seznam m\u00fdch nejd\u016fle\u017eit\u011bj\u0161\u00edch zm\u011bn<\/a><\/li>\n<li><a href=\"http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/\">Hlavn\u00ed str\u00e1nka Java Pathfinderu<\/a><\/li>\n<\/ul>\n<p><strong>Vybran\u00e9 nejd\u016fle\u017eit\u011bj\u0161\u00ed zm\u011bny, kter\u00e9 jsem provedl na projektu (<a href=\"https:\/\/github.com\/Soothsilver\/gsoc-inspector\/wiki\/2016-Changelog\">\u00fapln\u00fd seznam<\/a>):<\/strong><\/p>\n<ul>\n<li>Roz\u0161i\u0159itelnost: vlastn\u00ed p\u0159\u00edkazy, alias, podm\u00ednky pro p\u0159eru\u0161en\u00ed<\/li>\n<li>M\u00f3d pro p\u0159\u00edkazovou \u0159\u00e1dku<\/li>\n<li>Pr\u016fzkumn\u00edk, zobrazova\u010d zdrojov\u00e9ho k\u00f3du, rychl\u00e9 p\u0159\u00edkazy<\/li>\n<li>10 nov\u00fdch p\u0159\u00edkaz\u016f a 9 nov\u00fdch podm\u00ednek pro p\u0159eru\u0161en\u00ed<\/li>\n<li>Velmi podrobn\u00e1 dokumentace<\/li>\n<\/ul>\n<p><\/p>","protected":false},"excerpt":{"rendered":"<p>In the summer of 2016, I participated in the Google Summer of Code program, during which I updated and significantly improved the Java Pathfinder Inspector. Java Pathfinder (JPF) is a framework for formal checking of Java programs. Its core consists of a virtual machine for Java bytecode, running itself on Java; this allows JPF to [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-723","post","type-post","status-publish","format-standard","hentry","category-uncategorized"],"_links":{"self":[{"href":"https:\/\/hudecekpetr.cz\/cs\/wp-json\/wp\/v2\/posts\/723","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/hudecekpetr.cz\/cs\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/hudecekpetr.cz\/cs\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/hudecekpetr.cz\/cs\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/hudecekpetr.cz\/cs\/wp-json\/wp\/v2\/comments?post=723"}],"version-history":[{"count":1,"href":"https:\/\/hudecekpetr.cz\/cs\/wp-json\/wp\/v2\/posts\/723\/revisions"}],"predecessor-version":[{"id":727,"href":"https:\/\/hudecekpetr.cz\/cs\/wp-json\/wp\/v2\/posts\/723\/revisions\/727"}],"wp:attachment":[{"href":"https:\/\/hudecekpetr.cz\/cs\/wp-json\/wp\/v2\/media?parent=723"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/hudecekpetr.cz\/cs\/wp-json\/wp\/v2\/categories?post=723"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/hudecekpetr.cz\/cs\/wp-json\/wp\/v2\/tags?post=723"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}