ML Anthology

From Specifications to Programs: Induction in the Service of Synthesis (Abstract)

Nachum Dershowitz
ALT 1994 pp. 6-7
doi:10.1007/3-540-58520-6_48 /alt/1994/dershowitz1994alt-specifications/

Abstract

The deductive synthesis of programs from formal specifications can be aided by various forms of induction: Summative , or complete , induction is the deductive technique of reasoning by cases and plays an important role in creating conditionals. Recursive , or mathematical , induction is a deductive technique for reasoning about an infinite number of cases; it is used in the creation of loops, and is often necessary for establishing properties of data types. Eduction , or analogical reasoning, helps reduce the amount of work needed to generate a program, when similar programs already exist. Ampliative , or incomplete , induction is the process by which one generalizes from a finite number of instances; it can help the synthesizer guess what statement is needed and to verify the correctness of suggestions.

PDF ALT Semantic Scholar

Cite

Text

Dershowitz. "From Specifications to Programs: Induction in the Service of Synthesis (Abstract)." International Conference on Algorithmic Learning Theory, 1994. doi:10.1007/3-540-58520-6_48

Markdown

[Dershowitz. "From Specifications to Programs: Induction in the Service of Synthesis (Abstract)." International Conference on Algorithmic Learning Theory, 1994.](https://mlanthology.org/alt/1994/dershowitz1994alt-specifications/) doi:10.1007/3-540-58520-6_48

BibTeX

@inproceedings{dershowitz1994alt-specifications,
  title     = {{From Specifications to Programs: Induction in the Service of Synthesis (Abstract)}},
  author    = {Dershowitz, Nachum},
  booktitle = {International Conference on Algorithmic Learning Theory},
  year      = {1994},
  pages     = {6-7},
  doi       = {10.1007/3-540-58520-6_48},
  url       = {https://mlanthology.org/alt/1994/dershowitz1994alt-specifications/}
}