\documentclass[final,nocolorBG,a4,marieke,nototal,pdf,slideColor]{prosper}
\addtolength{\textheight}{-1cm}

\usepackage{pstricks,pst-node,pst-text,pst-3d}
\usepackage{amsmath}
\usepackage{alltt}
\usepackage{epsfig}

\usepackage{colordvi}
\usepackage{proof}
\usepackage{epsf}
\usepackage{amssymb}


\slideCaption{spopS}
\title{\Blue{Specification language and WP calculus for Java Bytecode. } }


\author{

joint work in progress\\
 Mariela Pavlova, Lilian Burdy \\

 
INRIA Sophia-Antipolis\\
}

\begin{document}
\maketitle

\begin{slide}{Motivation}

\begin{itemize}

\item Proof Carrying ByteCode
    \begin{itemize}
           \item Proof obligations. 
           \item What is the language in which properties will be expressed ? 
    \end{itemize}
\end{itemize}
\end{slide}

\begin{slide}{Overview}
  \begin{tabular} {|c|c|}
\hline
    JAVA source File & Java bytecode \\
\hline \\
    JML specification & Specification language for bytecode \\
\hline   
\end{tabular}
\end{slide}


\begin{slide}{Overview}
  \begin{itemize}
     \item Specifying java source files with the Java Modeling Language (JML).Examples       
     \item Translation of JML into specification language for Java bytecode. 
     \item Generation of  class files containing specification information.
     \item WP for Java bytecode   
     \item Example
     \item Conclusion 
\end{itemize}
 


\end{slide}

\begin{slide}[Dissolve]{Java Modeling Language  }
   A specification language by which one can declare : 
   \begin{itemize}
       \item method specification- preconditions, postconditions,  loop invariants , frame conditions  can be  specified for a method.
       \item  class specification- class invariants and history constraints can be specified for a class.
   \end{itemize}
\end{slide}

\begin{slide}[Dissolve]{Java Modeling Language.  } 
   \begin{itemize}
     \item Java expressions without side effects.
      \item JML model variables - in the JML specification variables that are discarded by the compiler can be used.
        These fields are used  for specification purposes only.

         \item specific JML  constants - $\backslash$\texttt{result}, $\backslash$\texttt{old} , etc. 
   \end{itemize}
\end{slide}

