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