equal
deleted
inserted
replaced
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *} |
7 header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *} |
8 |
8 |
9 theory BVSpecTypeSafe = Correct: |
9 theory BVSpecTypeSafe imports Correct begin |
10 |
10 |
11 text {* |
11 text {* |
12 This theory contains proof that the specification of the bytecode |
12 This theory contains proof that the specification of the bytecode |
13 verifier only admits type safe programs. |
13 verifier only admits type safe programs. |
14 *} |
14 *} |