A specification schema for indenting programs
作者:
Prabhaker Mateti,
期刊:
Software: Practice and Experience
(WILEY Available online 1983)
卷期:
Volume 13,
issue 2
页码: 163-179
ISSN:0038-0644
年代: 1983
DOI:10.1002/spe.4380130206
出版商: John Wiley&Sons, Ltd.
关键词: Functional specifications;Correctness proofs;Pretty‐printing;Pascal
数据来源: WILEY
摘要:
AbstractA two level specification of the functional behaviour of a class of indenting programs for Pascal is presented. The transformation that these programs perform on the input text is a composition of splitting input lines, altering the blank space between lexical tokens and computing the margin required in front of each of the split lines. The high level specification is given as a stylized Pascal grammar in Extended BNF. In contrast, the low level specifications, which are operationally closer to a program, and which define how syntactically invalid text is dealt with, require several mathematical functions that capture the essence of these basic transformations. The specifications of an indenting program for Pascal are then obtained as a further elaboration of these functions. Most indentation styles appearing in the literature can be specified with precision using methods developed in this paper. Our experience in this case study indicates that although specifications for real‐life programs can be given using simple mathematics, the effort required is still considerabl
点击下载:
PDF
(946KB)
返 回