Semantics and Data Refinement of Invariant Based Programs (Q7361822)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry DataRefinementIBP
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Semantics and Data Refinement of Invariant Based Programs |
AFP entry DataRefinementIBP |
Statements
28 May 2010
0 references
Viorel Preoteasa
0 references
Ralph-Johan Back
0 references
Semantics and Data Refinement of Invariant Based Programs (English)
0 references
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.
0 references
