Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Invariant Diagrams with Data R...

Invariant Diagrams with Data Refinement

Viorel Preoteasa, Ralph-Johan Back, Invariant Diagrams with Data Refinement . Formal Aspects of Computing 24(1), 67–95, 2012.

Abstract:

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.

Files:

Full publication in PDF-format

BibTeX entry:

@ARTICLE{jPrBa12a,
  title = {Invariant Diagrams with Data Refinement },
  author = {Preoteasa, Viorel and Back, Ralph-Johan},
  journal = {Formal Aspects of Computing},
  volume = {24},
  number = {1},
  publisher = {Springer},
  pages = {67–95},
  year = {2012},
  keywords = {Invariant based programming – Data refinement – Mechanical verification – Graph marking},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Publication Forum rating of this publication: level 2

Edit publication