kirancodes.me
To Proof Maintenance & Beyond!
ASE 1997

Notes on Refinement, Interpolation and Uniformity

Theodosis Dimitrakos, T. S. E. Maibaum

DOI 10.1109/ase.1997.632830dblp

Abstract

The connection between some modularity properties and interpolation is revisited and restated in a general "logic-independent" framework. The presence of uniform interpolants is shown to assist in certain proof obligations, which suffice to establish the composition of refinements. The absence of the desirable interpolation properties from many logics that have been used in refinement motivates a thorough investigation of methods to expand a specification formalism orthogonally, so that the critical uniform interpolants become available. A potential breakthrough is outlined in this paper.

BibTeX
@inproceedings{Dimitrakos-Maibaum:ASE97,
  author    = {Theodosis Dimitrakos and
               T. S. E. Maibaum},
  title     = {Notes on Refinement, Interpolation and Uniformity},
  booktitle = {ASE},
  pages     = {108--116},
  publisher = {{IEEE} Computer Society},
  year      = {1997},
}

Related papers