Towards automatic imperative program synthesis through proof planning

Author

Stark, Jamie ; Ireland, Andrew

Author_Institution

Dept. of Comput. & Electr. Eng., Heriot-Watt Univ., Edinburgh, UK

fYear

1999

fDate

36434

Firstpage

44

Lastpage

51

Abstract

An approach to automatic imperative program synthesis is presented which builds upon Gries´ (1981) vision of developing a program and its proof hand in hand. To achieve this vision we rely on the proof planning paradigm, which enables the coupling of both heuristic and deductive components. By formalising structured programming and proof heuristics within the proof planning framework we focus the search for a correct program. Encoding these heuristics within a proof plan and strengthening proof planning, by embedding it within the conventional AI planning paradigm, enables a significant degree of automation

Keywords

automatic programming; computer aided software engineering; heuristic programming; planning (artificial intelligence); structured programming; theorem proving; AI planning paradigm; automatic imperative program synthesis; automation; correct program; deductive components; heuristic components; proof heuristics; proof planning paradigm; structured programming formalisation; Artificial intelligence; Automation; Computer vision; Logic programming; Postal services; Writing;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 1999. 14th IEEE International Conference on.

Conference_Location

Cocoa Beach, FL

Print_ISBN

0-7695-0415-9

Type

conf

DOI

10.1109/ASE.1999.802091

Filename

802091