ASPECT: an economical bug-detector

Author

Jackson, Daniel

Author_Institution

MIT, Cambridge, MA, USA

fYear

1991

fDate

13-16 May 1991

Firstpage

13

Lastpage

22

Abstract

A technique-ASPECT-for catching code-level bugs is presented. ASPECT is intended to be economical for everyday software development. It comprises a formal specification language and a code-checking method. Programmers write simple assertions about the information required to compute a result; an efficient mechanical checker can then find bugs in the annotated code. Careless slips that escape type-checking and standard compiler anomaly tests can be detected, without the cost of formal verification or the uncertainty of testing. The essence of ASPECT is reasoning about dependencies between the aspects of abstract objects

Keywords

formal specification; program debugging; software engineering; specification languages; ASPECT; abstract objects; annotated code; bug-detector; careless slips; code-checking method; code-level bugs; dependencies; formal specification language; reasoning; software development; Computer bugs; Costs; Error correction codes; Formal specifications; Formal verification; Power generation economics; Programming profession; Specification languages; Testing; Uncertainty;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering, 1991. Proceedings., 13th International Conference on

Conference_Location

Austin, TX

Print_ISBN

0-8186-2140-0

Type

conf

DOI

10.1109/ICSE.1991.130619

Filename

130619