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