### Abstract

The invariant based programming is a technique of constructing correct programs by first identifying the basic situations (pre- and post-conditions and invariants) that can occur during the execution of the program, and then defining the transitions and proving that they preserve the invariants. Data refinement is a technique of building correct programs working on concrete datatypes as refinements of more abstract programs. In the theories presented here we formalize the predicate transformer semantics for invariant based programs and their data refinement.

### License

BSD License

### History

January 5, 2012
  Moved some general complete lattice properties to the AFP entry Lattice Properties. Changed the definition of the data refinement relation to be more general and updated all corresponding theorems. Added new syntax for demonic and angelic update statements.

### Topics

- Computer science/Programming languages/Logics

### Session DataRefinementIBP

- Preliminaries
- Statements
- Hoare
- Diagram
- DataRefinement

### Depends on

- Lattice Properties

### Used by

- Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement

### Auto-related entries

- Transformer Semantics
- Kleene Algebras with Domain
- Refinement for Monadic Programs
- Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement

## Cite

×

DataRefinementIBP-AFP

    @article{DataRefinementIBP-AFP,
      author  = {Viorel Preoteasa and Ralph-Johan Back},
      title   = {Semantics and Data Refinement of Invariant Based Programs},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2010},
      note    = {\url{https://isa-afp.org/entries/DataRefinementIBP.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 18, 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
- Jun 30, 2010 : Isabelle2009-2
- May 28, 2010 : Isabelle2009-1