Premium
A correctness proof of an indenting program
Author(s) -
Mateti Prabhaker,
Jaffar Joxan
Publication year - 1983
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/spe.4380130302
Subject(s) - correctness , mathematical proof , rigour , computer science , pascal (unit) , programming language , calculus (dental) , mathematics , medicine , geometry , dentistry
The correctness of an indenting program for Pascal is proved at an intermediate level of rigour. The specifications of the program are given in the companion paper. 1 The program is approximately 330 lines long and consists of four modules: io, lex, stack and indent . We prove first that the individual procedures contained in these modules meet their specifications as given by the entry and exit assertions. A global proof of the main routine then establishes that the interaction between modules is such that the main routine meets the specification of the entire program. We argue that correctness proofs at the level of rigour used here serve very well to transfer one's understanding of a program to others. We believe proofs at this level should become commonplace before more formal proofs can take over to reduce traditional testing to an inconsequential place.