DocumentCode
3027753
Title
Proving Total Correctness of Refinement Based on Tableau
Author
Gao, Xiaolei ; Miao, Huaikou
Author_Institution
Comput. Dept., Dongguan Univ. of Technol., Dongguan, China
fYear
2009
fDate
10-12 Aug. 2009
Firstpage
702
Lastpage
707
Abstract
The theorem proving is the basis on tableau method. The refinement process that transforms a specification to program regards a theorem proving process. If the proof is correct, then a program that satisfies its specification can be extracted from the proof steps. This paper proves that the program is totally correct and conforms to its specification.
Keywords
reasoning about programs; theorem proving; program synthesis; refinement process; tableau method; theorem proving; Application software; Concurrent computing; Distributed computing; Distributed processing; Induction generators; Logic; Power engineering and energy; Power engineering computing; Program Synthesis; Specification; Tableau method; refinement; theorem proving; total correctness;
fLanguage
English
Publisher
ieee
Conference_Titel
Parallel and Distributed Processing with Applications, 2009 IEEE International Symposium on
Conference_Location
Chengdu
Print_ISBN
978-0-7695-3747-4
Type
conf
DOI
10.1109/ISPA.2009.48
Filename
5207855
Link To Document