| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Semantics and Data Refinement of Invariant Based Programs
| Title: | Semantics and Data Refinement of Invariant Based Programs |
| Authors: | Viorel Preoteasa (viorel /dot/ preoteasa /at/ aalto /dot/ fi) and Ralph-Johan Back |
| Submission date: | 2010-05-28 |
| 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. |
| Change history: | [2012-01-05]: 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. |
| BibTeX: |
@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{http://isa-afp.org/entries/DataRefinementIBP.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | LatticeProperties |
| Used by: | GraphMarkingIBP |
| 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 |