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

Volume

2

fYear

2001

fDate

2001

Firstpage

718

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Systems, Man, and Cybernetics, 2001 IEEE International Conference on

Conference_Location

Tucson, AZ

ISSN

1062-922X

Print_ISBN

0-7803-7087-2

Type

conf

DOI

10.1109/ICSMC.2001.972999

Filename

972999