Abstract: This paper introduces a tableau method based program system,called DTPS.Based on mechanical theorem proving techniques, DTPS proves the existence of an object meeting the specified conditions in order to construct a program meeting a specification.If the proof exists, the program derived from the proof not only meets the specification, but also is free from logical error.