<?xml version="1.0" encoding="utf-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="10 15 718 319" width="718pt" height="319pt" xmlns:dc="http://purl.org/dc/elements/1.1/"><metadata> Produced by OmniGraffle 6.1 <dc:date>2014-12-05 00:34:03 +0000</dc:date></metadata><defs><font-face font-family="Courier" font-size="10" units-per-em="1000" underline-position="-144.04297" underline-thickness="91.796875" slope="0" x-height="462.40234" cap-height="594.72656" ascent="753.90625" descent="-246.09375" font-weight="bold"><font-face-src><font-face-name name="Courier-Bold"/></font-face-src></font-face><font-face font-family="Courier" font-size="10" units-per-em="1000" underline-position="-178.22266" underline-thickness="57.617188" slope="0" x-height="462.40234" cap-height="594.72656" ascent="753.90625" descent="-246.09375" font-weight="500"><font-face-src><font-face-name name="Courier"/></font-face-src></font-face><font-face font-family="Helvetica" font-size="9" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"><font-face-src><font-face-name name="Helvetica"/></font-face-src></font-face><font-face font-family="Helvetica" font-size="9" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="532.22656" cap-height="719.72656" ascent="770.01953" descent="-229.98047" font-weight="bold"><font-face-src><font-face-name name="Helvetica-Bold"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="UMLInheritance_Marker" viewBox="-1 -8 14 16" markerWidth="14" markerHeight="16" color="black"><g><path d="M 12 0 L 0 -7 L 0 7 Z" fill="none" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Helvetica" font-size="10" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"><font-face-src><font-face-name name="Helvetica"/></font-face-src></font-face><font-face font-family="Helvetica" font-size="12" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="-1e3" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-style="italic" font-weight="500"><font-face-src><font-face-name name="Helvetica-Oblique"/></font-face-src></font-face></defs><g stroke="none" stroke-opacity="1" stroke-dasharray="none" fill="none" fill-opacity="1"><title>Canvas 1</title><rect fill="white" width="756" height="553"/><g><title>Layer 1</title><text transform="translate(339.4 252.055)" fill="blue"><tspan font-family="Courier" font-size="10" font-weight="bold" fill="blue" x="0" y="10" textLength="30.004883">@Test</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="30.004883" y="10" textLength="78.012695"> public void </tspan><tspan font-family="Courier" font-size="10" font-weight="bold" fill="blue" x="108.01758" y="10" textLength="30.004883">testX</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="138.02246" y="10" textLength="24.003906">() {</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="22" textLength="216.03516">  if (verifyNoPropertyViolation()) {</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="34" textLength="24.003906">    </tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="red" x="24.003906" y="34" textLength="156.02539">String s = &quot;one&quot; + &quot; two&quot;;</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="red" x="0" y="46" textLength="186.03027">    assert &quot;one two&quot;.equals(s);</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="58" textLength="18.00293">  }</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="70" textLength="6.0009766">}</tspan></text><path d="M 361.58823 277.92 L 528.48 277.92 L 528.48 299.92 L 361.58823 299.92 Z" stroke="#fd7673" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/><path d="M 196.644 234.841 L 314.109 234.841 C 317.4227 234.841 320.109 237.52729 320.109 240.841 L 320.109 307.503 C 320.109 310.8167 317.4227 313.503 314.109 313.503 L 196.644 313.503 C 193.33029 313.503 190.644 310.8167 190.644 307.503 L 190.644 240.841 C 190.644 237.52729 193.33029 234.841 196.644 234.841 Z" fill="#e9ffe4"/><path d="M 196.644 234.841 L 314.109 234.841 C 317.4227 234.841 320.109 237.52729 320.109 240.841 L 320.109 307.503 C 320.109 310.8167 317.4227 313.503 314.109 313.503 L 196.644 313.503 C 193.33029 313.503 190.644 310.8167 190.644 307.503 L 190.644 240.841 C 190.644 237.52729 193.33029 234.841 196.644 234.841 Z" stroke="#aeffa8" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 85.6174 26.126 L 364.9384 26.126 C 368.2521 26.126 370.9384 28.812292 370.9384 32.126 L 370.9384 199.694 C 370.9384 203.00771 368.2521 205.694 364.9384 205.694 L 85.6174 205.694 C 82.30369 205.694 79.6174 203.00771 79.6174 199.694 L 79.6174 32.126 C 79.6174 28.812292 82.30369 26.126 85.6174 26.126 Z" fill="#fff8e0"/><path d="M 85.6174 26.126 L 364.9384 26.126 C 368.2521 26.126 370.9384 28.812292 370.9384 32.126 L 370.9384 199.694 C 370.9384 203.00771 368.2521 205.694 364.9384 205.694 L 85.6174 205.694 C 82.30369 205.694 79.6174 203.00771 79.6174 199.694 L 79.6174 32.126 C 79.6174 28.812292 82.30369 26.126 85.6174 26.126 Z" stroke="#ffcf9c" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(382.995 68.2183)" fill="blue"><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="10" textLength="48.007812">boolean </tspan><tspan font-family="Courier" font-size="10" font-weight="bold" fill="blue" x="48.007812" y="10" textLength="150.02441">verifyNoPropertyViolation</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="198.03223" y="10" textLength="132.021484"> (String... jpfArgs) {</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="22" textLength="30.004883">  ...</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="34" textLength="282.0459">  args = append(jpfArgs, caller.getClassName(),</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="46" textLength="294.04785">                         caller.getMethodName());</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="58" textLength="36.00586">    ..</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="70" textLength="216.03516">    JPF jpf = createAndRunJPF(args);</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="82" textLength="42.006836">    ...</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="94" textLength="210.03418">    errors = jpf.getSearchErrors();</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="106" textLength="156.02539">    if (!errors.isEmpty())</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="118" textLength="210.03418">      throw new AssertionError(..);</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="130" textLength="42.006836">    ...</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="142" textLength="276.04492">  return false; // -&gt; don&apos;t execute test block</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="154" textLength="6.0009766">}</tspan></text><text transform="translate(24.5953 63.4089)" fill="blue"><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="10" textLength="48.007812">boolean </tspan><tspan font-family="Courier" font-size="10" font-weight="bold" fill="blue" x="48.007812" y="10" textLength="150.02441">verifyNoPropertyViolation</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="198.03223" y="10" textLength="30.004883">(..){</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="22" textLength="84.01367">  return true;</tspan><tspan font-family="Courier" font-size="10" font-weight="500" fill="blue" x="0" y="34" textLength="6.0009766">}</tspan></text><rect x="251.28" y="45.6337" width="90" height="11" fill="white"/><rect x="251.28" y="45.6337" width="90" height="11" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(256.28 45.6337)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="9" textLength="23.497559">start()</tspan></text><rect x="251.28" y="34.6337" width="90" height="11" fill="white"/><rect x="251.28" y="34.6337" width="90" height="11" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(256.28 34.6337)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="bold" x="20.993652" y="9" textLength="38.012695">JPFShell</tspan></text><rect x="231.548" y="95.3416" width="129.465" height="88" fill="white"/><rect x="231.548" y="95.3416" width="129.465" height="88" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(236.548 95.3416)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="9" textLength="18.505371">runT</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="17.507812" y="9" textLength="71.507812">estsOfThisClass()</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="20" textLength="79.532227">createAndRunJPF()</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="31" textLength="7.501465">...</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="42" textLength="73.023926">verifyNoPropertyV</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="72.865723" y="42" textLength="34.514648">iolation()</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="53" textLength="61.519043">verifyPropertyV</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="61.36084" y="53" textLength="34.514648">iolation()</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="64" textLength="110.55762">verifyUnhandledException()</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="75" textLength="85.012207">verifyAssertionError()</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="86" textLength="7.501465">...</tspan></text><rect x="231.548" y="84.3416" width="129.465" height="11" fill="white"/><rect x="231.548" y="84.3416" width="129.465" height="11" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(236.548 84.3416)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="bold" x="42.558672" y="9" textLength="5.4975586">T</tspan><tspan font-family="Helvetica" font-size="9" font-weight="bold" x="47.392656" y="9" textLength="29.513672">estJPF</tspan></text><rect x="208.904" y="253.802" width="90" height="22" fill="white"/><rect x="208.904" y="253.802" width="90" height="22" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(213.904 253.802)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="9" textLength="26.503418">testX()</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="20" textLength="7.501465">...</tspan></text><rect x="208.904" y="242.802" width="90" height="11" fill="white"/><rect x="208.904" y="242.802" width="90" height="11" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(213.904 242.802)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="bold" x="1.3193359" y="9" textLength="65.01709">MyJPFProjectT</tspan><tspan font-family="Helvetica" font-size="9" font-weight="bold" x="65.67285" y="9" textLength="13.0078125">est</tspan></text><line x1="296.28021" y1="84.3416" x2="296.28013" y2="70.1337" marker-end="url(#UMLInheritance_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="253.904" y1="242.802" x2="253.904" y2="196.842" marker-end="url(#UMLInheritance_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(96.2759 34.6337)" fill="black"><tspan font-family="Helvetica" font-size="10" font-weight="500" x=".32763672" y="10" textLength="33.344727">jpf-core</tspan></text><text transform="translate(202.017 293.506)" fill="black"><tspan font-family="Helvetica" font-size="10" font-weight="500" x=".20458984" y="10" textLength="80.59082">tested JPF project</tspan></text><rect x="87.5524" y="117.184" width="129.465" height="44" fill="white"/><rect x="87.5524" y="117.184" width="129.465" height="44" stroke="#4f4f4f" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(92.5524 117.184)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="9" textLength="73.023926">verifyNoPropertyV</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="72.865723" y="9" textLength="34.514648">iolation()</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="20" textLength="61.519043">verifyPropertyV</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="61.36084" y="20" textLength="34.514648">iolation()</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="31" textLength="110.55762">verifyUnhandledException()</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="42" textLength="85.012207">verifyAssertionError()</tspan></text><rect x="87.5524" y="106.184" width="129.465" height="11" fill="white"/><rect x="87.5524" y="106.184" width="129.465" height="11" stroke="#4f4f4f" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(92.5524 106.184)" fill="#4f4f4f"><tspan font-family="Helvetica" font-size="9" font-weight="bold" fill="#4f4f4f" x="26.799883" y="9" textLength="37.015137">JPF_.._T</tspan><tspan font-family="Helvetica" font-size="9" font-weight="bold" fill="#4f4f4f" x="63.151445" y="9" textLength="29.513672">estJPF</tspan></text><line x1="217.0174" y1="133.75498" x2="231.548" y2="133.77092" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(127.285 89.2183)" fill="black"><tspan font-family="Helvetica" font-size="10" font-weight="500" x=".26123047" y="10" textLength="49.47754">native peer</tspan></text><text transform="translate(538.274 280.529)" fill="red"><tspan font-family="Helvetica" font-size="10" font-weight="500" fill="red" x=".20214844" y="10" textLength="45.576172">code verifi</tspan><tspan font-family="Helvetica" font-size="10" font-weight="500" fill="red" x="45.77832" y="10" textLength="45.01953">ed by JPF</tspan></text><text transform="translate(39.189 166.149)" fill="black"><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" x="0" y="11" textLength="121.40039">executed by JPF when</tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" x="0" y="25" textLength="62.70703">running test</tspan></text><text transform="translate(355.357 34.6337)" fill="black"><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" x="0" y="11" textLength="118.734375">executed outside JPF </tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" x="0" y="25" textLength="111.36914">(starting JPF on test)</tspan></text></g></g></svg>