src/HOL/Bali/document/root.tex
author berghofe
Sat Jan 30 17:03:46 2010 +0100 (2010-01-30)
changeset 34990 81e8fdfeb849
parent 28181 e98be9824b7d
child 58887 38db8ddc0f57
permissions -rw-r--r--
Adapted to changes in cases method.
     1 
     2 \documentclass[11pt,a4paper]{book}
     3 \usepackage{isabelle,isabellesym}
     4 \usepackage{latexsym}
     5 \usepackage{graphicx}
     6 \usepackage{pdfsetup}
     7 \usepackage[english]{babel}
     8 \usepackage{ifthen}
     9 
    10 \urlstyle{rm}
    11 \isabellestyle{it}
    12 
    13 \pagestyle{myheadings}
    14 
    15 \addtolength{\hoffset}{-1,5cm}
    16 \addtolength{\textwidth}{4cm}
    17 \addtolength{\voffset}{-2cm}
    18 \addtolength{\textheight}{4cm}
    19 
    20 %subsection instead of section to make the toc readable
    21 \renewcommand{\thesubsection}{\arabic{subsection}}
    22 \renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
    23 \renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}
    24 
    25 %remove spaces from the isabelle environment (trivlist makes them too large)
    26 \renewenvironment{isabelle}
    27 {\begin{isabellebody}}
    28 {\end{isabellebody}}
    29 
    30 \renewcommand{\isacommand}[1]{\ifthenelse{\equal{#1}{lemma}}
    31 {\par\isakeyword{#1}}{\isakeyword{#1}}}
    32 
    33 \begin{document}
    34 
    35 \title{Java Source and Bytecode Formalizations in Isabelle: Bali}
    36 \author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and
    37   Leonor Prensa Nieto \and Norbert Schirmer \and Martin Strecker}
    38 \maketitle
    39 
    40 \tableofcontents
    41 
    42 \begin{center}
    43   \includegraphics[scale=0.7]{session_graph}
    44 \end{center}
    45 
    46 \parindent 0pt\parskip 0.5ex
    47 \chapter{Overview}
    48 These theories, called Bali,  model and analyse different aspects of the 
    49 JavaCard \textbf{source language}. 
    50 The basis is an abstract model of the JavaCard source language. 
    51 On it, a type system, an operational semantics and an axiomatic semantics 
    52 (Hoare logic) are built. The execution of a wellformed program (with respect to
    53 the type system) according to the operational semantics is proved to be 
    54 typesafe. The axiomatic semantics is proved to be sound and relative complete 
    55 with respect to the operational semantics.
    56 
    57 We have modelled large parts of the original JavaCard source language. It models
    58 features such as:
    59 \begin{itemize}
    60 \item The basic ``primitive types'' of Java 
    61 \item Classes and related concepts 
    62 \item Class fields and methods
    63 \item Instance fields and methods
    64 \item Interfaces and related concepts 
    65 \item Arrays
    66 \item Static initialisation
    67 \item Static overloading of fields and methods
    68 \item Inheritance, overriding and hiding of methods, dynamic binding
    69 \item All cases of abrupt termination
    70       \begin{itemize}
    71         \item Exception throwing and handling
    72         \item \texttt{break}, \texttt{continue} and \texttt{return} 
    73       \end{itemize}
    74 \item Packages
    75 \item Access Modifiers (\texttt{private}, \texttt{protected}, \texttt{public})
    76 \item A ``definite assignment'' check
    77 \end{itemize}
    78 
    79 The following features are missing in Bali wrt.{} JavaCard:
    80 \begin{itemize}
    81 \item Some primitive types (\texttt{byte, short})
    82 \item Syntactic variants of statements
    83   (\texttt{do}-loop, \texttt{for}-loop)
    84 \item Interface fields
    85 \item Inner Classes
    86 \end{itemize}
    87 
    88 In addition, features are missing that are not part of the JavaCard
    89 language, such as multithreading and garbage collection. No attempt
    90 has been made to model peculiarities of JavaCard such as the applet
    91 firewall or the transaction mechanism.
    92 
    93 
    94 Overview of the theories:
    95 \begin{description}
    96 \item[Basis] 
    97 Some basic definitions and settings not specific to JavaCard but missing in HOL.
    98 
    99 \item[Table]
   100 Definition and some properties of a lookup table to map various names 
   101 (like class names or method names) to some content (like classes or methods).
   102 
   103 \item[Name]
   104 Definition of various names (class names, variable names, package names,...)
   105 
   106 \item[Value]
   107 JavaCard expression values (Boolean, Integer, Addresses,...)
   108 
   109 \item[Type]
   110 JavaCard types. Primitive types (Boolean, Integer,...) and reference types 
   111 (Classes, Interfaces, Arrays,...)
   112 
   113 \item[Term]
   114 JavaCard terms. Variables, expressions and statements.
   115 
   116 \item[Decl]
   117 Class, interface and program declarations. Recursion operators for the
   118 class and the interface hierarchy. 
   119 
   120 \item[TypeRel]
   121 Various relations on types like the subclass-, subinterface-, widening-, 
   122 narrowing- and casting-relation.
   123 
   124 \item[DeclConcepts]
   125 Advanced concepts on the class and interface hierarchy like inheritance, 
   126 overriding, hiding, accessibility of types and members according to the access 
   127 modifiers, method lookup.
   128 
   129 \item[WellType]
   130 Typesystem on the JavaCard term level.
   131 
   132 \item[DefiniteAssignment]
   133 The definite assignment analysis on the JavaCard term level.
   134 
   135 \item[WellForm]
   136 Typesystem on the JavaCard class, interface and program level.
   137 
   138 \item[State]
   139 The program state (like object store) for the execution of JavaCard.
   140 Abrupt completion (exceptions, break, continue, return) is modelled as flag
   141 inside the state.
   142 
   143 \item[Eval]
   144 Operational (big step) semantics for JavaCard.
   145 
   146 \item[Example]
   147 An concrete example of a JavaCard program to validate the typesystem and the
   148 operational semantics.
   149 
   150 \item[Conform]
   151 Conformance predicate for states. When does an execution state conform to the
   152 static types of the program given by the typesystem.
   153 
   154 \item[DefiniteAssignmentCorrect]
   155 Correctness of the definite assignment analysis. If the analysis regards a variable as definitely assigned at a
   156 certain program point, the variable will actually be assigned there during execution.
   157 
   158 \item[TypeSafe]
   159 Typesafety proof of the execution of JavaCard. ''Welltyped programs don't go
   160 wrong'' or more technical: The execution of a welltyped JavaCard program 
   161 preserves the conformance of execution states.
   162 
   163 \item[Evaln]
   164 Copy of the operational semantics given in theory Eval expanded with an annotation
   165 for the maximal recursive depth. The semantics is not altered. The annotation
   166 is needed for the soundness proof of the axiomatic semantics.
   167 
   168 \item[Trans]
   169 A smallstep operational semantics for JavaCard.
   170 
   171 \item[AxSem]
   172 An axiomatic semantics (Hoare logic) for JavaCard.
   173 
   174 \item[AxSound]
   175 The soundness proof of the axiomatic semantics with respect to the operational
   176 semantics.
   177 
   178 \item[AxCompl]
   179 The proof of (relative) completeness of the axiomatic semantics with respect
   180 to the operational semantics. 
   181 
   182 \item[AxExample]
   183 An concrete example of the axiomatic semantics at work, applied to prove 
   184 some properties of the JavaCard example given in theory Example.
   185 \end{description}
   186 
   187 
   188 \chapter{Basis}
   189 \input{Basis}
   190 
   191 \chapter{Table}
   192 \input{Table}    
   193 
   194 \chapter{Name}
   195 \input{Name}
   196 
   197 \chapter{Value}     
   198 \input{Value}
   199 
   200 \chapter{Type}
   201 \input{Type}      
   202 
   203 \chapter{Term}
   204 \input{Term}     
   205 
   206 \chapter{Decl}
   207 \input{Decl}          
   208 
   209 \chapter{TypeRel}
   210 \input{TypeRel}   
   211 
   212 \chapter{DeclConcepts}
   213 \input{DeclConcepts}  
   214 
   215 \chapter{WellType}
   216 \input{WellType}
   217 
   218 \chapter{DefiniteAssignment}
   219 \input{DefiniteAssignment}
   220 
   221 \chapter{WellForm}
   222 \input{WellForm}
   223 
   224 \chapter{State}
   225 \input{State}    
   226 
   227 \chapter{Eval}
   228 \input{Eval}          
   229 
   230 \chapter{Example}
   231 \input{Example}  
   232 
   233 \chapter{Conform}
   234 \input{Conform}       
   235 
   236 \chapter{DefiniteAssignmentCorrect}
   237 \input{DefiniteAssignmentCorrect}
   238 
   239 \chapter{TypeSafe}
   240 \input{TypeSafe}
   241 
   242 \chapter{Evaln}
   243 \input{Evaln}         
   244 
   245 \chapter{Trans}
   246 \input{Trans}         
   247 
   248 \chapter{AxSem}
   249 \input{AxSem}      
   250 
   251 \chapter{AxSound}
   252 \input{AxSound}    
   253 
   254 \chapter{AxCompl}
   255 \input{AxCompl}    
   256 
   257 \chapter{AxExample}
   258 \input{AxExample}  
   259 
   260 %\bibliographystyle{abbrv}
   261 %\bibliography{root}
   262 
   263 \end{document}