There are several specification languages (e.g. ACSL) that allow the user to express complex properties and write them as assertions into computer programs. An important usage scenario for such languages are assertions that check whether a given function written in some programming language fulfills its specification. The goal of this thesis is to write a tool that allows the user to avoid writing any traditional code at all: the tool should take such specifications as input, and automatically synthesizes program code that satisfies any given specification.