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