1\documentclass[11pt,a4paper]{article} 2\usepackage{isabelle,isabellesym} 3 4\usepackage{amssymb} 5\usepackage[english]{babel} 6\usepackage[utf8]{inputenc} 7\usepackage[only,bigsqcap]{stmaryrd} 8\usepackage{eufrak} 9\usepackage{textcomp} 10 11% this should be the last package used 12\usepackage{pdfsetup} 13 14% urls in roman style, theory text in math-similar italics 15\urlstyle{rm} 16 17% for rule output in LaTeXsugar 18\usepackage{mathpartir} 19\usepackage{graphicx} 20\isabellestyle{it} 21 22% this should be the last package used 23\usepackage{pdfsetup} 24 25\renewcommand{\isasymacute}{\isatext{\'\relax\hspace{-0.20em}}} 26\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup\relax\hspace{-0.15em}} 27 28\begin{document} 29 30\title{--- \textbf{Simpl} --- \\ 31 A Sequential Imperative Programming Language\\ 32 Syntax, Semantics, Hoare Logics and Verification Environment} 33\author{Norbert W. Schirmer} 34 35\begin{abstract} 36We present the theory of Simpl, a sequential imperative programming language. 37We introduce its syntax, its semantics (big and small-step operational 38semantics) and Hoare logics for both partial as well as total correctness. 39We prove soundness and completeness of the Hoare logic. We 40integrate and automate the Hoare logic in Isabelle/HOL to obtain a 41practically usable verification environment for imperative programs. 42 43Simpl is independent of a concrete programming language but expressive 44enough to cover all common language features: mutually recursive 45procedures, abrupt termination and exceptions, runtime faults, local 46and global variables, pointers and heap, expressions with side 47effects, pointers to procedures, partial application and closures, 48dynamic method invocation and also unbounded nondeterminism. 49\end{abstract} 50 51\maketitle 52 53\tableofcontents 54\parindent 0pt\parskip 0.5ex 55 56\pagebreak 57 58\begin{center} 59 \makebox[0pt]{\includegraphics[width=\paperwidth=\textheight,keepaspectratio]{session_graph} 60}\end{center} 61 62\pagebreak 63 64\section{Introduction} 65 66The work presented in these theories was developed within the German Verisoft 67project\footnote{\url{http://www.verisoft.de}}. A thorough description of the core 68parts can be found in my PhD thesis~\cite{Schirmer-PhD}. A tutorial-like user guide 69is in Section~\ref{sec:UserGuide}. 70 71Applications so far include BDD-normalisation~\cite{Ortner-Schirmer-TPHOL05}, 72a C0 compiler~\cite{Leinenbach:SSV08-??}, a page fault handler~\cite{Alkassar:TACAS08-??} 73and extensions towards separation logic~\cite{Tuch:separation-logic:2007}. 74 75 76% generated text of all theories 77\input{session} 78 79% optional bibliography 80\bibliographystyle{abbrv} 81\bibliography{root} 82 83\end{document} 84 85%%% Local Variables: 86%%% mode: latex 87%%% TeX-master: t 88%%% End: 89