Invariant diagrams with data refinement

Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and post-conditions as well as invariants) that could arise during the execution of the algorithm. These situations are identified before any code is written. After that,...

Full description

Saved in:
Bibliographic Details
Published in:Formal aspects of computing 2012, Vol.24 (1), p.67-95
Main Authors: Preoteasa, Viorel, Back, Ralph-Johan
Format: Article
Language:English
Subjects:
Algorithms
Computation
Computer Science
Concrete construction
Construction
Graphs
Invariants
Math Applications in Computer Science
Original Article
Programming
Theorem proving
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and post-conditions as well as invariants) that could arise during the execution of the algorithm. These situations are identified before any code is written. After that, we identify the transitions between the situations, which will give us the flow of control in the program. Data refinement is a technique of building correct programs working on concrete data structures as refinements of more abstract programs working on abstract data types. We study in this paper data refinement for invariant based programs and we apply it to the construction of the classical Deutsch–Schorr–Waite graph marking algorithm. Our results are formalized and mechanically proved in the Isabelle/HOL theorem prover.
ISSN:0934-5043
1433-299X
DOI:10.1007/s00165-011-0195-2