Title :
Verifiable program construction in a user-friendly style
Author_Institution :
Dept. of Comput. Sci., Stirling Univ.
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;
Conference_Titel :
Computer Software and Applications Conference, 1988. COMPSAC 88. Proceedings., Twelfth International
Conference_Location :
Chicago, IL
Print_ISBN :
0-8186-0873-0
DOI :
10.1109/CMPSAC.1988.17151
