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