UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

PROJECTING FUNCTIONAL MODELS OF IMPERATIVE PROGRAMS

HARMAN, M; DANICIC, S; (1993) PROJECTING FUNCTIONAL MODELS OF IMPERATIVE PROGRAMS. SIGPLAN NOTICES , 28 (11) 33 - 41.

Full text not available from this repository.

Abstract

Functional modelling [17,291 enables functional reasoning methods to be applied to programs written in imperative languages. It is, however, the view of many workers [4,24] that it is not the notation in which a program is written, but the sheer size of a program which prohibits the application of reasoning and proof techniques.The beauty of Projection is that simple aspects of programs have correspondingly simple models, irrespective of the size and complexity of the overall imperative program.We describe the Projection technique, showing how it allows for the manageable application of functional language technology to 'real' imperative programs. We demonstrate how Projection may facilitate the development of a proof of a program in terms of its constituents and how Projection may allow programmers to select the safety-critical sections of programs for particular attention.We briefly discuss the connection between Projection and Slicing, introduced by Weiser [34,35], and give examples of the functional programming techniques made available to imperative programmers by virtue of functional modelling. Specifically, we use formal proof [23,24,4], Transformation [5,91 and Partial Evaluation [14,16,31]. We claim that the Projection of functional models lends itself to the analysis and proof of existing computer software written in imperative programming languages.

Type: Article
Title: PROJECTING FUNCTIONAL MODELS OF IMPERATIVE PROGRAMS
UCL classification: UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: http://discovery.ucl.ac.uk/id/eprint/1302257
Downloads since deposit
0Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item