kirancodes.me
To Proof Maintenance & Beyond!

GRIT-an extended REFINE for more executable specifications

Paul A. Bailes, Murray Chapman, Ming Gong, Ian Peake

Abstract

Knowledge-based software engineering (KBSE) languages should be as expressive as possible and should allow the reflection in executable programs of their non-executable specification origins. REFINE is the KBSE language for the Software Refinery metaprogramming environment. REFINE's expressiveness is extended with recursively-enumerable sets and parallel logical connectives. A subtype system was developed for the otherwise typeless functional language G, hence the name GRIT (G-REFINE InTegration) for this effort. The relationships between REFINE programs and original specifications is made possible by using the recursively-enumerable sets as the basis for a comprehensive system of run-time-checked assertions, which are subject to both set- and type-theoretic compositions.>

BibTeX
@inproceedings{Bailes-al:ASE93,
  author    = {Paul A. Bailes and
               Murray Chapman and
               Ming Gong and
               Ian Peake},
  title     = {{GRIT-an} extended {REFINE} for more executable specifications},
  booktitle = {ASE},
  pages     = {123--132},
  publisher = {{IEEE} Computer Society},
  year      = {1993},
}

Related papers