Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Data Refinement of Invariant B...

Data Refinement of Invariant Based Programs

Viorel Preoteasa, Ralph-Johan Back, Data Refinement of Invariant Based Programs. In: E. Boiten, J. Derrick, S. Reeves (Eds.), Proceedings of the 14th BCS-FACS Refinement Workshop (REFINE 2009) , Electronic Notes in Theoretical Computer Science 259, 143–163, Elsevier, 2009.

Abstract:

Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and postconditions 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 the 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:

@INPROCEEDINGS{inpPrBa09a,
  title = {Data Refinement of Invariant Based Programs},
  booktitle = {Proceedings of the 14th BCS-FACS Refinement Workshop (REFINE 2009) },
  author = {Preoteasa, Viorel and Back, Ralph-Johan},
  volume = {259},
  series = {Electronic Notes in Theoretical Computer Science},
  editor = {Boiten, E. and Derrick, J. and Reeves, S.},
  publisher = {Elsevier},
  pages = {143–163},
  year = {2009},
  keywords = {Invariant based programming, Data refinement, Mechanical verification},
}

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

Publication Forum rating of this publication: level 1

Edit publication