Cited By
View all- van Otterlo M(2009)Intensional dynamic programming. A Rosetta stone for structured dynamic programmingJournal of Algorithms10.1016/j.jalgor.2009.04.00464:4(169-191)Online publication date: 1-Oct-2009
The synthesis of structure-changing programs
Abstract
Deductive techniques are presented for deriving programs systematically from given specifications. The specifications express the purpose of the desired program without giving any hint of the algorithm to be employed. The desired program is intended to achieve this purpose by means of such low-level primitives as assignment statements, the conditional statements, and recursion. The basic approach is to transform the specifications repeatedly according to certain rules, until a satisfactory program is produced. The rules are guided by a number of strategic controls.
Many of the transformation rules represent knowledge about the program's subject domain (e.g., numbers, lists, sets); some represent the meaning of the constructs of the specification language and the target programming language; and a few rules represent basic programming principles. The weakest-precondition operator and the concept of protection are employed to construct programs that must achieve more than one condition simultaneously.
Our previous work has centered on the synthesis of structure-maintaining programs, which produce an output without altering the value of any variable or changing the configuration of any data structure. Here, we extend our previous techniques to permit the construction of structure-changing programs, which can reset the values of variables, change the contents of an array, and alter the structure of a list or other data object.
References
[1]
Bledsoe, W. W. and M. Tyson {1977}, Typing and proof by cases in program verification, in Machine Intelligence 8: Machine Representations of Knowledge (E. W. Elcock and D. Michie, eds.), Ellis Horwood Ltd., Chichester, England, pp. 30-51.
[2]
Burstall, R. M. and J. Darlington {Jan. 1977}, A tranformation system for developing recursive programs, JACM, Vol. 24, No. 1, pp. 44-67.
[3]
Dijkstra, E. W. {Aug. 1975}, Guarded commands, nondeterminacy and formal derivation of programs, CACM, Vol. 18, No. 8, pp. 453-457.
[4]
Floyd, R. W.{1967}, Assigning meanings to programs, Proceedings of the Symposium in Applied Mathematics, Vol. 19 (J. T. Schwartz, ed.), American Mathematical Society, Providence, RI, pp. 19-32.
[5]
Hoare, C. A. R. {Oct. 1969}, An axiomatic basis for computer programming, CACM, Vol. 12, No. 10, pp. 576-580, 583.
[6]
Luckham, D. C. and J. R. Buchanan {July 1974}, Automatic generation of programs containing conditional statements, Proceedings of the Conference on Artificial Intelligence and the Simulation of Behaviour, Sussex, England, pp. 102-126.
[7]
Manna, Z. and R. Waldinger {Nov. 1977}, Synthesis: dreams &equil;> programs, Technical Report, *Artificial Intelligence Lab, Stanford University and Artificial Intelligence Center, SRI International.#
[8]
Sacerdoti, E. D. {Sept. 1975}, The nonlinear nature of plans, Proceedings of the Fourth International Joint Conference on Artificial Intelligence, Tbilisi, USSR, pp. 206-214.
[9]
Sussman, G. J. {1975}, A computer model of skill acquisition, American Elsevier, New York, NY.
[10]
Tate, A. {Sept. 1975}, Interacting goals and their use, Proceedings of the Fourth International Joint Conference on Artificial Intelligence, Tbilisi, USSR, pp. 215-218.
[11]
Waldinger, R. {1977}, Achieving several goals simultaneously, in Machine Intelligence 8: Machine Representations of Knowledge (E. W. Elcock and D. Michie, eds.), Ellis Horwood Ltd., Chichester, England, pp. 94-136.
[12]
Warren, D. H. D. {June 1974}, WARPLAN: A system for generating plans, Technical Report, Department of Computational Logic, University of Edinburgh, Edinburgh, Scotland.
[13]
Warren, D. H. D. {July 1976}, Generating conditional plans and programs, Proceedings of the Conference on Artificial Intelligence and Simulation of Behaviour, Edinburgh, Scotland, pp. 344-354.
Index Terms
- The synthesis of structure-changing programs
Recommendations
Natural synthesis of provably-correct data-structure manipulations
This paper presents natural synthesis, which generalizes the proof-theoretic synthesis technique to support very expressive logic theories. This approach leverages the natural proof methodology and reduces an intractable, unbounded-size synthesis ...
Efficient synthesis of probabilistic programs
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe show how to automatically synthesize probabilistic programs from real-world datasets. Such a synthesis is feasible due to a combination of two techniques: (1) We borrow the idea of ``sketching'' from synthesis of deterministic programs, and allow ...
Efficient synthesis of probabilistic programs
PLDI '15We show how to automatically synthesize probabilistic programs from real-world datasets. Such a synthesis is feasible due to a combination of two techniques: (1) We borrow the idea of ``sketching'' from synthesis of deterministic programs, and allow ...
Comments
Information & Contributors
Information
Published In
Sponsors
- NBS: National Bureau of Standards
- SIGSOFT: ACM Special Interest Group on Software Engineering
- IEEE-CS: Computer Society
Publisher
IEEE Press
Publication History
Published: 10 May 1978
Check for updates
Qualifiers
- Article
Acceptance Rates
Overall Acceptance Rate 276 of 1,856 submissions, 15%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 260Total Downloads
- Downloads (Last 12 months)20
- Downloads (Last 6 weeks)7
Reflects downloads up to 07 Nov 2024
Other Metrics
Citations
Cited By
View all- van Otterlo M(2009)Intensional dynamic programming. A Rosetta stone for structured dynamic programmingJournal of Algorithms10.1016/j.jalgor.2009.04.00464:4(169-191)Online publication date: 1-Oct-2009
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in