Title :
A formal method for proving programs correct
Author :
Chiang, Chia-Chu ; NEUBART, DAVID
Author_Institution :
Dept. of Comput. Sci., Arkansas Univ., Little Rock, AR, USA
Abstract :
A formal method using a formal specification, called TUG (Tree Unified with Grammar) is introduced to develop software. A formal specification is written and then systematically mapped into a structured design and successively into a structured program. The mapping process is performed in terms of the patterns of Sequence, Selection, and Iteration in the specification with a set of mapping rules. The patterns build a linkage between specification, design, code, and proofs. Whenever there is a change of user requirements, the impact and changes are located and traced in the specification, design and code in terms of the patterns
Keywords :
formal specification; grammars; program verification; structured programming; theorem proving; trees (mathematics); TUG; Tree Unified with Grammar; formal method; formal specification; mapping process; mapping rules; program correctness proving; program proofs; structured design; structured program; user requirements; Computer languages; Computer science; Costs; Couplings; Formal specifications; Natural languages; Programming; Skeleton; Software testing; Tree data structures;
Conference_Titel :
Systems, Man, and Cybernetics, 2001 IEEE International Conference on
Conference_Location :
Tucson, AZ
Print_ISBN :
0-7803-7087-2
DOI :
10.1109/ICSMC.2001.972999
