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}