Diff of /thys/BytecodeLogicJmlTypes/document/root.tex [000000] .. [653eb8]  Maximize  Restore

Switch to side-by-side view

--- a
+++ b/thys/BytecodeLogicJmlTypes/document/root.tex
@@ -0,0 +1,80 @@
+% further packages required for unusual symbols (see also isabellesym.sty)
+% use only when needed
+\usepackage{amssymb}                  % for \<leadsto>, \<box>, \<diamond>,
+                                       % \<sqsupset>, \<mho>, \<Join>, 
+                                       % \<lhd>, \<lesssim>, \<greatersim>,
+                                       % \<lessapprox>, \<greaterapprox>,
+                                       % \<triangleq>, \<yen>, \<lozenge>
+%\usepackage[greek,english]{babel}     % greek for \<euro>,
+                                       % english for \<guillemotleft>, 
+                                       %             \<guillemotright>
+                                       % default language = last
+%\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,
+                                       % \<twosuperior>, \<onehalf>,
+                                       % \<threesuperior>, \<threequarters>,
+                                       % \<degree>
+\usepackage{stmaryrd}  % for \<Sqinter>
+%\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
+                                       % (only needed if amssymb not used)
+%\usepackage{textcomp}                 % for \<cent>, \<currency>
+% this should be the last package used
+% urls in roman style, theory text in math-similar italics
+\title{A bytecode logic for JML and types\\ (Isabelle/HOL sources)}
+\author{Lennart Beringer and Martin Hofmann}
+  This document contains the Isabelle/HOL sources underlying our paper
+  \emph{A bytecode logic for JML and
+    types}~\cite{DBLP:conf/aplas/BeringerH06}, updated to Isabelle
+  2008. We present a program logic for a subset of sequential Java
+  bytecode that is suitable for representing both, features found in
+  high-level specification language JML as well as interpretations of
+  high-level type systems. To this end, we introduce a fine-grained
+  collection of assertions, including strong invariants, local
+  annotations and VDM-reminiscent partial-correctness specifications.
+  Thanks to a goal-oriented structure and interpretation of
+  judgements, verification may proceed without recourse to an
+  additional control flow analysis. The suitability for interpreting
+  intensional type systems is illustrated by the proof-carrying-code
+  style encoding of a type system for a first-order functional
+  language which guarantees a constant upper bound on the number of
+  objects allocated throughout an execution, be the execution
+  terminating or non-terminating.
+  Like the published paper, the formal development is restricted to a
+  comparatively small subset of the JVML, lacking (among other
+  features) exceptions, arrays, virtual methods, and static fields.
+  This shortcoming has been overcome meanwhile, as our paper has
+  formed the basis of the {\sc Mobius} base
+  logic~\cite{MobiusDeliverable3.1}, a program logic for the full
+  sequential fragment of the JVML. Indeed, the present formalisation
+  formed the basis of a subsequent formalisation of the {\sc Mobius}
+  base logic in the proof assistant Coq, which includes a proof of
+  soundness with respect to the Bicolano operational
+  semantics~\cite{Pichardie06}.
+\parindent 0pt\parskip 0.5ex
+% include generated text of all theories

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:

No, thanks