<commit_before>\documentclass[11pt]{article}

\usepackage{a4wide}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{proof}
\usepackage{amsmath}
\usepackage{listings}
\usepackage{graphicx}
\usepackage{cite}

\newcommand{\jStar}{{\sf jStar}}

\newcommand{\psto}{\mapsto}
\newcommand{\sem}[1]{[\!|#1 |\!] }
\newcommand{\rearr}{\mathsf{rearr}}
\newcommand{\FNames}{\mathit{FNames}}
\newcommand{\MNames}{\mathit{MNames}}
\newcommand{\CNames}{\mathit{CNames}}
\newcommand{\TNames}{\mathit{TNames}}
\newcommand{\NodeLL}{\mathit{NodeLL}}
\newcommand{\val}{\mathit{val}}
\newcommand{\intT}{\mathit{int}}
\newcommand{\next}{\mathit{next}}
\newcommand{\returnStm}{{\sf return}}
\newcommand{\invoke}{{\sf invoke}}
\newcommand{\sinvoke}{{\sf sinvoke}}
\newcommand{\jsr}{{\sf jsr}}
\newcommand{\init}{{\sf init}}
\newcommand{\emp}{{\sf emp}}
\newcommand{\TT}{{\sf true}}
\newcommand{\FF}{{\sf false}}
\newcommand{\void}{\mathit{void}}
\newcommand{\spec}{{\sf spec}}
\newcommand{\sspec}{{\sf sspec}}
\newcommand{\new}{{\sf new}}
\newcommand{\ra}{\longrightarrow}
\newcommand{\pto}{\mapsto}
\newcommand{\ret}{\mathit{ret}}
\newcommand{\refe}[4]{#1.\langle #2{:} \; #3 \ #4 \rangle}
\newcommand{\signature}[3]{\langle #1{:} \; #2 \ #3 \rangle}
\newcommand{\Sig}{\mathit{Sig}}
\newcommand{\Specs}{\mathit{Specs}}
\newcommand{\Heaps}{\mathit{Heaps}}
\newcommand{\Val}{\mathit{Val}}
\newcommand{\Powerset}{{\cal P}}
\newcommand{\lseg}{{\sf lseg}} 
\newcommand{\nil}{{\sf nil}} 
\newcommand{\junk}{{\sf junk}} 
\newcommand{\Var}{\mathit{Var}} 

%\newcommand{\ex}[1]{\mathord{\_\!\_#1}}
\newcommand{\ex}[1]{\mathord{\hat{#1}}}

% Definition for specifications
\newcommand{\define}{\mathbf{define} \ }
\newcommand{\content}[1]{\{\text{content=} \, #1 \}}
\newcommand{\true}{\mathbf{true}}
\newcommand{\symbolicheap}[2]{#1 \mid #2}
\newcommand{\this}{\mathbf{this}}
\newcommand{\return}{\mathbf{return}}
\newcommand{\parameter}{\mathbf{param0}}
\newcommand{\contentOld}[2]{\{\text{content=} \, #1; \  \text{oldcon=} \, #2 \}}
\newcommand{\type}{\mbox{type}}
\newcommand{\Visitor}{\mathit{Visitor}}
\newcommand{\Ast}{\mathit{Ast}}
\newcommand{\Visited}{\mathit{Visited}}
\newcommand{\context}[1]{\{\text{context=} \, #1 \}}
\newcommand{\contentCA}[3]{\{\text{content=} \, #1; \  \text{context=} \, #2; \ \text{ast=} \, #3 \}}
\newcommand{\export}{\mathbf{export}}
\newcommand{\const}{\mathit{const}}
\newcommand{\plus}{\mathit{plus}}
\newcommand{\lft}{\mathit{left}}
\newcommand{\rgt}{\mathit{right}}
\newcommand{\summ}{\mathit{sum}}
\newcommand{\union}{\mathit{union}}
\newcommand{\amount}{\mathit{amount}}
\newcommand{\rz}{\mathit{rz}}
\newcommand{\isZero}{\mathit{isZero}}
\newcommand{\isChanged}{\mathit{isChanged}}
\newcommand{\newl}{\mathit{newl}}
\newcommand{\false}{\mathbf{false}}
\newcommand{\zero}{\mathbf{zero}}
\newcommand{\DBPool}{\mathit{D\!B\!Pool}}
\newcommand{\DBConnection}{\mathit{D\!B\!Connection}}
\newcommand{\connection}[1]{\{\text{connection=} \, #1 \}}
\newcommand{\sql}{\mathit{sql}}
\newcommand{\url}{\mathit{url}}
\newcommand{\user}{\mathit{user}}
\newcommand{\password}{\mathit{password}}
\newcommand{\conns}{\mathit{conns}}
\newcommand{\LinkedList}{\mathit{LinkedList}}
\newcommand{\DBSet}{\mathit{D\!B\!Set}}
\newcommand{\setof}{\mathit{setof}}
\newcommand{\handle}[2]{\{\text{handle=} \, #1; \  \text{type=} \, #2 \}}
\newcommand{\ResourceFactory}{\mathit{ResourceFactory}}
\newcommand{\Resource}{\mathit{Resource}}
\newcommand{\factory}[2]{\{\text{factory=} \, #1; \  \text{type=} \, #2 \}}
\newcommand{\ResPool}{\mathit{ResPool}}
\newcommand{\resources}{\mathit{resources}}
\newcommand{\rf}{\mathit{rf}}
%\newcommand{\ResourceFactory}{\mathit{ResourceFactory}}
\newcommand{\IterRes}{\mathit{IterRes}}
\newcommand{\Subject}{\mathit{Subject}}
\newcommand{\ObsSet}{\mathit{ObsSet}}
\newcommand{\SubjectObs}{\mathit{SubjectObs}}
\newcommand{\observers}{\mathit{observers}}
\newcommand{\listIT}{\mathit{list}}
\newcommand{\SubjectData}{\mathit{SubjectData}}
\newcommand{\SubjectInternal}{\mathit{SubjectInternal}}
\newcommand{\obsVals}[2]{\{\text{obs=} \, #1; \  \text{vals=} \, #2 \}}
\newcommand{\obs}[1]{\{\text{obs=} \, #1 \}}
\newcommand{\vals}[1]{\{\text{vals=} \, #1 \}}
\newcommand{\valsSubject}[2]{\{\text{vals=} \, #1; \  \text{subject=} \, #2 \}}
\newcommand{\dollar}{\mbox{\$}}
\newcommand{\Observer}{\mathit{Observer}}
\newcommand{\add}{\mathit{add}}
\newcommand{\emptyP}{\mathit{empty}}




\newtheorem{thm}{Theorem}
\newtheorem{defn}{Definition}
\newtheorem{lemma}{Lemma}
\newtheorem{example}{Example}
\newtheorem{notation}{Notation}

\newcommand{\field}[3]{\textrm{#1}.\textrm{#2} \mapsto \textrm{#3}}




\lstset{language=Java,framesep=5pt,columns=fullflexible,basicstyle=\small,
 stringstyle=\ttfamily,
 showstringspaces=true,
 mathescape=true,
 deletekeywords={const},
 morekeywords={ensures,requires,inherit,andalso,define,as,dynamic,export,rule,rewrite},
 literate=
           {@}{$\$$}1
           {/\\}{$\land\ $}2
           {|-}{$\vdash\ $}2
           {|->}{$\mapsto\ $}2
           {@this:}{\textbf{this}}4
           {inherited\ with\ type}{\textbf{inherited with type}}4
           {@parameter0:}{\textbf{param0}}6
           {@parameter1:}{\textbf{param1}}6
           {@parameter2:}{\textbf{param2}}6
           {@return:}{\textbf{return}}6
           {-*}{$\mathbin{-\!*\,}$}6
,}
\def\J{\lstinline}
\newcommand{\JS}[1]{$\mathit{#1}$}


%\renewcommand{\jStar}{\raisebox{-.2em}{\includegraphics[height=1em]{logo.pdf}}}
\newcommand{\jStarlogo}{\raisebox{-.2em}{\includegraphics[height=1em]{logo.pdf}}}
%\newcommand{\jStarPlain}{jStar}
\newcommand{\jStarPlain}{\jStar}
\newcommand{\jStarQED}{\hfill \jStarlogo}


\newcommand{\mattcomment}[1]{
\begin{center}
\fbox{
\begin{minipage}{3.0in}
{\bf Matt's comment:} {\it #1}
\end{minipage}
}
\end{center}
}

\newcommand{\dinocomment}[1]{
\begin{center}
\fbox{
\begin{minipage}{3.0in}
{\bf Dino's comment:} {\it #1}
\end{minipage}
}
\end{center}
}

\begin{document}
\title{\bf How to Verify Java Program with \jStar: a  Tutorial \\[2ex]
\jStarlogo \qquad  \jStarlogo  \qquad \jStarlogo }

\author{{\sc <NAME>} \\
Queen Mary University of London, UK \\ 
{\tt <EMAIL>} 
\and 
{\sc <NAME>} \\
University of Cambridge, UK \\ 
{\tt <EMAIL>}}

\maketitle

\begin{abstract}
  In this tutorial we describe how to use the tool \jStar \ to verify
  Java programs. The document is meant to be an informal and basic introduction to
  \jStar \ and many of the key notions behind this tool. 
  
  This is an evolving document, we hope to improve it along with the improvement of the tool.
\end{abstract}

\section{Introduction}
\jStar~\cite{jstar} is an automatic verification tool based on
separation logic aiming at object-oriented programs written in
Java. \jStar \ integrates theorem proving and abstract interpretation
techniques. The user is required to provide specifications of pre/post
conditions whereas loop invariants are synthesized  automatically,
minimizing the burden of verification.  \jStar \ uses succinct
separation logic specification therefore pre/post specs in this language are often 
simpler than what would be in other formalisms.

\jStar \ aims at those applications which present challenging problems
for the other verification tools for object-oriented
programs~\cite{jml,jmltool, spec, DHHR05,DLR06, chin08}.
Example of key challenges in verifying object-oriented programs are:
\begin{description}
\item [Properties across multiple objects] where one needs to be able
  to express properties about several interacting objects from many<commit_msg>Mike is now an author<commit_after>\documentclass[11pt]{article}

\usepackage{a4wide}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{proof}
\usepackage{amsmath}
\usepackage{listings}
\usepackage{graphicx}
\usepackage{cite}

\newcommand{\jStar}{{\sf jStar}}

\newcommand{\psto}{\mapsto}
\newcommand{\sem}[1]{[\!|#1 |\!] }
\newcommand{\rearr}{\mathsf{rearr}}
\newcommand{\FNames}{\mathit{FNames}}
\newcommand{\MNames}{\mathit{MNames}}
\newcommand{\CNames}{\mathit{CNames}}
\newcommand{\TNames}{\mathit{TNames}}
\newcommand{\NodeLL}{\mathit{NodeLL}}
\newcommand{\val}{\mathit{val}}
\newcommand{\intT}{\mathit{int}}
\newcommand{\next}{\mathit{next}}
\newcommand{\returnStm}{{\sf return}}
\newcommand{\invoke}{{\sf invoke}}
\newcommand{\sinvoke}{{\sf sinvoke}}
\newcommand{\jsr}{{\sf jsr}}
\newcommand{\init}{{\sf init}}
\newcommand{\emp}{{\sf emp}}
\newcommand{\TT}{{\sf true}}
\newcommand{\FF}{{\sf false}}
\newcommand{\void}{\mathit{void}}
\newcommand{\spec}{{\sf spec}}
\newcommand{\sspec}{{\sf sspec}}
\newcommand{\new}{{\sf new}}
\newcommand{\ra}{\longrightarrow}
\newcommand{\pto}{\mapsto}
\newcommand{\ret}{\mathit{ret}}
\newcommand{\refe}[4]{#1.\langle #2{:} \; #3 \ #4 \rangle}
\newcommand{\signature}[3]{\langle #1{:} \; #2 \ #3 \rangle}
\newcommand{\Sig}{\mathit{Sig}}
\newcommand{\Specs}{\mathit{Specs}}
\newcommand{\Heaps}{\mathit{Heaps}}
\newcommand{\Val}{\mathit{Val}}
\newcommand{\Powerset}{{\cal P}}
\newcommand{\lseg}{{\sf lseg}} 
\newcommand{\nil}{{\sf nil}} 
\newcommand{\junk}{{\sf junk}} 
\newcommand{\Var}{\mathit{Var}} 

%\newcommand{\ex}[1]{\mathord{\_\!\_#1}}
\newcommand{\ex}[1]{\mathord{\hat{#1}}}

% Definition for specifications
\newcommand{\define}{\mathbf{define} \ }
\newcommand{\content}[1]{\{\text{content=} \, #1 \}}
\newcommand{\true}{\mathbf{true}}
\newcommand{\symbolicheap}[2]{#1 \mid #2}
\newcommand{\this}{\mathbf{this}}
\newcommand{\return}{\mathbf{return}}
\newcommand{\parameter}{\mathbf{param0}}
\newcommand{\contentOld}[2]{\{\text{content=} \, #1; \  \text{oldcon=} \, #2 \}}
\newcommand{\type}{\mbox{type}}
\newcommand{\Visitor}{\mathit{Visitor}}
\newcommand{\Ast}{\mathit{Ast}}
\newcommand{\Visited}{\mathit{Visited}}
\newcommand{\context}[1]{\{\text{context=} \, #1 \}}
\newcommand{\contentCA}[3]{\{\text{content=} \, #1; \  \text{context=} \, #2; \ \text{ast=} \, #3 \}}
\newcommand{\export}{\mathbf{export}}
\newcommand{\const}{\mathit{const}}
\newcommand{\plus}{\mathit{plus}}
\newcommand{\lft}{\mathit{left}}
\newcommand{\rgt}{\mathit{right}}
\newcommand{\summ}{\mathit{sum}}
\newcommand{\union}{\mathit{union}}
\newcommand{\amount}{\mathit{amount}}
\newcommand{\rz}{\mathit{rz}}
\newcommand{\isZero}{\mathit{isZero}}
\newcommand{\isChanged}{\mathit{isChanged}}
\newcommand{\newl}{\mathit{newl}}
\newcommand{\false}{\mathbf{false}}
\newcommand{\zero}{\mathbf{zero}}
\newcommand{\DBPool}{\mathit{D\!B\!Pool}}
\newcommand{\DBConnection}{\mathit{D\!B\!Connection}}
\newcommand{\connection}[1]{\{\text{connection=} \, #1 \}}
\newcommand{\sql}{\mathit{sql}}
\newcommand{\url}{\mathit{url}}
\newcommand{\user}{\mathit{user}}
\newcommand{\password}{\mathit{password}}
\newcommand{\conns}{\mathit{conns}}
\newcommand{\LinkedList}{\mathit{LinkedList}}
\newcommand{\DBSet}{\mathit{D\!B\!Set}}
\newcommand{\setof}{\mathit{setof}}
\newcommand{\handle}[2]{\{\text{handle=} \, #1; \  \text{type=} \, #2 \}}
\newcommand{\ResourceFactory}{\mathit{ResourceFactory}}
\newcommand{\Resource}{\mathit{Resource}}
\newcommand{\factory}[2]{\{\text{factory=} \, #1; \  \text{type=} \, #2 \}}
\newcommand{\ResPool}{\mathit{ResPool}}
\newcommand{\resources}{\mathit{resources}}
\newcommand{\rf}{\mathit{rf}}
%\newcommand{\ResourceFactory}{\mathit{ResourceFactory}}
\newcommand{\IterRes}{\mathit{IterRes}}
\newcommand{\Subject}{\mathit{Subject}}
\newcommand{\ObsSet}{\mathit{ObsSet}}
\newcommand{\SubjectObs}{\mathit{SubjectObs}}
\newcommand{\observers}{\mathit{observers}}
\newcommand{\listIT}{\mathit{list}}
\newcommand{\SubjectData}{\mathit{SubjectData}}
\newcommand{\SubjectInternal}{\mathit{SubjectInternal}}
\newcommand{\obsVals}[2]{\{\text{obs=} \, #1; \  \text{vals=} \, #2 \}}
\newcommand{\obs}[1]{\{\text{obs=} \, #1 \}}
\newcommand{\vals}[1]{\{\text{vals=} \, #1 \}}
\newcommand{\valsSubject}[2]{\{\text{vals=} \, #1; \  \text{subject=} \, #2 \}}
\newcommand{\dollar}{\mbox{\$}}
\newcommand{\Observer}{\mathit{Observer}}
\newcommand{\add}{\mathit{add}}
\newcommand{\emptyP}{\mathit{empty}}




\newtheorem{thm}{Theorem}
\newtheorem{defn}{Definition}
\newtheorem{lemma}{Lemma}
\newtheorem{example}{Example}
\newtheorem{notation}{Notation}

\newcommand{\field}[3]{\textrm{#1}.\textrm{#2} \mapsto \textrm{#3}}




\lstset{language=Java,framesep=5pt,columns=fullflexible,basicstyle=\small,
 stringstyle=\ttfamily,
 showstringspaces=true,
 mathescape=true,
 deletekeywords={const},
 morekeywords={ensures,requires,inherit,andalso,define,as,dynamic,export,rule,rewrite},
 literate=
           {@}{$\$$}1
           {/\\}{$\land\ $}2
           {|-}{$\vdash\ $}2
           {|->}{$\mapsto\ $}2
           {@this:}{\textbf{this}}4
           {inherited\ with\ type}{\textbf{inherited with type}}4
           {@parameter0:}{\textbf{param0}}6
           {@parameter1:}{\textbf{param1}}6
           {@parameter2:}{\textbf{param2}}6
           {@return:}{\textbf{return}}6
           {-*}{$\mathbin{-\!*\,}$}6
,}
\def\J{\lstinline}
\newcommand{\JS}[1]{$\mathit{#1}$}


%\renewcommand{\jStar}{\raisebox{-.2em}{\includegraphics[height=1em]{logo.pdf}}}
\newcommand{\jStarlogo}{\raisebox{-.2em}{\includegraphics[height=1em]{logo.pdf}}}
%\newcommand{\jStarPlain}{jStar}
\newcommand{\jStarPlain}{\jStar}
\newcommand{\jStarQED}{\hfill \jStarlogo}


\newcommand{\mattcomment}[1]{
\begin{center}
\fbox{
\begin{minipage}{3.0in}
{\bf Matt's comment:} {\it #1}
\end{minipage}
}
\end{center}
}

\newcommand{\dinocomment}[1]{
\begin{center}
\fbox{
\begin{minipage}{3.0in}
{\bf Dino's comment:} {\it #1}
\end{minipage}
}
\end{center}
}

\begin{document}
\title{\bf How to Verify Java Program with \jStar: a  Tutorial \\[2ex]
\jStarlogo \qquad  \jStarlogo  \qquad \jStarlogo }

\author{{\sc <NAME>} \\
Queen Mary University of London, UK \\ 
{\tt <EMAIL>} 
\and 
{\sc <NAME>} \\
University of Cambridge, UK \\ 
{\tt <EMAIL>}
\and
{\sc <NAME>} \\
University of Cambridge, UK \\ 
{\tt <EMAIL>}}

\maketitle

\begin{abstract}
  In this tutorial we describe how to use the tool \jStar \ to verify
  Java programs. The document is meant to be an informal and basic introduction to
  \jStar \ and many of the key notions behind this tool. 
  
  This is an evolving document, we hope to improve it along with the improvement of the tool.
\end{abstract}

\section{Introduction}
\jStar~\cite{jstar} is an automatic verification tool based on
separation logic aiming at object-oriented programs written in
Java. \jStar \ integrates theorem proving and abstract interpretation
techniques. The user is required to provide specifications of pre/post
conditions whereas loop invariants are synthesized  automatically,
minimizing the burden of verification.  \jStar \ uses succinct
separation logic specification therefore pre/post specs in this language are often 
simpler than what would be in other formalisms.

\jStar \ aims at those applications which present challenging problems
for the other verification tools for object-oriented
programs~\cite{jml,jmltool, spec, DHHR05,DLR06, chin08}.
Example of key challenges in verifying object-oriented programs are:
\begin{description}
\item [Properties across multiple objects] where one needs to be able
  to express properties about several interacting objects from many
{'fraction_non_alphanumeric': 0.21813386086383119, 'fraction_numerical': 0.012396966699637323, 'mean_word_length': 5.135113268608414, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2067646', 'n_tokens_mistral': 5086, 'n_tokens_neox': 4849, 'n_words': 894}