Separation Logic for While Programs with Functions

Sep-Imp Example version 0.3

About

We design and prove the soundness of a separation logic for a simple imperative language with loops and functions.

Note: We are planning some human-readable documentation.  For now, see our APLAS tutorial and this web site.

This example is designed to showcase some of the features of the Mechanized Semantic Library, particularly the Separation Algebra and Logics components.  It is distributed with the MSL under the same BSD-style license.

Component Overview

# Name Description
1. Setup Engineering to handle files in multiple directories (for Proof General)
2. Machine Syntax and operational semantics of the machine
3. Separation Logic Models of assertions and Hoare triples of Separation Logic; soundness proofs of Hoare rules

File list

# File name Line count     Component
1. 0path.v 1   Setup
2. imp.v 265   Machine
3. hoare.v 1,732   Separation Logic
         
  Total 1,998    

Component Details

Setup

Download 0path.v
An engineering hack to help Proof General handle files in multiple directories.

Machine

Download imp.v
Definition of the syntax and operational semantics of the machine; that is, most of the TCB.  A few simple lemmas about the semantics.

Separation Logic

Download hoare.v
Semantics of assertions.  Semantics of Hoare judgment and proofs of the soundness of the standard Hoare rules.  Most of the work is in the call rule and the while rule.

People

The Mechanized Semantic Library is developed and maintained by Andrew W. Appel, Robert Dockins, and Aquinas Hobor.

License

Copyright (c) 2009-2010, Andrew Appel, Robert Dockins and Aquinas Hobor.
All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

- Redistribution of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

- Redistribution in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR THE CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.