Title :
Proving Total Correctness of Refinement Based on Tableau
Author :
Gao, Xiaolei ; Miao, Huaikou
Author_Institution :
Comput. Dept., Dongguan Univ. of Technol., Dongguan, China
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;
Conference_Titel :
Parallel and Distributed Processing with Applications, 2009 IEEE International Symposium on
Conference_Location :
Chengdu
Print_ISBN :
978-0-7695-3747-4
DOI :
10.1109/ISPA.2009.48
