ZHAO Ying, QUAN Bingzhe, JIN Chunzhao. DTPS: A PROGRAM SYNTHESIS SYSTEM BASED ON TABLEAU METHODJ. Journal of Computer Research and Development, 1997, 34(8).
Citation:
ZHAO Ying, QUAN Bingzhe, JIN Chunzhao. DTPS: A PROGRAM SYNTHESIS SYSTEM BASED ON TABLEAU METHODJ. Journal of Computer Research and Development, 1997, 34(8).
ZHAO Ying, QUAN Bingzhe, JIN Chunzhao. DTPS: A PROGRAM SYNTHESIS SYSTEM BASED ON TABLEAU METHODJ. Journal of Computer Research and Development, 1997, 34(8).
Citation:
ZHAO Ying, QUAN Bingzhe, JIN Chunzhao. DTPS: A PROGRAM SYNTHESIS SYSTEM BASED ON TABLEAU METHODJ. Journal of Computer Research and Development, 1997, 34(8).
DTPS: A PROGRAM SYNTHESIS SYSTEM BASED ON TABLEAU METHOD
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.
DownLoad: