### 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.

### License

BSD License

### History

February 18, 2024
  License change to BSD; more canonical and versatile ML interfaces; some more derived language constructs.

### Topics

- Computer science/Programming languages/Language definitions
- Computer science/Programming languages/Logics

### Session Simpl

- Language
- Semantic
- HoarePartialDef
- HoarePartialProps
- HoarePartial
- Termination
- SmallStep
- HoareTotalDef
- HoareTotalProps
- HoareTotal
- Hoare
- StateSpace
- AlternativeSmallStep
- Simpl_Heap
- HeapList
- Generalise
- Vcg
- SyntaxTest
- VcgEx
- VcgExSP
- VcgExTotal
- Quicksort
- XVcg
- XVcgEx
- ProcParEx
- ProcParExSP
- Closure
- ClosureEx
- Compose
- ComposeEx
- UserGuide
- Simpl

### Used by

- Planarity Certificates
- BDD Normalisation

## Cite

×

Simpl-AFP

    @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   = {February},
      year    = {2008},
      note    = {\url{https://isa-afp.org/entries/Simpl.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2
- Dec 12, 2009 : Isabelle2009-1
- Sep 12, 2009 : Isabelle2009
- Apr 29, 2009 : Isabelle2009
- Jun 10, 2008 : Isabelle2008
- Mar 7, 2008 : Isabelle2007