Two-dimensional pinpointing: debugging with formal specifications

1 January 1991

journal article
Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Software

Vol. 8 (1) , 74-84
https://doi.org/10.1109/52.62935

Abstract

Debugging techniques and tools that draw on both the high-level concepts (defined as functions) used in formal specifications and the abstraction and information-hiding constructs used in modern languages are described. The technique is based on two components. One is a novel specification language with support tools. Ada programs are specified with a language that the authors created called Anna. Their tool set is used to check the Ada program's runtime behavior for consistency with the Anna specifications. The other technique uses the tool set to find missing specifications by comparing the specification with program prototypes and to test and debug Ada programs after an accepted specification has been developed. The approach, called two-dimensional pinpointing, locates inconsistencies in software that is structured in levels.<>

Keywords

This publication has 3 references indexed in Scilit:

Formal program construction by transformations-computer-aided, intuition-guided programming
IEEE Transactions on Software Engineering, 1989
ANNA A Language for Annotating Ada Programs
Published by Springer Nature ,1987
An implementation of Anna
ACM SIGAda Ada Letters, 1985