|
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} |