\batchmode


\documentclass{article}
\makeatletter

\usepackage{myway}
\usepackage{latexsym}
\usepackage{epsf,epsfig}
\usepackage{url}
\usepackage{/usr/local/apps2/latex2html/texinputs/html}





	  		      
















 








































														



			             			












												







\newlength{\lindent}
\setlength{\lindent}{\parindent}




























































                                                                                       




                         
               
































































































 

























































































                        
                       








                          


























































































               


     
  


























                                 































              
















































  












































                





















































































































































\title{The Bandera Tools for Model-checking Java Source Code: \\ 
       A User's Manual}

\author{John Hatcliff and Oksana Tkachuk}

\date{\today}



\newcommand {\menuft}[1]{{\bf #1}}

\newcommand {\dsb}[1]{[\![{#1}]\!]}

\newcommand {\ssb}[1]{[{#1}]}

\newcommand {\sab}[1]{\langle{#1}\rangle}

\newcommand {\dab}[1]{\langle\![ #1 ]\!\rangle}

\newcommand {\synbraces}[1]{\dab{#1}}

\newcommand {\SynTra}[2]{\synbraces{#1}^{#2}}

\newcommand {\ie}{{\it i.e.}}

\newcommand {\eg}{{\it e.g.}}

\newcommand {\etc}{{\it etc.}}

\newcommand {\vs}{{\it vs.}}

\newcommand {\cf}{{\it cf.}}

\newcommand {\etal}{{\it et al.}}

\newcommand {\via}{{\it via}}

\renewcommand {\k}{\kappa}

\newcommand {\g}{\gamma}

\renewcommand {\r}{\rho}

\renewcommand {\t}{\theta}

\renewcommand {\l}{\lambda}

\newcommand {\lam}{$\lambda$}

\newtheorem {lemma}{Lemma}

\newtheorem {definition}{Definition}

\newtheorem {theorem}{Theorem}

\newtheorem {proposition}{Proposition}

\newtheorem {property}{Property}

\newtheorem {proof}{Proof}

\newtheorem {conjecture}{Conjecture}

\newtheorem {principle}{Principle}

\newtheorem {corollary}{Corollary}

\newtheorem {consequence}{Consequence}

\newtheorem {observation}{Observation}

\newtheorem {example}{Example}

\newtheorem {requirement}{Requirement}

\newcommand {\proves}[2]{{#1}\,\vdash\,{#2}}

\newcommand {\notproves}[2]{{#1}\,\not\vdash\,{#2}}

\newcommand {\defeq}{\stackrel{\rm def}{=}}

\newcommand {\notimplies}{\not\Rightarrow}

\newcommand {\compose}[2]{{#1}\,\circ\,{#2}}

\newcommand {\myand}{\wedge}

\newcommand {\myor}{\vee}

\newcommand {\eqcor}{\simeq}

\newcommand {\hs}[1]{\hspace{#1}}

\newcommand {\hsi}{\hs{.5cm}}

\newcommand {\hsii}{\hs{1cm}}

\newcommand {\hsiii}{\hs{1.5cm}}

\newcommand {\ignore}[1]{}

\newcommand {\lFCL}{\mbox{\rm FCL}}

\newcommand {\lFCLtwo}{\mbox{\rm FCL-2}}

\newcommand {\subst}[3]{{#1}[{#2}\,:=\,{#3}]}

\newcommand {\cxtvar}{{\it C}}

\newcommand {\cxtemp}[1]{\ssb{#1}}

\newcommand {\cxtstd}[1]{\cxtvar\cxtemp{#1}}

\newcommand {\cxtstdt}[1]{\cxtvar\tau\cxtemp{#1}}

\newcommand {\fv}[1]{\mbox{\it FV}({#1})}

\newcommand {\quantdot}{\:.\:}

\newcommand {\hole}{\cdot}

\newcommand {\cxttrvf}[1]{[{#1}]}

\newcommand {\cxtapp}[2]{{#1}{\cxttrvf{#2}}}

\newcommand {\cxttrv}{\cxttrvf{\cdot}}

\newcommand {\rawiff}{\mbox{\it iff}}

\newcommand {\obeq}{\approx}

\newcommand {\obapprox}{\sqsubseteq}

\newcommand {\keq}{\simeq}

\newcommand {\rawtaurel}{\stackrel{\rtau}{\sim}}

\newcommand {\rawcontrelb}{\stackrel{\circ}{\sim}}

\newcommand {\sr}{\longmapsto}

\newcommand {\src}{\longmapsto^{*}}

\newcommand {\srd}{\longmapsto^{+}}

\newcommand {\srn}{\sr_{\rm n}}

\newcommand {\srv}{\sr_{\rm v}}

\newcommand {\srg}{\sr_{i}}

\newcommand {\srnc}{\srn^{*}}

\newcommand {\srrule}[2]{\begin{array}{c} {#1} \\  \hline {#2} \end{array}}

\newcommand {\srrulesp}{\;\;\;\;\;\;}

\newcommand {\annot}[1]{\mbox{\em ...{#1}}}

\newenvironment {myindent}[2]{\begin{list}{}{\setlength{\leftmargin}{#1}
			       \setlength{\rightmargin}{#2}
			       \setlength{\itemindent}{0cm}}\item []}{\end{list}}

\newenvironment {proofind}{\begin{myindent}{\lindent}{0cm}}{\end{myindent}}

\newenvironment {myitemize}[1]{\begin{itemize}\setlength{\itemsep}{#1}}{\end{itemize}}

\newenvironment {myenumerate}[1]{\begin{enumerate}\setlength{\itemsep}{#1}}{\end{enumerate}}

\newcommand {\BBox}{\rule{1ex}{.75em}}

\renewenvironment {proof}{\noindent{\bf Proof:}}{\hfill\BBox}

\newenvironment {proofof}[1]{\begin{trivlist}\item\noindent{\bf Proof of {#1}:}}{\hfill\BBox\end{trivlist}}

\newenvironment {steps}{\begin{proofind}\begin{tabbing}case \= \hspace{\lindent} 
					   \= \hspace{\lindent} 
					   \= \hspace{\lindent} 
					   \= \hspace{\lindent} 
					   \= \hspace{\lindent} 
					   \= \hspace{\lindent} 
					   \kill}{\end{tabbing}\end{proofind}}

\newcommand {\step}[1]{\parbox[t]{12cm}{#1}}

\newcommand {\steptab}[1]{\begin{minipage}[t]{12cm} {#1} \end{minipage}}

\newcommand {\sdfont}{\rm}

\newcommand {\rawprograms}{\mbox{\sdfont Programs}}

\newcommand {\rawblocks}{\mbox{\sdfont Blocks}}

\newcommand {\rawblocklabels}{\mbox{\sdfont Block-Labels}}

\newcommand {\rawassignments}{\mbox{\sdfont Assignments}}

\newcommand {\rawassignmentlists}{\mbox{\sdfont Assignment-Lists}}

\newcommand {\rawvariables}{\mbox{\sdfont Variables}}

\newcommand {\rawvars}{\mbox{\sdfont Vars}}

\newcommand {\rawexpressions}{\mbox{\sdfont Expressions}}

\newcommand {\rawconstants}{\mbox{\sdfont Constants}}

\newcommand {\rawjumps}{\mbox{\sdfont Jumps}}

\newcommand {\rawoperations}{\mbox{\sdfont Operations}}

\newcommand {\rawtests}{\mbox{\sdfont Tests}}

\newcommand {\programs}[1]{\rawprograms[{#1}]}

\newcommand {\blocks}[1]{\rawblocks[{#1}]}

\newcommand {\blocklabels}[1]{\rawblocklabels[{#1}]}

\newcommand {\assignments}[1]{\rawassignments[{#1}]}

\newcommand {\assignmentlists}[1]{\rawassignmentlists[{#1}]}

\newcommand {\variables}[1]{\rawvariables[{#1}]}

\newcommand {\vars}[1]{\rawvars[{#1}]}

\newcommand {\expressions}[1]{\rawexpressions[{#1}]}

\newcommand {\constants}[1]{\rawconstants[{#1}]}

\newcommand {\jumps}[1]{\rawjumps[{#1}]}

\newcommand {\operations}[1]{\rawoperations[{#1}]}

\newcommand {\tests}[1]{\rawtests[{#1}]}

\newcommand {\programsfcl}{\programs{\lFCL}}

\newcommand {\blocksfcl}{\blocks{\lFCL}}

\newcommand {\blocklabelsfcl}{\blocklabels{\lFCL}}

\newcommand {\assignmentsfcl}{\assignments{\lFCL}}

\newcommand {\assignmentlistsfcl}{\assignmentlists{\lFCL}}

\newcommand {\variablesfcl}{\variables{\lFCL}}

\newcommand {\expressionsfcl}{\expressions{\lFCL}}

\newcommand {\constantsfcl}{\constants{\lFCL}}

\newcommand {\jumpsfcl}{\jumps{\lFCL}}

\newcommand {\operationsfcl}{\operations{\lFCL}}

\newcommand {\testsfcl}{\tests{\lFCL}}

\newcommand {\sigfont}{\sf}

\newcommand {\sigv}{\Sigma}

\newcommand {\signum}{\sigv_{num}}

\newcommand {\signumeo}{\sigv_{num-eo}}

\newcommand {\sigeo}{\sigv_{eo}}

\newcommand {\sigres}{\sigv_{res}}

\newcommand {\sigtup}[2]{({#1}\,,\,{#2})}

\newcommand {\sigops}{\operationssig}

\newcommand {\sigtests}{\testssig}

\newcommand {\rawarity}{\mbox{\sf arity}}

\newcommand {\rawcard}{\mbox{\sf card}}

\newcommand {\rawaritysm}{\mbox{\scriptsize \sf arity}}

\newcommand {\arity}[1]{\rawarity({#1})}

\newcommand {\aritysm}[1]{\rawaritysm({#1})}

\newcommand {\card}[1]{\rawcard({#1})}

\newcommand {\algv}{{\it A}}

\newcommand {\algres}{\algv_{res}}

\newcommand {\algcarrier}[1]{\values{#1}}

\newcommand {\algops}[1]{\operations{#1}}

\newcommand {\algtests}[1]{\tests{#1}}

\newcommand {\algcarriers}{\algcarrier{\algv}}

\newcommand {\algopss}{\algops{\algv}}

\newcommand {\algtestss}{\algtests{\algv}}

\newcommand {\lesssym}{\sqsubseteq}

\newcommand {\lesssyms}{\lesssym_{\algv}}

\newcommand {\less}[2]{{#1}\,\lesssym\,{#2}}

\newcommand {\strictlesssym}{\sqsubset}

\newcommand {\strictlesssyms}{\lesssym_{\algv}}

\newcommand {\strictless}[2]{{#1}\,\strictlesssym\,{#2}}

\newcommand {\equal}[2]{{#1}\,=\,{#2}}

\newcommand {\algopv}[1]{\opv_{#1}}

\newcommand {\algtestv}[1]{\testv_{#1}}

\newcommand {\algopvs}{\algopv{\algv}}

\newcommand {\algtestvs}{\algtestv{\algv}}

\newcommand {\algcon}{\algv_{\mbox{\scriptsize con}}}

\newcommand {\algabs}{\algv_{\mbox{\scriptsize abs}}}

\newcommand {\algeo}{\algv_{\mbox{\scriptsize eo}}}

\newcommand {\algnum}{\algv_{\mbox{\scriptsize num}}}

\newcommand {\abssym}{\alpha}

\newcommand {\abseosym}{\alpha_{eo}}

\newcommand {\abseopsym}{\alpha'_{eo}}

\newcommand {\consym}{\gamma}

\newcommand {\abs}[1]{\abssym({#1})}

\newcommand {\abseo}[1]{\abseosym({#1})}

\newcommand {\abseop}[1]{\abseopsym({#1})}

\newcommand {\con}[1]{\consym({#1})}

\newcommand {\liftsym}{\mbox{\it lift}}

\newcommand {\liftinvsym}{\mbox{\it lift}^{-1}}

\newcommand {\lift}[1]{\liftsym({#1})}

\newcommand {\liftinv}[1]{\liftinvsym({#1})}

\newcommand {\sstructv}{\Xi}

\newcommand {\sstruct}[7]{({#1},{#2},{#3},{#4},{#5},{#6},{#7})}

\newcommand {\resvaluesv}{R}

\newcommand {\defined}[1]{{#1}\!\downarrow}

\newcommand {\undefined}[1]{{#1}\!\uparrow}

\newcommand {\safesym}{\lhd}

\newcommand {\safe}[2]{{#1}\,\lhd\,{#2}}

\newcommand {\even}{\mbox{\it even}}

\newcommand {\odd}{\mbox{\it odd}}

\newcommand {\evenop}{\prg{even}}

\newcommand {\oddop}{\prg{odd}}

\newcommand {\addop}{\mbox{\it add}}

\newcommand {\subop}{\mbox{\it sub}}

\newcommand {\multop}{\mbox{\it mult}}

\newcommand {\equalt}{\mbox{\it equal?}}

\newcommand {\event}{\mbox{\it even?}}

\newcommand {\programssig}{\programs{\sigv}}

\newcommand {\blockssig}{\blocks{\sigv}}

\newcommand {\blocklabelssig}{\blocklabels{\sigv}}

\newcommand {\assignmentssig}{\assignments{\sigv}}

\newcommand {\assignmentlistssig}{\assignmentlists{\sigv}}

\newcommand {\variablessig}{\variables{\sigv}}

\newcommand {\expressionssig}{\expressions{\sigv}}

\newcommand {\constantssig}{\constants{\sigv}}

\newcommand {\jumpssig}{\jumps{\sigv}}

\newcommand {\progv}{p}

\newcommand {\blockv}{b}

\newcommand {\labelv}{l}

\newcommand {\assignv}{a}

\newcommand {\assignsv}{\assignv^*}

\newcommand {\assignlv}{al}

\newcommand {\expv}{e}

\newcommand {\varv}{x}

\newcommand {\constv}{c}

\newcommand {\jumpv}{j}

\newcommand {\opv}{o}

\newcommand {\testv}{t}

\newcommand {\twolevelv}[1]{\hat{#1}}

\newcommand {\progtwov}{\twolevelv{p}}

\newcommand {\blocktwov}{\twolevelv{b}}

\newcommand {\assigntwov}{\twolevelv{a}}

\newcommand {\assignltwov}{\twolevelv{al}}

\newcommand {\exptwov}{\twolevelv{e}}

\newcommand {\consttwov}{\twolevelv{c}}

\newcommand {\jumptwov}{\twolevelv{j}}

\newcommand {\rawgoto}{\mbox{\bf goto}}

\newcommand {\rawreturn}{\mbox{\bf return}}

\newcommand {\rawif}{\mbox{\bf if}}

\newcommand {\rawthen}{\mbox{\bf then}}

\newcommand {\rawelse}{\mbox{\bf else}}

\newcommand {\rawskip}{\mbox{\bf skip}}

\newcommand {\progast}[3]{{\bf (}{#1}{\bf )} \; {\bf (}{#2}{\bf )} \; {#3}}

\newcommand {\blockast}[3]{{#1}:\; {#2}\; {#3}}

\newcommand {\assignast}[2]{{#1} \; \mbox{\bf :=} \; {#2}}

\newcommand {\assignlast}[2]{{#1}\:{#2}}

\newcommand {\gotoast}[1]{\rawgoto \; {#1}}

\newcommand {\returnast}{\rawreturn}

\newcommand {\ifast}[3]{\rawif \; {#1} \; \rawthen \; {#2} \; \rawelse \; {#3}}

\newcommand {\applyast}[2]{{#1}{\bf (}{#2}{\bf )}}

\newcommand {\binapplyast}[3]{\applyast{#1}{{#2} \; {#3}}}

\newcommand {\opast}[1]{\prg{{#1}}}

\newcommand {\varast}[1]{\mbox{\tt {#1}}}

\newcommand {\skipast}{\rawskip}

\newcommand {\annast}[2]{{#1}\:\blined{#2}}

\newcommand {\vect}[1]{{#1}^*}

\newcommand {\rawdgoto}{\mbox{\bf \underline{goto}}}

\newcommand {\rawdreturn}{\mbox{\bf \underline{return}}}

\newcommand {\rawdif}{\mbox{\bf \underline{if}}}

\newcommand {\rawdthen}{\mbox{\bf \underline{then}}}

\newcommand {\rawdelse}{\mbox{\bf \underline{else}}}

\newcommand {\rawlift}{\mbox{\it lift}}

\newcommand {\dconstv}{\underline{\constv}}

\newcommand {\dassignast}[2]{{#1} \; \mbox{\bf \underline{:=}} \; {#2};}

\newcommand {\dgotoast}[1]{\rawdgoto \; {#1};}

\newcommand {\dreturnast}{\rawdreturn;}

\newcommand {\difast}[3]{\rawdif \; {#1} \; 
                        \rawdthen \; {#2} \; \rawdelse \; {#3};}

\newcommand {\dapplyast}[2]{{#1}\underline{(}{#2}\underline{)}}

\newcommand {\dbinapplyast}[3]{\dapplyast{#1}{{#2} \; {#3}}}

\newcommand {\dopast}[1]{\dprg{#1}}

\newcommand {\dvarast}[1]{\mbox{\tt \underline{#1}}}

\newcommand {\liftast}[1]{\rawlift({#1})}

\newcommand {\semdfont}{\rm}

\newcommand {\rawvalues}{\mbox{\semdfont Values}}

\newcommand {\rawlabels}{\mbox{\semdfont Labels}}

\newcommand {\rawstores}{\mbox{\semdfont Stores}}

\newcommand {\rawstates}{\mbox{\semdfont States}}

\newcommand {\rawnodes}{\mbox{\semdfont Nodes}}

\newcommand {\rawbmaps}{\mbox{\semdfont Block-Maps}}

\newcommand {\rawonpevalues}{\mbox{\semdfont PE-Values}}

\newcommand {\rawspecvalues}{\mbox{\semdfont Spec-Values}}

\newcommand {\rawabsvalues}{\mbox{\semdfont Abstract-Values}}

\newcommand {\rawindices}{\mbox{\semdfont Indices}}

\newcommand {\values}[1]{\rawvalues[{#1}]}

\newcommand {\labels}[1]{\rawlabels[{#1}]}

\newcommand {\stores}[1]{\rawstores[{#1}]}

\newcommand {\states}[1]{\rawstates[{#1}]}

\newcommand {\nodes}[1]{\rawnodes[{#1}]}

\newcommand {\bmaps}[1]{\rawbmaps[{#1}]}

\newcommand {\onpevalues}[1]{\rawonpevalues[{#1}]}

\newcommand {\specvalues}[1]{\rawspecvalues[{#1}]}

\newcommand {\absvalues}[1]{\rawabsvalues[{#1}]}

\newcommand {\indices}{\rawindices}

\newcommand {\valuesfcl}{\values{\lFCL}}

\newcommand {\labelsfcl}{\labels{\lFCL}}

\newcommand {\storesfcl}{\stores{\lFCL}}

\newcommand {\statesfcl}{\states{\lFCL}}

\newcommand {\nodesfcl}{\nodes{\lFCL}}

\newcommand {\bmapsfcl}{\bmaps{\lFCL}}

\newcommand {\onpevaluesfcl}{\onpevalues{\lFCL}}

\newcommand {\absvaluesfcl}{\absvalues{\lFCL}}

\newcommand {\valuessig}{\values{\sigv}}

\newcommand {\labelssig}{\labels{\sigv}}

\newcommand {\storessig}{\stores{\sigv}}

\newcommand {\bmapssig}{\bmaps{\sigv}}

\newcommand {\onpevaluessig}{\onpevalues{\sigv}}

\newcommand {\absvaluessig}{\absvalues{\sigv}}

\newcommand {\rawdomain}{\mbox{\it domain}}

\newcommand {\domain}[1]{\rawdomain({#1})}

\newcommand {\valv}{v}

\newcommand {\store}{\sigma}

\newcommand {\storeinit}{{\store_{\mbox{\scriptsize \it init}}}}

\newcommand {\storetuple}[1]{[{#1}]}

\newcommand {\lookup}[2]{{#1}({#2})}

\newcommand {\lookups}[1]{\lookup{\store}{#1}}

\newcommand {\update}[3]{{#1}\storetuple{\binding{#2}{#3}}}

\newcommand {\updates}[2]{\update{\store}{#1}{#2}}

\newcommand {\rawbinding}{\mapsto}

\newcommand {\binding}[2]{{#1} \rawbinding {#2}}

\newcommand {\blockmap}{\Gamma}

\newcommand {\blockmapr}{{\Gamma_{\mbox{\rm \tiny R}}}}

\newcommand {\rawtruevalue}{\mbox{\it true-value}}

\newcommand {\truevalue}[1]{\rawtruevalue({#1})}

\newcommand {\rawfalsevalue}{\mbox{\it false-value}}

\newcommand {\falsevalue}[1]{\rawfalsevalue({#1})}

\newcommand {\rawdynamicvalue}{\mbox{\it dynamic}}

\newcommand {\dynamicvalue}[1]{\rawdynamicvalue({#1})}

\newcommand {\halt}{\mbox{\sf halt}}

\newcommand {\tvalue}[1]{\dsb{#1}}

\newcommand {\algmap}[3]{\dsb{#3}^{#1}_{#2}}

\newcommand {\cons}[2]{{#1}\,::\,{#2}}

\newcommand {\nulllist}{[]}

\newcommand {\singletonlist}[1]{[{#1}]}

\newcommand {\append}[2]{{#1}\,+\!\!\!\!+\,\,{#2}}

\newcommand {\onatgconfig}[2]{\langle{#1}\,,\,{#2}\rangle}

\newcommand {\rawonatgtrans}{\longmapsto}

\newcommand {\onatgtrans}[2]{{#1}\:\rawonatgtrans\:{#2}}

\newcommand {\onatgtransc}[2]{{#1}\:\rawonatgtrans^*\:{#2}}

\newcommand {\onatgjudge}[2]{\vdash_{#1}\:{#2}}

\newcommand {\onpeconfig}[3]{\langle{#1}\,,\,{#2}\,,\,{#3}\rangle}

\newcommand {\gconfig}[1]{({#1})}

\newcommand {\rawonpetrans}{\longmapsto}

\newcommand {\onpetrans}[2]{{#1}\:\rawonatgtrans\:{#2}}

\newcommand {\onpetransc}[2]{{#1}\:\rawonatgtrans^*\:{#2}}

\newcommand {\onpejudge}[2]{\vdash_{#1}\:{#2}}

\newcommand {\pendingv}{{\cal P}}

\newcommand {\seenv}{{\cal S}}

\newcommand {\residualv}{{\cal R}}

\newcommand {\skeletonv}{{\cal S}}

\newcommand {\cachev}{{\cal C}}

\newcommand {\statev}{s}

\newcommand {\nodesv}{\Xi}

\newcommand {\pathv}{\pi}

\newcommand {\ssv}{\Pi}

\newcommand {\suffix}[2]{{#1}^{#2}}

\newcommand {\emptypath}{\bullet}

\newcommand {\blinenumv}{n}

\newcommand {\marked}{\bullet}

\newcommand {\unmarked}{\circ}

\newcommand {\markv}{m}

\newcommand {\node}[2]{{#1}^{#2}}

\newcommand {\nodev}{n}

\newcommand {\addchildsym}{\mbox{\it add-child}}

\newcommand {\addchild}[3]{\addchildsym({#1},{#2},{#3})}

\newcommand {\makearcsym}{\mbox{\it make-arc}}

\newcommand {\makearc}[3]{\makearcsym({#1},{#2},{#3})}

\newcommand {\removearcssym}{\mbox{\it remove-arcs}}

\newcommand {\removearcs}[2]{\removearcssym({#1},{#2})}

\newcommand {\unmarksym}{\mbox{\it unmark}}

\newcommand {\unmark}[2]{\unmarksym({#1},{#2})}

\newcommand {\marksym}{\mbox{\it mark}}

\renewcommand {\mark}[2]{\marksym({#1},{#2})}

\newcommand {\prunesym}{\mbox{\it prune}}

\newcommand {\prune}[2]{\prunesym({#1},{#2})}

\newcommand {\firstsym}{\mbox{\it first}}

\newcommand {\first}[1]{\firstsym({#1})}

\newcommand {\rawresid}{\mbox{residualizable?}}

\newcommand {\resid}[1]{\rawresid({#1})}

\newcommand {\widesym}{\theta}

\newcommand {\wide}[2]{\widesym({#1},{#2})}

\newcommand {\onexptup}[2]{\langle\, {#1}\,,\,{#2}\,\rangle}

\newcommand {\onassigntup}[2]{\langle\, {#1}\,,\,{#2}\,\rangle}

\newcommand {\onjumptup}[2]{\langle\, {#1}\,,\,{#2}\,\rangle}

\newcommand {\onblocktup}[2]{\langle\, {#1}\,,\,{#2}\,\rangle}

\newcommand {\lubsym}{\sqcup}

\newcommand {\glbsym}{\sqcap}

\newcommand {\biglubsym}{\bigsqcup}

\newcommand {\lub}[2]{{#1}\,\lubsym\,{#2}}

\newcommand {\glb}[2]{{#1}\,\glbsym\,{#2}}

\newcommand {\biglub}[3]{\biglubsym^{#1}_{#2}\,{#3}}

\newcommand {\state}[2]{({#1},{#2})}

\newcommand {\bline}[2]{[{#1}.{#2}]}

\newcommand {\blined}[1]{[{#1}]}

\newcommand {\rawtrans}{\rightarrow}

\newcommand {\rawtransbm}[1]{\rawtrans_{#1}}

\newcommand {\transrelg}[2]{{#1}\,\rawtrans\,{#2}}

\newcommand {\transrelgc}[2]{{#1}\,\rawtrans^*\,{#2}}

\newcommand {\ttrans}[4]{{#1} \vdash_{#2} 
                             {#3} \rawtrans {#4}}

\newcommand {\ttransc}[4]{{#1} \vdash_{#2} 
                              {#3} \rawtrans^* {#4}}

\newcommand {\itrans}[4]{{#1}\,{\vdash\!\!\!\vdash}_{#2} 
                             {#3} \rawtrans {#4}}

\newcommand {\itransc}[4]{{#1}\,{\vdash\!\!\!\vdash}_{#2} 
                              {#3} \rawtrans^* {#4}}

\newcommand {\trule}[2]{\begin{array}[b]{c} {#1} \\  \hline {#2} \end{array}}

\newcommand {\trulesp}{\;\;\;\;\;\;}

\newcommand {\ijudge}[4]{{#1}\, {\vdash\!\!\!\vdash}_{#2}\,{#3} \Rightarrow {#4}}

\newcommand {\ptjudge}[5]{{#2} \vdash^{#1}_{#3}\,{#4} \Rightarrow {#5}}

\newcommand {\tjudge}[4]{{#1} \vdash_{#2}\,{#3} \Rightarrow {#4}}

\newcommand {\vtjudge}[4]{\begin{array}{rl}
                         {#1} \vdash_{#2} & {#3} \\ 
                         & \Rightarrow {#4}
                         \end{array}}

\newcommand {\onlift}[2]{{#1} \Uparrow {#2}}

\newcommand {\derv}{\Delta}

\newcommand {\tdvrule}[2]{\begin{array}[b]{c} {#1} \\  {#2} \end{array}}

\newcommand {\tnlrule}[1]{\begin{array}[b]{c} \\  {#1} \end{array}}

\newcommand {\tnldrule}[2]{\begin{array}[b]{l} \\  {#1} \\  {#2} \end{array}}

\newcommand {\evalprog}[1]{\dsb{#1}}

\newcommand {\iorelsym}{\mbox{IO}}

\newcommand {\iorel}[4]{\iorelsym^{#1}_{#2}({#3},{#4})}

\newcommand {\runsym}{\mbox{Output}}

\newcommand {\run}[4]{\runsym^{#1}_{#2}({#3},{#4})}

\newcommand {\runs}[2]{\runsym({#1},{#2})}

\newcommand {\divv}{\Xi}

\newcommand {\divapp}[2]{{#1}({#2})}

\newcommand {\divapps}[1]{\divapp{\divv}{#1}}

\newcommand {\btjudgeexpr}[4]{{#1} \vdash^{bt}_{expr} \,{#2}\; [{#3} : {#4}]}

\newcommand {\btjudgeassign}[3]{{#1} \vdash^{bt}_{assign} \,{#2}\, [{#3}]}

\newcommand {\btjudgeassignl}[3]{{#1} \vdash^{bt}_{assigns} \,{#2}\, [{#3}]}

\newcommand {\btjudgejump}[3]{{#1} \vdash^{bt}_{jump} \,{#2}\, [{#3}]}

\newcommand {\btjudgeblock}[3]{{#1} \vdash^{bt}_{block} \,{#2}\, [{#3}]}

\newcommand {\btjudgeexprs}[3]{\btjudgeexpr{\divv}{#1}{#2}{#3}}

\newcommand {\btjudgeassigns}[2]{\btjudgeassign{\divv}{#1}{#2}}

\newcommand {\btjudgeassignls}[2]{\btjudgeassignl{\divv}{#1}{#2}}

\newcommand {\btjudgejumps}[2]{\btjudgejump{\divv}{#1}{#2}}

\newcommand {\btjudgeblocks}[2]{\btjudgeblock{\divv}{#1}{#2}}

\newcommand {\aexp}{expr}

\newcommand {\aassign}{assign}

\newcommand {\aassignl}{assigns}

\newcommand {\ajump}{jump}

\newcommand {\ablock}{block}

\newcommand {\specjudge}[4]{{#1} \vdash^{spec}_{{#2}} \,
                                  {#3} \Rightarrow {#4}}

\newcommand {\specjudgeexpr}[3]{{#1} \vdash^{spec}_{expr} \,
                                  {#2} \Rightarrow {#3}}

\newcommand {\specjudgeassign}[3]{{#1} \vdash^{spec}_{assign} \,
                                  {#2} \Rightarrow {#3}}

\newcommand {\specjudgeassignl}[3]{{#1} \vdash^{spec}_{assigns} \,
                                  {#2} \Rightarrow {#3}}

\newcommand {\specjudgejump}[3]{{#1} \vdash^{spec}_{jump} \,
                                  {#2} \Rightarrow {#3}}

\newcommand {\specjudgeblock}[3]{{#1} \vdash^{spec}_{block} \,
                                  {#2} \Rightarrow {#3}}

\newcommand {\storesta}{\sigma_s}

\newcommand {\varraysp}{4ex}

\newcommand {\ymset}[1]{\{...,\,{#1},\,...\}}

\newcommand {\myset}[2]{\{{#1},\,...,\,{#2}\}}

\newcommand {\myseq}[2]{{#1},\,\ldots,\,{#2}}

\newcommand {\mkset}[1]{\{{#1}\}}

\newcommand {\vmkset}[2]{\!\!\!\begin{array}[b]{l}
                          \{{#1}, \\ 
                          \;\;{#2}\}
                          \end{array}}

\newcommand {\powersetsym}{\wp}

\newcommand {\powerset}[1]{\powersetsym({#1})}

\newcommand {\fs}[2]{{#1}\!\rightarrow\!{#2}}

\newcommand {\pfs}[2]{{#1}\!\rightharpoonup\!{#2}}

\newcommand {\LFS}[2]{{#1}\:\rightarrow\:{#2}}

\newcommand {\union}[2]{{#1}\:\cup\:{#2}}

\newcommand {\intersect}[2]{{#1}\:\cap\:{#2}}

\newcommand {\difference}[2]{{#1}\,-\,{#2}}

\newcommand {\rtimeso}[2]{{#1}\times{#2}}

\newcommand {\mymid}{\;\;|\;\;}

\newcommand {\mf}{\bf}

\newcommand {\rfont}{\rm}

\newcommand {\texp}[2]{{#1}\,:\,{#2}}

\newcommand {\subfigureo}[1]{\mbox{\it {#1}}}

\newcommand {\introduce}[1]{\emph{#1}}

\newcommand {\petagfont}{\it}

\newcommand {\dynval}{{\petagfont D}}

\newcommand {\staval}{{\petagfont S}}

\newcommand {\btvalv}{t}

\newcommand {\onpeval}[2]{\langle {#1}\,,\,{#2} \rangle}

\newcommand {\specval}[2]{\langle {#1}\,,\,{#2} \rangle}

\newcommand {\onpevaldyn}[1]{\onpeval{\dynval}{#1}}

\newcommand {\onpevalsta}[1]{\onpeval{\staval}{#1}}

\newcommand {\onpevalv}{w}

\newcommand {\specvalv}{w}

\newcommand {\absvalv}{t}

\def\doframeit#1{\vbox{\hrule height\fboxrule
    \hbox{\vrule width\fboxrule \kern\fboxsep
      \vbox{\kern\fboxsep #1\kern\fboxsep }\kern\fboxsep \vrule width\fboxrule }\hrule height\fboxrule }}

\def\frameit{\smallskip \advance \linewidth by -7.5pt \setbox0=\vbox \bgroup
\strut \ignorespaces }

\def\endframeit{\ifhmode \par \nointerlineskip \fi \egroup
\doframeit{\box0}}

\newcommand {\figline}{\rule{\textwidth}{.5mm}}

\newcommand {\prg}[1]{{\tt {#1}}}

\newcommand {\lab}[1]{{\tt {#1}}}

\newcommand {\var}[1]{{\tt {#1}}}

\newcommand {\dprg}[1]{{\tt \underline{#1}}}

\newcommand {\exstepsym}{\longmapsto}

\newcommand {\exstepcsym}{\longmapsto^*}

\newcommand {\exstepisym}[1]{\stackrel{#1}{\exstepsym}}

\newcommand {\exstepcisym}[1]{\stackrel{#1}{\exstepsym}^*}

\newcommand {\exstep}[2]{{#1}\,\exstepsym\,{#2}}

\newcommand {\exstepc}[2]{{#1}\,\exstepsym^*\,{#2}}

\newcommand {\exstepi}[3]{{#2}\,\stackrel{#1}{\exstepsym}\,{#3}}

\newcommand {\exstepci}[3]{{#2}\,\stackrel{#1}{\exstepsym}^*\,{#3}}

\newcommand {\ieqsym}[1]{{=_{#1}}}

\newcommand {\ineqsym}[1]{{{\not=}_{#1}}}

\newcommand {\ieq}[3]{{#2}\,\ieqsym{#1}\,{#3}}

\newcommand {\ineq}[3]{{#2}\,\ineqsym{#1}\,{#3}}

\newcommand {\pjudge}[2]{\vdash^{#1}\:{#2}}

\newcommand {\cfgtup}[4]{({#1},{#2},{#3},{#4})}

\newcommand {\cfgv}{G}

\newcommand {\pdgv}{P}

\newcommand {\cfgnodesv}{N}

\newcommand {\cfgedgesv}{E}

\newcommand {\cfgiv}{\cfgv^{-1}}

\newcommand {\edgetup}[2]{({#1},{#2})}

\newcommand {\edgerel}[2]{{#1}\rightarrow{#2}}

\newcommand {\indexv}{i}

\newcommand {\cfgnodessym}{\mbox{\it nodes}}

\newcommand {\cfgnodes}[1]{\cfgnodessym[{#1}]}

\newcommand {\haltsym}{\mbox{\sf halt}}

\newcommand {\codemap}{\mbox{\it code}}

\newcommand {\firstmap}{\mbox{\it first}}

\newcommand {\dependssym}{\rightarrow}

\newcommand {\gdependssym}{\stackrel{{\it d}}{\dependssym}}

\newcommand {\gdependscsym}{\stackrel{{\it d}}{\dependssym^*}}

\newcommand {\cdependssym}{\stackrel{{\it cd}}{\dependssym}}

\newcommand {\ddependssym}{\stackrel{{\it dd}}{\dependssym}}

\newcommand {\odependssym}{\stackrel{{\it {\Omega}d}}{\dependssym}}

\newcommand {\depends}[2]{{#1}\,\dependssym\,{#2}}

\newcommand {\gdepends}[2]{{#1}\,\gdependssym\,{#2}}

\newcommand {\gdependsc}[2]{{#1}\,\gdependscsym\,{#2}}

\newcommand {\ddepends}[2]{{#1}\,\ddependssym\,{#2}}

\newcommand {\cdepends}[2]{{#1}\,\cdependssym\,{#2}}

\newcommand {\odepends}[2]{{#1}\,\odependssym\,{#2}}

\newcommand {\psuccsym}{\mbox{\it succ}}

\newcommand {\ppredsym}{\mbox{\it pred}}

\newcommand {\psucc}[1]{\psuccsym({#1})}

\newcommand {\ppred}[1]{\ppredsym({#1})}

\newcommand {\ipsucc}[2]{\psuccsym[{#1}]({#2})}

\newcommand {\ippred}[2]{\ppredsym[{#1}]({#2})}

\newcommand {\domsym}{\mbox{\it dom}}

\newcommand {\domi}[2]{\domsym({#1},{#2})}

\newcommand {\postdomsym}{\mbox{\it post-dom}}

\newcommand {\postdom}[2]{\postdomsym({#1},{#2})}

\newcommand {\vrefsym}{\mbox{\it ref}}

\newcommand {\vref}[1]{\vrefsym({#1})}

\newcommand {\vrefi}[2]{\vrefsym[{#1}]({#2})}

\newcommand {\vdefsym}{\mbox{\it def}}

\newcommand {\vdef}[1]{\vdefsym({#1})}

\newcommand {\vdefi}[2]{\vdefsym[{#1}]({#2})}

\newcommand {\cdsym}{\mbox{\it cd}}

\newcommand {\cd}[1]{\cdsym({#1})}

\newcommand {\bcsym}{\mbox{\it bc}}

\newcommand {\bc}[1]{\bcsym({#1})}

\newcommand {\scritup}[2]{({#1},{#2})}

\newcommand {\scriv}{C}

\newcommand {\scripair}[2]{({#1},{#2})}

\newcommand {\scripairv}[2]{\begin{array}{l@{}l}
                            ( & {#1},\\ 
                              & {#2})
                           \end{array}}

\newcommand {\scrionodes}[1]{{#1}.\onodessym}

\newcommand {\scriostates}[1]{{#1}.\ostatessym}

\newcommand {\relsym}[1]{R_{#1}}

\newcommand {\rel}[2]{\relsym{#1}({#2})}

\newcommand {\reli}[3]{\relsym{#1}[{#2}]({#3})}

\newcommand {\extranodes}{\Theta}

\newcommand {\genextrafrom}[1]{\extranodes({#1})}

\newcommand {\cdependscsym}{\stackrel{{\it cd}}{\dependssym^+}}

\newcommand {\cdependsc}[2]{{#1}\,\cdependscsym\,{#2}}

\newcommand {\gclosedset}[1]{\slicesetsym^d_{#1}}

\newcommand {\obligatorysym}{O}

\newcommand {\obligatoryset}[1]{\obligatorysym_{#1}}

\newcommand {\residualsym}{U}

\newcommand {\residualnodes}[1]{\residualsym_{#1}}

\newcommand {\scriodef}{\vdef{\scriostates{\scriv}}}

\newcommand {\slicesetsym}{S}

\newcommand {\sliceset}[1]{\slicesetsym_{#1}}

\newcommand {\refinesym}{\succ}

\newcommand {\refinesymi}[1]{\succ_{#1}}

\newcommand {\refine}[2]{{#1}\,\refinesym\,{#2}}

\newcommand {\refinec}[2]{{#1}\,\refinesym^*\,{#2}}

\newcommand {\refinei}[3]{{#2}\,\refinesym_{#1}\,{#3}}

\newcommand {\stuttercompresssym}{\leadsto}

\newcommand {\stuttercompresssymi}[1]{\stuttercompresssym_{#1}}

\newcommand {\stuttercompress}[2]{{#1}\,\stuttercompresssym\,{#2}}

\newcommand {\stuttercompressi}[3]{{#2}\,\stuttercompresssymi{#1}\,{#3}}

\newcommand {\propequivsym}{\equiv}

\newcommand {\propequivsymi}[1]{\propequivsym_{#1}}

\newcommand {\propequiv}[2]{{#1}\,\propequivsym\,{#2}}

\newcommand {\propequivi}[3]{{#2}\,\propequivsymi{#1}\,{#3}}

\newcommand {\stutterequivsym}{\approx}

\newcommand {\stutterequivsymi}[1]{\stutterequivsym_{#1}}

\newcommand {\stutterequiv}[2]{{#1}\,\stutterequivsym\,{#2}}

\newcommand {\stutterequivi}[3]{{#2}\,\stutterequivsymi{#1}\,{#3}}

\newcommand {\onodessym}{N}

\newcommand {\ostatessym}{S}

\newcommand {\branchsetsym}{B}

\newcommand {\branchset}[2]{\branchsetsym^{#1}_{#2}}

\newcommand {\projsym}{\downarrow}

\newcommand {\projpsym}[1]{\projsym[{#1}]}

\newcommand {\proj}[2]{\projsym[{#1}]({#2})}

\newcommand {\projvarsym}{\nu}

\newcommand {\projvar}[1]{\projvarsym({#1})}

\newcommand {\ropsym}{\mbox{\it rop}}

\newcommand {\restrictstore}[2]{{#1} \mid_{{#2}}}

\newcommand {\extractsym}{\mbox{\sf extract}}

\newcommand {\extract}[1]{\extractsym({#1})}

\newcommand {\cformv}{\psi}

\newcommand {\cpropv}{P}

\newcommand {\cpropsetv}{{\cal P}}

\newcommand {\cpropline}[2]{\bline{#1}{#2}}

\newcommand {\cpropnode}[1]{[{#1}]}

\newcommand {\cpropval}[3]{[{#1}{#2}{#3}]}

\newcommand {\ctrue}{\top}

\newcommand {\cfalse}{\perp}

\newcommand {\caxsym}{\mbox{AX}}

\newcommand {\cexsym}{\mbox{EX}}

\newcommand {\cagsym}{\mbox{AG}}

\newcommand {\cegsym}{\mbox{EG}}

\newcommand {\cafsym}{\mbox{AF}}

\newcommand {\cefsym}{\mbox{EF}}

\newcommand {\cesym}{\mbox{E}}

\newcommand {\casym}{\mbox{A}}

\newcommand {\cusym}{\until}

\newcommand {\cboxsym}{\Box}

\newcommand {\cdiasym}{\Diamond}

\newcommand {\cnextsym}{\circ}

\newcommand {\cnot}[1]{\neg{#1}}

\newcommand {\cand}[2]{{#1}\,\wedge\,{#2}}

\newcommand {\cor}[2]{{#1}\,\vee\,{#2}}

\newcommand {\cimplies}[2]{{#1}\,\Rightarrow\,{#2}}

\newcommand {\cax}[1]{\caxsym {#1}}

\newcommand {\cex}[1]{\cexsym {#1}}

\newcommand {\cag}[1]{\cagsym {#1}}

\newcommand {\ceg}[1]{\cegsym {#1}}

\newcommand {\caf}[1]{\cafsym {#1}}

\newcommand {\cef}[1]{\cefsym {#1}}

\newcommand {\cau}[2]{\casym [{#1}\,\cusym\,{#2}]}

\newcommand {\ceu}[2]{\cesym [{#1}\,\cusym\,{#2}]}

\newcommand {\cu}[2]{{#1}\,\cusym\,{#2}}

\newcommand {\cbox}[1]{\cboxsym{#1}}

\newcommand {\cdia}[1]{\cdiasym{#1}}

\newcommand {\cnext}[1]{\cnextsym{#1}}

\makeatother
\newenvironment{tex2html_wrap}{}{}
\newwrite\lthtmlwrite
\def\lthtmltypeout#1{{\let\protect\string\immediate\write\lthtmlwrite{#1}}}%
\newbox\sizebox
\begin{document}
\pagestyle{empty}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \begin{tabular}% latex2html id marker 1686
{ll}
{\tt Bandera.java} & Main program file \\ 
{\tt Bandera.class} & Main program class file \\ 
{\tt COPYING} & License notice \\ 
{\tt README.html} & Release information \\ 
{\tt filelist.txt} & Complete list of distribution files \\ 
{\tt ca} & McGill University Soot Framework \\ 
{\tt doc} & Documents, tutorials and examples (downloaded separately)\\ 
{\tt edu} & All programs reside here \\ 
\verb+java_cup+ & Necessary files for parsing \\ 
\end{tabular}
}

\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{figure}% latex2html id marker 1888
\begin{frameit}
\begin{enumerate}
\item Write an informal English statement of the property (we will
refer to this as the \emph{requirement}).
\item Examine the requirement to see which particular source code features
(control points, variable values) are explicitly mentioned or alluded to
in the requirement.
\item Use Bandera's Java-doc-based \emph{predicate definition
language} to declare the identified source code features to be
\emph{observable} to Bandera's property specification tool.
These observables form the primitive propositions that can appear
in the temporal property that we will ask Bandera to check.
\item Use the BUI's property manage to construct the temporal property
the formalizes the given requirement.
\end{enumerate}

\end{frameit}
\label{fig:spec-method}
\end{figure}
}

\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{subsection}
\stepcounter{paragraph}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsection}
\stepcounter{paragraph}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}

\end{document}
