Symbol IC-Evaluation as an Aid to Program Synthesis
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 Advance Research Projects Agency of the Department of Defence under Office of Nava...
| Main Author: | |
|---|---|
| Format: | Working Paper |
| Language: | en_US |
| Published: |
MIT Artificial Intelligence Laboratory
2008
|
| Online Access: | http://hdl.handle.net/1721.1/41952 |
| _version_ | 1811071071075434496 |
|---|---|
| author | Yonezawa, Akinori |
| author_facet | Yonezawa, Akinori |
| author_sort | Yonezawa, Akinori |
| 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 Advance Research Projects Agency of the Department of Defence under Office of Naval Research contract N00014-75-C0522. |
| first_indexed | 2024-09-23T08:45:37Z |
| format | Working Paper |
| id | mit-1721.1/41952 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T08:45:37Z |
| publishDate | 2008 |
| publisher | MIT Artificial Intelligence Laboratory |
| record_format | dspace |
| spelling | mit-1721.1/419522019-04-10T07:20:55Z Symbol IC-Evaluation as an Aid to Program Synthesis Yonezawa, Akinori 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 Advance Research Projects Agency of the Department of Defence under Office of Naval Research contract N00014-75-C0522. Symbolic-evaluation is the process which abstractly evaluates an actor program and checks to see whether the program fulfills its contract (specification). In this paper, a formalism based on the conceptual representation is proposed as a specification language and a proof system for programs which may include change of behavior (side-effects). The relation between algebraic specifications and the specifications based on the conceptual representation is discussed and the limitation of the current algebraic specifications is pointed out. The proposed formalism can deal with problems of side-effects which have been beyond the scope of Floyd-Hoare proof rules. Symbolic-evaluation is carried out with explicit use of the notion of situation (local state of an actor system). Uses of situational tags in assertions make it possible to state relations holding between objects in different situations. As an illustrative example, an impure actors which behave like a queue is extensively examined. The verification of a procedure which deals with the queue-actors and the correctness of its implementations are demonstrated by the symbolic-evaluation. Furthermore how the symbolic-evaluation serves as an aid to program synthesis is illustrated using two different implementations of the queue-actor. MIT Artificial Intelligence Laboratory Department of Defense Advanced Research Projects Agency 2008-08-25T19:41:52Z 2008-08-25T19:41:52Z 1976-04 Working Paper http://hdl.handle.net/1721.1/41952 en_US MIT Artificial Intelligence Laboratory Working Papers, WP-124; application/pdf MIT Artificial Intelligence Laboratory |
| spellingShingle | Yonezawa, Akinori Symbol IC-Evaluation as an Aid to Program Synthesis |
| title | Symbol IC-Evaluation as an Aid to Program Synthesis |
| title_full | Symbol IC-Evaluation as an Aid to Program Synthesis |
| title_fullStr | Symbol IC-Evaluation as an Aid to Program Synthesis |
| title_full_unstemmed | Symbol IC-Evaluation as an Aid to Program Synthesis |
| title_short | Symbol IC-Evaluation as an Aid to Program Synthesis |
| title_sort | symbol ic evaluation as an aid to program synthesis |
| url | http://hdl.handle.net/1721.1/41952 |
| work_keys_str_mv | AT yonezawaakinori symbolicevaluationasanaidtoprogramsynthesis |