src/HOL/Bali/document/root.tex
 author wenzelm Wed Nov 01 20:46:23 2017 +0100 (23 months ago) changeset 66983 df83b66f1d94 parent 58887 38db8ddc0f57 permissions -rw-r--r--
proper merge (amending fb46c031c841);
     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}

    47 These theories, called Bali,  model and analyse different aspects of the

    48 JavaCard \textbf{source language}.

    49 The basis is an abstract model of the JavaCard source language.

    50 On 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

    52 the type system) according to the operational semantics is proved to be

    53 typesafe. The axiomatic semantics is proved to be sound and relative complete

    54 with respect to the operational semantics.

    55

    56 We have modelled large parts of the original JavaCard source language. It models

    57 features 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

    78 The 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

    87 In addition, features are missing that are not part of the JavaCard

    88 language, such as multithreading and garbage collection. No attempt

    89 has been made to model peculiarities of JavaCard such as the applet

    90 firewall or the transaction mechanism.

    91

    92

    93 Overview of the theories:

    94 \begin{description}

    95 \item[Basis]

    96 Some basic definitions and settings not specific to JavaCard but missing in HOL.

    97

    98 \item[Table]

    99 Definition 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]

   103 Definition of various names (class names, variable names, package names,...)

   104

   105 \item[Value]

   106 JavaCard expression values (Boolean, Integer, Addresses,...)

   107

   108 \item[Type]

   109 JavaCard types. Primitive types (Boolean, Integer,...) and reference types

   110 (Classes, Interfaces, Arrays,...)

   111

   112 \item[Term]

   113 JavaCard terms. Variables, expressions and statements.

   114

   115 \item[Decl]

   116 Class, interface and program declarations. Recursion operators for the

   117 class and the interface hierarchy.

   118

   119 \item[TypeRel]

   120 Various relations on types like the subclass-, subinterface-, widening-,

   121 narrowing- and casting-relation.

   122

   123 \item[DeclConcepts]

   124 Advanced concepts on the class and interface hierarchy like inheritance,

   125 overriding, hiding, accessibility of types and members according to the access

   126 modifiers, method lookup.

   127

   128 \item[WellType]

   129 Typesystem on the JavaCard term level.

   130

   131 \item[DefiniteAssignment]

   132 The definite assignment analysis on the JavaCard term level.

   133

   134 \item[WellForm]

   135 Typesystem on the JavaCard class, interface and program level.

   136

   137 \item[State]

   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]

   143 Operational (big step) semantics for JavaCard.

   144

   145 \item[Example]

   146 An concrete example of a JavaCard program to validate the typesystem and the

   147 operational semantics.

   148

   149 \item[Conform]

   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[DefiniteAssignmentCorrect]

   154 Correctness of the definite assignment analysis. If the analysis regards a variable as definitely assigned at a

   155 certain program point, the variable will actually be assigned there during execution.

   156

   157 \item[TypeSafe]

   158 Typesafety proof of the execution of JavaCard. ''Welltyped programs don't go

   159 wrong'' or more technical: The execution of a welltyped JavaCard program

   160 preserves the conformance of execution states.

   161

   162 \item[Evaln]

   163 Copy of the operational semantics given in theory Eval expanded with an annotation

   164 for the maximal recursive depth. The semantics is not altered. The annotation

   165 is needed for the soundness proof of the axiomatic semantics.

   166

   167 \item[Trans]

   168 A smallstep operational semantics for JavaCard.

   169

   170 \item[AxSem]

   171 An axiomatic semantics (Hoare logic) for JavaCard.

   172

   173 \item[AxSound]

   174 The soundness proof of the axiomatic semantics with respect to the operational

   175 semantics.

   176

   177 \item[AxCompl]

   178 The proof of (relative) completeness of the axiomatic semantics with respect

   179 to the operational semantics.

   180

   181 \item[AxExample]

   182 An concrete example of the axiomatic semantics at work, applied to prove

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