Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project!

## [7860bc]: thys / Simpl / document / root.tex Maximize Restore History

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