Knowledge-Based Software Engineering Conference (1995)
Nov. 12, 1995 to Nov. 15, 1995
H. Ruess , Ulm Univ., Germany
Using the example of the divide et impera program scheme we present a knowledge-assisted refinement process based on type theory that yields executable programs from given requirement specifications. Programming knowledge is described in terms of precise mathematical theories and proofs, and programs and knowledge about programs is expressed in the same language and are developed using the same techniques.
type theory; programming theory; formal specification; inference mechanisms; knowledge based systems; high-level deductive program synthesis; type theory; divide et impera program scheme; knowledge-assisted refinement process; executable programs; requirement specifications; programming knowledge; mathematical theories; mathematical proofs; language
H. Ruess, "Towards high-level deductive program synthesis based on type theory," Knowledge-Based Software Engineering Conference(KBSE), Boston, Massachusetts, 1995, pp. 174.