Using off-the-shelf formal methods to verify attribute grammar properties

Shirley Goldrei*, Anthony Sloane

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

Abstract

Attribute Grammars are the specification language of many tools that automatically generate programming language implementations. We consider the problem of verifying properties of attribute grammar specifications, particularly properties that are not well supported by existing tools. Rather than propose methods for extending existing tool implementation techniques, we propose the use of off-the-shelf formal methods tools as the basis for attribute grammar verification. Off-the-shelf tools can provide significant expressive power at a much lower cost than extending an existing evaluator generator. As a specific example, we describe how to use the Alloy model finding and checking tool to verify properties of remote attribution constructs in the LIDO attribute grammar specification language. A naive application of this approach has significant performance overheads; we discuss techniques for limiting the scope of the problems that are solved to make the approach tractable.

Original languageEnglish
Pages (from-to)33-54
Number of pages22
JournalElectronic Notes in Theoretical Computer Science
Volume110
DOIs
Publication statusPublished - 31 Dec 2004

Keywords

  • attribute grammars
  • compiler generation
  • formal methods
  • software verification

Fingerprint Dive into the research topics of 'Using off-the-shelf formal methods to verify attribute grammar properties'. Together they form a unique fingerprint.

Cite this