| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
| Title: | A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment |
| Author: | Norbert Schirmer (norbert /dot/ schirmer /at/ web /dot/ de) |
| Submission date: | 2008-02-29 |
| 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. |
| BibTeX: |
@article{Simpl-AFP,
author = {Norbert Schirmer},
title = {A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment},
journal = {Archive of Formal Proofs},
month = feb,
year = 2008,
note = {\url{http://isa-afp.org/entries/Simpl.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | GNU Lesser General Public License (LGPL) |
| Used by: | BDD, Planarity_Certificates |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |