Verifiable program construction in a user-friendly style

Author

Naftalin, M.

Author_Institution

Dept. of Comput. Sci., Stirling Univ.

fYear

1988

fDate

5-7 Oct 1988

Firstpage

60

Lastpage

66

Abstract

The author presents a method for formal program development, designed specifically for use at an introductory level. It formalizes stepwise refinement in a natural way by regarding specifications as unimplemented program components. A graphical notation is used for specifications and their refinement rules, which supports this approach. The method places specifications and programs within the same semantic framework and gives the same meaning to the standard compositional operators (sequence, selection, and repetition) when applied to either

Keywords

formal specification; program verification; software reliability; formal program development; graphical notation; program verification; refinement rules; semantic framework; software reliability; standard compositional operators; stepwise refinement; unimplemented program components; user-friendly; Application software; Computer industry; Computer languages; Education; Educational programs; Logic programming; Programming profession; Reasoning about programs; Refining; Software engineering;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Software and Applications Conference, 1988. COMPSAC 88. Proceedings., Twelfth International

Conference_Location

Chicago, IL

Print_ISBN

0-8186-0873-0

Type

conf

DOI

10.1109/CMPSAC.1988.17151

Filename

17151