The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

MSc Thesis #92149

Title:Using Refinement Logic in Requirements Capture and Program Generation
Date: 1992
Abstract:This paper discussed the approach to requirements capture using a new notation called Refinement Logic to define problem descriptions in a lattice structure and to guide the process of program generation by extracting a program from the lattice defined. In the paper, we explain the Refinement Logic notation and present its syntax and semantics which are based on FOPC and the newly developed language COR. We also show the mapping of Refinement Logic to Prolog, the language of the program generated, and explain the translation algorithm implemented. Then, we describe some proof rules and mechanisms to help constructing the refinement lattice and explain the program extraction algorithm implemented as an interactive system and tested on two examples generating partial Prolog programs.

[Search These Pages] [DAI Home Page] [Comment]