Function Extraction: Mapping Programs into Mathematica Equations

Ali Mili

Much of the trouble in software engineering stems from our inability to determine precisely the functionof a program; programmers routinely write programs whose precise function they do not know, and canonly speculate about; and most modern software development processes involve composing existingsoftware components on the basis of documentation that is typically vague, incomplete and outdated. Inthis talk we discuss the design and implementation of a tool that derives the function of a C-like programby mapping it onto a mathematical equation formulated in the syntax of Mathematica (© WolframResearch). Such an equation involves the program’s inputs and outputs; by solving this equation in theoutput as a function of the input, we obtain the function of the program. Also, whether the function can orcannot be solved, it can still be used to prove or disprove the correctness of the program with respect tospecifications. The unique novelty of our approach is that we can capture the semantics of iterativeconstructs in full, provided we codify the requisite programming knowledge and domain knowledge.