\begin{slide}[Dissolve]{Java Modeling Language.Example  }
                     $ \phantom{...}$ \Red{ \texttt{ //@requires i != 0; } } \\
                     $ \phantom{...}$ \Red{\texttt{ //@ensures}  $\tt{\backslash}$\texttt{result == 1/i; } } \\
                     $ \phantom{...}$ \Red{\texttt{ //@exsures ArithemticException}  \texttt{ i==0; } } \\
                     $ \phantom{...}$ \texttt{ int  m(int i )  \{ }\\
                     $ \phantom{...} \phantom{...} $ \texttt{ int j;}\\
                     $ \phantom{...} \phantom{...} $ \texttt{ j = 1/i;}\\
                     $ \phantom{...} \phantom{...} $ \texttt{ return j;}\\
                     $ \phantom{...}$ \texttt{ \} }\\  
\end{slide}


\begin{slide}[Dissolve]{ Translation of JML }
    \begin{itemize}
       \item translation that should fit to bytecode - use of the same names, for example
       \item Integration of the specification in the class file
        \item The new class file format must respect the VM specification and not create problems at execution time.
         \item efficient coding - not too rich in order not to increase considerably the class file 
    \end{itemize}\
\end{slide}

\begin{slide}[Dissolve]{ Translation of JML }
\begin{itemize}
       \item for every JML unit - precondition, postcondition there will be a new attribute defined
       \item attribute\_info \{ \\
            $\phantom{................}$   u2 attribute$\_$name$\_$index;\\
            $\phantom{................}$   u4 attribute$\_$length;\\
            $\phantom{................}$   u1 info[attribute$\_$length];\\
     \} 
  \end{itemize}
\end{slide}



\begin{slide}[Dissolve]{ Generation of new class file format }
\begin{tabular}{lll}
    ClassFile  &  & \\
\quad  \begin{tabular}{ll}
      
         u2 constant\_pool\_count; & \\
         cp\_info constant\_pool[constant\_pool\_count-1];& \\
         \vdots & \\
          methodinfo[]  & \\
         \vdots & \\
          u2 attributes\_count;&\\
          attribute\_info attributes[attributes\_count];&\\
      
\end{tabular}
\end{tabular}

\end{slide}





\begin{slide}[Dissolve]{Translation of JML. Extension of the  constant pool(\texttt{CP}) }
   \begin{itemize}
      \item Java virtual machine instructions do not rely on the runtime layout of classes, interfaces, class instances, or arrays. Instead, instructions refer to symbolic 
        infomation in the class \texttt{CP}.  
      \item Motivation \\
        Specification may involve fields that are not  present in the class \texttt{CP}: \\
        - java fields that are not dereferenced in the code - so there is no index for them in the constant pool \\
      \item Attribute - \texttt{ConstantPool\_attribute }, that contains references that are added every time that they are not in the original constant pool, but are needed for the specification        
   \end{itemize}
\end{slide}


\begin{slide}[Dissolve]{Translation of JML.\texttt{ Model variables} }
   \begin{itemize}
      \item  Completely ignored by Java compilers. Define \texttt{Model\_Field\_Attribute} 
       \item For every model variable in class \texttt{C}, an attribute added to the \texttt{attribute} array for the class file  for \texttt{C}
        \item If a \texttt{model variable} is dereferenced at least once, add new index into the   \texttt{ConstantPool\_attribute }
   \end{itemize}
\end{slide}


\begin{slide}[Dissolve]{Translation of JML. Method specification translation }
   \begin{itemize}
        \item Precondition,   Postcondition,  Loop Invariant, Assertions    translated as new attributes for the \texttt{ method$\_$info} attribute
        \item Translation of any JML constant \texttt{c}- by its corresponding $code$(\texttt{c})
        \item Translation of fields - by their corresponding index in the constant pool(the original or in its extension)
        \item Translation of local variables - by their indexes in the local variable array 
   \end{itemize}
\end{slide}


\begin{slide}[Dissolve]{ Translation of JML }
\begin{tabular}{lll}
    ClassFile  &  & \\
\quad  \begin{tabular}{ll}
      
         u2 constant\_pool\_count; & \\
         cp\_info constant\_pool[constant\_pool\_count-1];& \\
         \vdots & \\
          methodinfo  & \\
         \quad \begin{tabular} {l} 
                      code\_attribute \\
                      \Red{Requires\_Attribute} \\
                      \Red{Ensures\_Attribute }\\
                    \end{tabular} \\
         \vdots & \\
         \Red{Class\_Invariant\_Attribute}; & \\
          \Red{Constant\_Pool\_Attribute}; & \\
\end{tabular}
\end{tabular}
\end{slide}


\begin{slide}[Dissolve]{Translation of JML.Example }
Translation of method postcondition in bytecode format : \\
 JMLEnsures\_attribute \{ \\ 
            $\phantom{............}$ u2 attribute\_name\_index;\\ 
            $\phantom{............}$ u4 attribute\_length;\\ 
            $\phantom{............}$ un attribute\_formula;\\ 
      \}   
\end{slide}

\begin{slide}[Dissolve]{Example  }
                     $ \phantom{...}$ \Red{ \texttt{ //@requires i != 0; } } \\
                     $ \phantom{...}$ \Red{\texttt{ //@ensures}  $\tt{\backslash}$\texttt{result == 1/i; } } \\
                     $ \phantom{...}$ \texttt{ int  m(int i )  \{ }\\
                     $ \phantom{...} \phantom{...} $ \texttt{ int j;}\\
                     $ \phantom{...} \phantom{...} $ \texttt{ j = 1/i;}\\
                     $ \phantom{...} \phantom{...} $ \texttt{ return j;}\\
                     $ \phantom{...}$ \texttt{ \} }\\  
\end{slide}

\begin{slide}[Dissolve]{Example of translation of the postcondition predicate }
  For method \texttt{m} postcondition attribute will look be:  \\
   JMLEnsures\_attribute \{ \\ 
         \phantom{............} u2 attribute\_name\_index;\\ 
          \phantom{............} u4 attribute\_length;\\ 
          \phantom{............} un attribute\_formula =  $code(\backslash \tt{result}) \ulcorner == \urcorner  \ulcorner  1 \ div  \ local(1) \urcorner  $ \\
      \} 


%The value of the entry \textbf{attribute\_formula} for the attribute \texttt{ JMLEnsures\_attribute} for the \texttt{method\_info} entry for the method \texttt{m} will be  : \\
%$code(\backslash \tt{result}) \ulcorner == \urcorner  \ulcorner  1 \ div  \ local(1) \urcorner  $ \\
%where  $\ulcorner . \urcorner $ is a translation function from JML into the bytecode specification language 
 \end{slide}


\begin{slide}[Dissolve]{Example of translation of the postcondition predicate }
For method \texttt{m} precondition attribute will look be: \\
    JMLEnsures\_attribute \{ \\ 
          \phantom{............} u2 attribute\_name\_index;\\ 
          \phantom{............} u4 attribute\_length;\\ 
          \phantom{............} un attribute\_formula =  $\ulcorner local(1) != 1 \urcorner $ \\
       \} \\  

\end{slide}


\begin{slide}[Dissolve]{Translation of JML.Class specification }
 \begin{itemize}
        \item Translation of class specification
              \begin{itemize}
                   \item Class invariant, History constraints  : new attributes defined for the \texttt{class$\_$info} data structure
                    \item   JMLClassInvariant\_attribute \{ \\ 
                              \phantom{............} u2 attribute\_name\_index;\\ 
                              \phantom{............} u4 attribute\_length;\\ 
                              \phantom{............} un attribute\_formula;\\ 
         \} \\ 
        \end{itemize}
   \end{itemize}
\end{slide}

\begin{slide}[Dissolve]{Translation of JML. Limitations }
  \begin{itemize}
     \item Additional information that is not a must in the Java Virtual machine specification is required:  \texttt{Linenumbertable} , \texttt{Local\_variable\_table}
           attributes might not be generated by certain Java language compilers. 
     
  \end{itemize}
\end{slide}

\begin{slide}[Dissolve]{Weakest precondition for Java bytecode. Definitions}
   \begin{itemize}
         \item defined over the execution graph of a bytecode
         \item Definition of a bytecode \texttt{block} : a subsequence of a bytecode \textit{B}  that
         \begin{itemize}
                 \item starts either with the initial instruction of \textit{B}, either with a target of a jump instruction and
                 \item terminates either  with a jump instruction or the last instruction of the bytecode \textit{B}.
        \end{itemize}
  \end{itemize}
\end{slide}


\begin{slide}[Dissolve]{Weakest precondition for Java bytecode}
  \begin{itemize}
    \item  \texttt{wp} : Java$\_$instruction $\rightarrow$ Predicate  $\rightarrow$ (Exception\_name $\rightarrow$ Predicate ) $\rightarrow$ Predicate \\
    \item  
         \textit{ Definition} : \\
         \texttt{wp}(\textrm{b} , $psi^n$, $psi^e$) is a predicate that must hold in those initial states of the  execution of the bytecode block \textrm{b} for which
      \begin{itemize}
            \item      it terminates in a state that satisfies the predicate $psi^n$ if it terminates normally or
            \item      it terminates by throwing an exception of type $Exception\_Name$  in a state that satisfies $psi^e(Exception\_Name)$ 

      \end{itemize}
\end{itemize}
\end{slide}   



\begin{slide}[Dissolve]{ WP for Java  bytecode. Example}
   ByteCode for the method \texttt{m} :\\   



\begin{tabular}{p{7cm}p{5cm}} 
{\small
\begin{verbatim}
//@ requires i != 0;
//@ ensures \result == 1/i;
int m(int i) {
   int j;
   j = 1/i;
   return j;
}
\end{verbatim}
}

&

\begin{verbatim}
0  iconst_1
1  iload_1
2  idiv
3  istore_2
4  iload_2
5  ireturn
\end{verbatim}
\end{tabular} 


\end{slide}


\begin{slide}[Dissolve]{WP for Java  bytecode. Example } 
Some namings : \\
  \texttt{S} - the stack \\
  \texttt{t} - the stack top \\
  \texttt{head} - a function that returns the subbytecode of a bytecode except for the last instruction  \\
\end{slide}

\overlays{5}{\begin{slide}[Dissolve]{WP for Java  bytecode. Example }  
Calculating the Weakest precondition for the method \texttt{m} over its bytecode: \\
\begin{itemstep} 
 \item  $\tt{wp}(\tt{B}, postcondition(m) ) = $ \\
 \item  $\tt{wp}(\tt{B}, code(\backslash \tt{result}) \ulcorner == \urcorner  \ulcorner 1 \ div \ local(1) \urcorner )  $ \\
 \item  $\tt{wp}(\tt{head(B)}, \tt{wp}(ireturn, code(\backslash \tt{result}) \ulcorner == \urcorner  \ulcorner 1 \ div \ local(1) \urcorner) )  $\\
 \item  $\tt{wp}(\tt{head(B)}, code(\backslash \tt{result}) \ulcorner == \urcorner  \ulcorner 1 \ div \ local(1) \urcorner[code(\backslash \tt{result}]) \leftarrow S(t) ]  $\\
 \item  $\tt{wp}( \tt{ head(head(B))}, wp ( \tt{ iload\_1 }, code(\backslash \tt{result}) \ulcorner == \urcorner  \ulcorner 1 \ div \ local(1) \urcorner[code(\backslash \tt{result}]) \leftarrow S(t) ]) )$\\
   ......... \\

\end{itemstep}
\end{slide}}




\begin{slide}[Dissolve]{WP for Java  bytecode. Example } 
What is obtained is : \\

  $( code(\backslash \tt{result}) \ulcorner == \urcorner  \ulcorner 1 \ div \ local(1) \urcorner ) $\\
  $\phantom{( code(\backslash \tt{result}) \ulcorner == \urcorner  \ulcorner 1 \ div  \  }  [$code$(\backslash \tt{result}]) \leftarrow S(t)] $  \\
  $\phantom{( code(\backslash \tt{result}) \ulcorner == \urcorner  \ulcorner 1 \ div \  }  [S(t) \leftarrow local(1)] $ \\
  $\phantom{( code(\backslash \tt{result}) \ulcorner == \urcorner  \ulcorner 1 \ div  \  }  [ t \leftarrow  t + 1 ]$\\
  $\phantom{( code(\backslash \tt{result}) \ulcorner == \urcorner  \ulcorner 1 \ div  \  } $.... \\
doing all the substitutions the weakest precondition for \texttt{m} is : \\
  $( \ulcorner   1 \ div \ local(1) \urcorner   \ulcorner == \urcorner  \ulcorner 1 \ div \ local(1) \urcorner ) $

\end{slide}


\begin{slide}[Dissolve]{Conclusion}

\begin{itemize}
\item Results
    \begin{itemize}
         \item class file  format  extension containing specification information - doesnot violate the VM specification and will not create conflicts on execution
         \item calculus for extracting proof obligations from the java bytecode and the added specification 
     \end{itemize}
\item Possible shortcomings : the size of the file  increases, tests needed
   \end{itemize}
\end{slide}
\end{document}

