Plan Verification in a Programmer's Apprentice
This report describes research done at the Artificial Intelligence Laboratory of the Massachusetts Institute of Technology. Support for the Laboratory's artificial intelligence research is provided in part by the Advanced Research Projects Agency of the Department of Defense under the Office of...
| Main Author: | |
|---|---|
| Format: | Working Paper |
| Language: | en_US |
| Published: |
MIT Artificial Intelligence Laboratory
2008
|
| Online Access: | http://hdl.handle.net/1721.1/41968 |
| _version_ | 1826215328189775872 |
|---|---|
| author | Shrobe, Howard Elliot |
| author_facet | Shrobe, Howard Elliot |
| author_sort | Shrobe, Howard Elliot |
| collection | MIT |
| description | This report describes research done at the Artificial Intelligence Laboratory of the Massachusetts Institute of Technology. Support for the Laboratory's artificial intelligence research is provided in part by the Advanced Research Projects Agency of the Department of Defense under the Office of Naval Research contract N00014-75-C-0643. |
| first_indexed | 2024-09-23T16:24:06Z |
| format | Working Paper |
| id | mit-1721.1/41968 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T16:24:06Z |
| publishDate | 2008 |
| publisher | MIT Artificial Intelligence Laboratory |
| record_format | dspace |
| spelling | mit-1721.1/419682019-04-11T04:02:58Z Plan Verification in a Programmer's Apprentice Shrobe, Howard Elliot This report describes research done at the Artificial Intelligence Laboratory of the Massachusetts Institute of Technology. Support for the Laboratory's artificial intelligence research is provided in part by the Advanced Research Projects Agency of the Department of Defense under the Office of Naval Research contract N00014-75-C-0643. Brief Statement of the Problem: An interactive programming environment called the Programmer's Apprentice is described. Intended for use by the expert programmer in the process of program design and maintenance, the apprentice will be capable of understanding, explaining and reasoning about the behavior of real-world LISP programs with side effects on complex data-structures. We view programs as engineered devices whose analysis must be carried out at many level of abstraction. This leads to a set of logical dependencies between modules which explains how and why modules interact to achieve an overall intention. Such a network of dependencies is a teleological structure which we call a plan; the process of elucidating such a plan stucture and showing that it is coherent and that it achieves its overall intended behavior we call plan verification. This approach to program verification is sharply contrasted with the traditional Floyd-Hoare systems which overly restrict themselves to surface features of the programming language. More similar in philosophy is the evolving methodology of languages like CLU or ALPHARD which stress conceptual layering. MIT Artificial Intelligence Laboratory Department of Defense Advanced Research Projects Agency 2008-08-26T14:48:46Z 2008-08-26T14:48:46Z 1978-01 Working Paper http://hdl.handle.net/1721.1/41968 en_US MIT Artificial Intelligence Laboratory Working Papers, WP-158; application/pdf MIT Artificial Intelligence Laboratory |
| spellingShingle | Shrobe, Howard Elliot Plan Verification in a Programmer's Apprentice |
| title | Plan Verification in a Programmer's Apprentice |
| title_full | Plan Verification in a Programmer's Apprentice |
| title_fullStr | Plan Verification in a Programmer's Apprentice |
| title_full_unstemmed | Plan Verification in a Programmer's Apprentice |
| title_short | Plan Verification in a Programmer's Apprentice |
| title_sort | plan verification in a programmer s apprentice |
| url | http://hdl.handle.net/1721.1/41968 |
| work_keys_str_mv | AT shrobehowardelliot planverificationinaprogrammersapprentice |