This is the title of my undergraduate thesis, written at EPFL in June 2011. I would like to thank Prof. Viktor Kuncak for supervising me on this project.
I describe rchoosec, a tool to synthesize code snippets from specifications written in the language of linear rational arithmetic. rchoosec produces a Scala subroutine that can readily be integrated in a more complex project. The main idea is to let the programmer describe what is wanted rather than how to obtain it. Another goal is to produce code that is specialized to the task at hand, so that it runs faster than calling a generic solver.
I outline some possible practical applications in control theory. In particular, I present a “proof of concept” simulator of a rocket in a gravitational field. The rocket’s engine is partially controlled by synthesized code.