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