93 firewall or the transaction mechanism. |
85 firewall or the transaction mechanism. |
94 |
86 |
95 |
87 |
96 Overview of the theories: |
88 Overview of the theories: |
97 \begin{description} |
89 \begin{description} |
98 \item [Basis.thy] |
90 \item[Basis] |
99 Some basic definitions and settings not specific to JavaCard but missing in HOL. |
91 Some basic definitions and settings not specific to JavaCard but missing in HOL. |
100 |
92 |
101 \item [Table.thy] |
93 \item[Table] |
102 Definition and some properties of a lookup table to map various names |
94 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). |
95 (like class names or method names) to some content (like classes or methods). |
104 |
96 |
105 \item[Name.thy] |
97 \item[Name] |
106 Definition of various names (class names, variable names, package names,...) |
98 Definition of various names (class names, variable names, package names,...) |
107 |
99 |
108 \item[Value.thy] |
100 \item[Value] |
109 JavaCard expression values (Boolean, Integer, Addresses,...) |
101 JavaCard expression values (Boolean, Integer, Addresses,...) |
110 |
102 |
111 \item[Type.thy] |
103 \item[Type] |
112 JavaCard types. Primitive types (Boolean, Integer,...) and reference types |
104 JavaCard types. Primitive types (Boolean, Integer,...) and reference types |
113 (Classes, Interfaces, Arrays,...) |
105 (Classes, Interfaces, Arrays,...) |
114 |
106 |
115 \item[Term.thy] |
107 \item[Term] |
116 JavaCard terms. Variables, expressions and statements. |
108 JavaCard terms. Variables, expressions and statements. |
117 |
109 |
118 \item[Decl.thy] |
110 \item[Decl] |
119 Class, interface and program declarations. Recursion operators for the |
111 Class, interface and program declarations. Recursion operators for the |
120 class and the interface hierarchy. |
112 class and the interface hierarchy. |
121 |
113 |
122 \item[TypeRel.thy] |
114 \item[TypeRel] |
123 Various relations on types like the subclass-, subinterface-, widening-, |
115 Various relations on types like the subclass-, subinterface-, widening-, |
124 narrowing- and casting-relation. |
116 narrowing- and casting-relation. |
125 |
117 |
126 \item[DeclConcepts.thy] |
118 \item[DeclConcepts] |
127 Advanced concepts on the class and interface hierarchy like inheritance, |
119 Advanced concepts on the class and interface hierarchy like inheritance, |
128 overriding, hiding, accessibility of types and members according to the access |
120 overriding, hiding, accessibility of types and members according to the access |
129 modifiers, method lookup. |
121 modifiers, method lookup. |
130 |
122 |
131 \item[WellType.thy] |
123 \item[WellType] |
132 Typesystem on the JavaCard term level. |
124 Typesystem on the JavaCard term level. |
133 |
125 |
134 \item[WellForm.thy] |
126 \item[WellForm] |
135 Typesystem on the JavaCard class, interface and program level. |
127 Typesystem on the JavaCard class, interface and program level. |
136 |
128 |
137 \item[State.thy] |
129 \item[State] |
138 The program state (like object store) for the execution of JavaCard. |
130 The program state (like object store) for the execution of JavaCard. |
139 Abrupt completion (exceptions, break, continue, return) is modelled as flag |
131 Abrupt completion (exceptions, break, continue, return) is modelled as flag |
140 inside the state. |
132 inside the state. |
141 |
133 |
142 \item[Eval.thy] |
134 \item[Eval] |
143 Operational (big step) semantics for JavaCard. |
135 Operational (big step) semantics for JavaCard. |
144 |
136 |
145 \item[Example.thy] |
137 \item[Example] |
146 An concrete example of a JavaCard program to validate the typesystem and the |
138 An concrete example of a JavaCard program to validate the typesystem and the |
147 operational semantics. |
139 operational semantics. |
148 |
140 |
149 \item[Conform.thy] |
141 \item[Conform] |
150 Conformance predicate for states. When does an execution state conform to the |
142 Conformance predicate for states. When does an execution state conform to the |
151 static types of the program given by the typesystem. |
143 static types of the program given by the typesystem. |
152 |
144 |
153 \item[TypeSafe.thy] |
145 \item[TypeSafe] |
154 Typesafety proof of the execution of JavaCard. ''Welltyped programs don't go |
146 Typesafety proof of the execution of JavaCard. ''Welltyped programs don't go |
155 wrong'' or more technical: The execution of a welltyped JavaCard program |
147 wrong'' or more technical: The execution of a welltyped JavaCard program |
156 preserves the conformance of execution states. |
148 preserves the conformance of execution states. |
157 |
149 |
158 \item[Evaln.thy] |
150 \item[Evaln] |
159 Copy of the operational semantics given in Eval.thy expanded with an annotation |
151 Copy of the operational semantics given in theory Eval expanded with an annotation |
160 for the maximal recursive depth. The semantics is not altered. The annotation |
152 for the maximal recursive depth. The semantics is not altered. The annotation |
161 is needed for the soundness proof of the axiomatic semantics. |
153 is needed for the soundness proof of the axiomatic semantics. |
162 |
154 |
163 \item[AxSem.thy] |
155 \item[AxSem] |
164 An axiomatic semantics (Hoare logic) for JavaCard. |
156 An axiomatic semantics (Hoare logic) for JavaCard. |
165 |
157 |
166 \item[AxSound.thy] |
158 \item[AxSound] |
167 The soundness proof of the axiomatic semantics with respect to the operational |
159 The soundness proof of the axiomatic semantics with respect to the operational |
168 semantics. |
160 semantics. |
169 |
161 |
170 \item[AxCompl.thy] |
162 \item[AxCompl] |
171 The proof of (relative) completeness of the axiomatic semantics with respect |
163 The proof of (relative) completeness of the axiomatic semantics with respect |
172 to the operational semantics. |
164 to the operational semantics. |
173 |
165 |
174 \item[AxExample.thy] |
166 \item[AxExample] |
175 An concrete example of the axiomatic semantics at work, applied to prove |
167 An concrete example of the axiomatic semantics at work, applied to prove |
176 some properties of the JavaCard example given in Example.thy. |
168 some properties of the JavaCard example given in theory Example. |
177 \end{description} |
169 \end{description} |
178 |
170 |
179 % include generated text of all theories |
171 |
180 \chapter{Basis.thy} |
172 \chapter{Basis} |
181 \input{../generated/Basis.tex} |
173 \input{Basis} |
182 \chapter{Table.thy} |
174 \chapter{Table} |
183 \input{../generated/Table.tex} |
175 \input{Table} |
184 |
176 |
185 \chapter{Name.thy} |
177 \chapter{Name} |
186 \input{../generated/Name.tex} |
178 \input{Name} |
187 \chapter{Value.thy} |
179 \chapter{Value} |
188 \input{../generated/Value.tex} |
180 \input{Value} |
189 \chapter{Type.thy} |
181 \chapter{Type} |
190 \input{../generated/Type.tex} |
182 \input{Type} |
191 \chapter{Term.thy} |
183 \chapter{Term} |
192 \input{../generated/Term.tex} |
184 \input{Term} |
193 \chapter{Decl.thy} |
185 \chapter{Decl} |
194 \input{../generated/Decl.tex} |
186 \input{Decl} |
195 \chapter{TypeRel.thy} |
187 \chapter{TypeRel} |
196 \input{../generated/TypeRel.tex} |
188 \input{TypeRel} |
197 \chapter{DeclConcepts.thy} |
189 \chapter{DeclConcepts} |
198 \input{../generated/DeclConcepts.tex} |
190 \input{DeclConcepts} |
199 |
191 |
200 \chapter{WellType.thy} |
192 \chapter{WellType} |
201 \input{../generated/WellType.tex} |
193 \input{WellType} |
202 \chapter{WellForm.thy} |
194 \chapter{WellForm} |
203 \input{../generated/WellForm.tex} |
195 \input{WellForm} |
204 |
196 |
205 \chapter{State.thy} |
197 \chapter{State} |
206 \input{../generated/State.tex} |
198 \input{State} |
207 \chapter{Eval.thy} |
199 \chapter{Eval} |
208 \input{../generated/Eval.tex} |
200 \input{Eval} |
209 |
201 |
210 \chapter{Example.thy} |
202 \chapter{Example} |
211 \input{../generated/Example.tex} |
203 \input{Example} |
212 |
204 |
213 \chapter{Conform.thy} |
205 \chapter{Conform} |
214 \input{../generated/Conform.tex} |
206 \input{Conform} |
215 \chapter{TypeSafe.thy} |
207 \chapter{TypeSafe} |
216 \input{../generated/TypeSafe.tex} |
208 \input{TypeSafe} |
217 |
209 |
218 \chapter{Evaln.thy} |
210 \chapter{Evaln} |
219 \input{../generated/Evaln.tex} |
211 \input{Evaln} |
220 \chapter{AxSem.thy} |
212 \chapter{AxSem} |
221 \input{../generated/AxSem.tex} |
213 \input{AxSem} |
222 \chapter{AxSound.thy} |
214 \chapter{AxSound} |
223 \input{../generated/AxSound.tex} |
215 \input{AxSound} |
224 \chapter{AxCompl.thy} |
216 \chapter{AxCompl} |
225 \input{../generated/AxCompl.tex} |
217 \input{AxCompl} |
226 \chapter{AxExample.thy} |
218 \chapter{AxExample} |
227 \input{../generated/AxExample.tex} |
219 \input{AxExample} |
228 |
|
229 |
|
230 |
|
231 |
|
232 |
|
233 |
|
234 |
220 |
235 %\bibliographystyle{abbrv} |
221 %\bibliographystyle{abbrv} |
236 %\bibliography{root} |
222 %\bibliography{root} |
237 |
223 |
238 \end{document} |
224 \end{document} |