tuned;
authorwenzelm
Mon Jan 28 18:48:25 2002 +0100 (2002-01-28)
changeset 1285617ae8bbb46cb
parent 12855 21225338f8db
child 12857 a4386cc9b1c3
tuned;
src/HOL/Bali/document/root.tex
     1.1 --- a/src/HOL/Bali/document/root.tex	Mon Jan 28 17:52:13 2002 +0100
     1.2 +++ b/src/HOL/Bali/document/root.tex	Mon Jan 28 18:48:25 2002 +0100
     1.3 @@ -1,22 +1,10 @@
     1.4  
     1.5  \documentclass[11pt,a4paper]{book}
     1.6  \usepackage{isabelle,isabellesym}
     1.7 -
     1.8 -% further packages required for unusual symbols (see also isabellesym.sty)
     1.9  \usepackage{latexsym}
    1.10 -%\usepackage{amssymb}
    1.11 -%\usepackage[english]{babel}
    1.12 -%\usepackage[latin1]{inputenc}
    1.13 -%\usepackage[only,bigsqcap]{stmaryrd}
    1.14 -%\usepackage{wasysym}
    1.15 -%\usepackage{eufrak}
    1.16 -%\usepackage{textcomp}
    1.17 -%\usepackage{marvosym}
    1.18 -
    1.19 -% this should be the last package used
    1.20 +\usepackage{graphicx}
    1.21  \usepackage{pdfsetup}
    1.22  
    1.23 -% proper setup for best-style documents
    1.24  \urlstyle{rm}
    1.25  \isabellestyle{it}
    1.26  
    1.27 @@ -37,16 +25,20 @@
    1.28  {\begin{isabellebody}}
    1.29  {\end{isabellebody}}
    1.30  
    1.31 +
    1.32  \begin{document}
    1.33  
    1.34 -\title{Java Source and Bytecode Formalizations in Isabelle: Bali\\
    1.35 -  {\large -- VerifiCard Project Deliverables -- }}
    1.36 +\title{Java Source and Bytecode Formalizations in Isabelle: Bali}
    1.37  \author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and
    1.38    Leonor Prensa Nieto \and Norbert Schirmer \and Martin Strecker}
    1.39  \maketitle
    1.40  
    1.41  \tableofcontents
    1.42  
    1.43 +\begin{center}
    1.44 +  \includegraphics[scale=0.7]{session_graph}
    1.45 +\end{center}
    1.46 +
    1.47  \parindent 0pt\parskip 0.5ex
    1.48  \chapter{Overview}
    1.49  These theories, called Bali,  model and analyse different aspects of the 
    1.50 @@ -95,142 +87,136 @@
    1.51  
    1.52  Overview of the theories:
    1.53  \begin{description}
    1.54 -\item [Basis.thy] 
    1.55 +\item[Basis] 
    1.56  Some basic definitions and settings not specific to JavaCard but missing in HOL.
    1.57  
    1.58 -\item [Table.thy]
    1.59 +\item[Table]
    1.60  Definition and some properties of a lookup table to map various names 
    1.61  (like class names or method names) to some content (like classes or methods).
    1.62  
    1.63 -\item[Name.thy]
    1.64 +\item[Name]
    1.65  Definition of various names (class names, variable names, package names,...)
    1.66  
    1.67 -\item[Value.thy]
    1.68 +\item[Value]
    1.69  JavaCard expression values (Boolean, Integer, Addresses,...)
    1.70  
    1.71 -\item[Type.thy]
    1.72 +\item[Type]
    1.73  JavaCard types. Primitive types (Boolean, Integer,...) and reference types 
    1.74  (Classes, Interfaces, Arrays,...)
    1.75  
    1.76 -\item[Term.thy]
    1.77 +\item[Term]
    1.78  JavaCard terms. Variables, expressions and statements.
    1.79  
    1.80 -\item[Decl.thy]
    1.81 +\item[Decl]
    1.82  Class, interface and program declarations. Recursion operators for the
    1.83  class and the interface hierarchy. 
    1.84  
    1.85 -\item[TypeRel.thy]
    1.86 +\item[TypeRel]
    1.87  Various relations on types like the subclass-, subinterface-, widening-, 
    1.88  narrowing- and casting-relation.
    1.89  
    1.90 -\item[DeclConcepts.thy]
    1.91 +\item[DeclConcepts]
    1.92  Advanced concepts on the class and interface hierarchy like inheritance, 
    1.93  overriding, hiding, accessibility of types and members according to the access 
    1.94  modifiers, method lookup.
    1.95  
    1.96 -\item[WellType.thy]
    1.97 +\item[WellType]
    1.98  Typesystem on the JavaCard term level.
    1.99  
   1.100 -\item[WellForm.thy]
   1.101 +\item[WellForm]
   1.102  Typesystem on the JavaCard class, interface and program level.
   1.103  
   1.104 -\item[State.thy]
   1.105 +\item[State]
   1.106  The program state (like object store) for the execution of JavaCard.
   1.107  Abrupt completion (exceptions, break, continue, return) is modelled as flag
   1.108  inside the state.
   1.109  
   1.110 -\item[Eval.thy]
   1.111 +\item[Eval]
   1.112  Operational (big step) semantics for JavaCard.
   1.113  
   1.114 -\item[Example.thy]
   1.115 +\item[Example]
   1.116  An concrete example of a JavaCard program to validate the typesystem and the
   1.117  operational semantics.
   1.118  
   1.119 -\item[Conform.thy]
   1.120 +\item[Conform]
   1.121  Conformance predicate for states. When does an execution state conform to the
   1.122  static types of the program given by the typesystem.
   1.123  
   1.124 -\item[TypeSafe.thy]
   1.125 +\item[TypeSafe]
   1.126  Typesafety proof of the execution of JavaCard. ''Welltyped programs don't go
   1.127  wrong'' or more technical: The execution of a welltyped JavaCard program 
   1.128  preserves the conformance of execution states.
   1.129  
   1.130 -\item[Evaln.thy]
   1.131 -Copy of the operational semantics given in Eval.thy expanded with an annotation
   1.132 +\item[Evaln]
   1.133 +Copy of the operational semantics given in theory Eval expanded with an annotation
   1.134  for the maximal recursive depth. The semantics is not altered. The annotation
   1.135  is needed for the soundness proof of the axiomatic semantics.
   1.136  
   1.137 -\item[AxSem.thy]
   1.138 +\item[AxSem]
   1.139  An axiomatic semantics (Hoare logic) for JavaCard.
   1.140  
   1.141 -\item[AxSound.thy]
   1.142 +\item[AxSound]
   1.143  The soundness proof of the axiomatic semantics with respect to the operational
   1.144  semantics.
   1.145  
   1.146 -\item[AxCompl.thy]
   1.147 +\item[AxCompl]
   1.148  The proof of (relative) completeness of the axiomatic semantics with respect
   1.149  to the operational semantics. 
   1.150  
   1.151 -\item[AxExample.thy]
   1.152 +\item[AxExample]
   1.153  An concrete example of the axiomatic semantics at work, applied to prove 
   1.154 -some properties of the JavaCard example given in Example.thy.
   1.155 +some properties of the JavaCard example given in theory Example.
   1.156  \end{description}
   1.157  
   1.158 -% include generated text of all theories
   1.159 -\chapter{Basis.thy}
   1.160 -\input{../generated/Basis.tex}
   1.161 -\chapter{Table.thy}
   1.162 -\input{../generated/Table.tex}    
   1.163 +
   1.164 +\chapter{Basis}
   1.165 +\input{Basis}
   1.166 +\chapter{Table}
   1.167 +\input{Table}    
   1.168  
   1.169 -\chapter{Name.thy}
   1.170 -\input{../generated/Name.tex}
   1.171 -\chapter{Value.thy}     
   1.172 -\input{../generated/Value.tex}
   1.173 -\chapter{Type.thy}
   1.174 -\input{../generated/Type.tex}      
   1.175 -\chapter{Term.thy}
   1.176 -\input{../generated/Term.tex}     
   1.177 -\chapter{Decl.thy}
   1.178 -\input{../generated/Decl.tex}          
   1.179 -\chapter{TypeRel.thy}
   1.180 -\input{../generated/TypeRel.tex}   
   1.181 -\chapter{DeclConcepts.thy}
   1.182 -\input{../generated/DeclConcepts.tex}  
   1.183 -
   1.184 -\chapter{WellType.thy}
   1.185 -\input{../generated/WellType.tex}
   1.186 -\chapter{WellForm.thy}
   1.187 -\input{../generated/WellForm.tex}
   1.188 +\chapter{Name}
   1.189 +\input{Name}
   1.190 +\chapter{Value}     
   1.191 +\input{Value}
   1.192 +\chapter{Type}
   1.193 +\input{Type}      
   1.194 +\chapter{Term}
   1.195 +\input{Term}     
   1.196 +\chapter{Decl}
   1.197 +\input{Decl}          
   1.198 +\chapter{TypeRel}
   1.199 +\input{TypeRel}   
   1.200 +\chapter{DeclConcepts}
   1.201 +\input{DeclConcepts}  
   1.202  
   1.203 -\chapter{State.thy}
   1.204 -\input{../generated/State.tex}    
   1.205 -\chapter{Eval.thy}
   1.206 -\input{../generated/Eval.tex}          
   1.207 +\chapter{WellType}
   1.208 +\input{WellType}
   1.209 +\chapter{WellForm}
   1.210 +\input{WellForm}
   1.211  
   1.212 -\chapter{Example.thy}
   1.213 -\input{../generated/Example.tex}  
   1.214 +\chapter{State}
   1.215 +\input{State}    
   1.216 +\chapter{Eval}
   1.217 +\input{Eval}          
   1.218  
   1.219 -\chapter{Conform.thy}
   1.220 -\input{../generated/Conform.tex}       
   1.221 -\chapter{TypeSafe.thy}
   1.222 -\input{../generated/TypeSafe.tex}
   1.223 +\chapter{Example}
   1.224 +\input{Example}  
   1.225  
   1.226 -\chapter{Evaln.thy}
   1.227 -\input{../generated/Evaln.tex}         
   1.228 -\chapter{AxSem.thy}
   1.229 -\input{../generated/AxSem.tex}      
   1.230 -\chapter{AxSound.thy}
   1.231 -\input{../generated/AxSound.tex}    
   1.232 -\chapter{AxCompl.thy}
   1.233 -\input{../generated/AxCompl.tex}    
   1.234 -\chapter{AxExample.thy}
   1.235 -\input{../generated/AxExample.tex}  
   1.236 +\chapter{Conform}
   1.237 +\input{Conform}       
   1.238 +\chapter{TypeSafe}
   1.239 +\input{TypeSafe}
   1.240  
   1.241 -
   1.242 -
   1.243 -
   1.244 -
   1.245 -
   1.246 +\chapter{Evaln}
   1.247 +\input{Evaln}         
   1.248 +\chapter{AxSem}
   1.249 +\input{AxSem}      
   1.250 +\chapter{AxSound}
   1.251 +\input{AxSound}    
   1.252 +\chapter{AxCompl}
   1.253 +\input{AxCompl}    
   1.254 +\chapter{AxExample}
   1.255 +\input{AxExample}  
   1.256  
   1.257  %\bibliographystyle{abbrv}
   1.258  %\bibliography{root}