An example of proving attribute grammars correct : the representation of arithmetical expressions by DAGs
Ajjm Jos Marcelis · TU/e Research Portal · 1991
The proof system for one-pass attribute grammars is employed to prove the correctness of an example AG in a modular fashion. The AG concerns the translation of arithmetical expressions as they are produced by the underlying CFG into directed acyclic graphs (which are a suitable basis for the generation of efficient code for arithmetical expressions). The entities needed to specify the problem formally are provided within the framework of typed inference systems and relevant properties of these entities are investigated. Such a formalisation is a prerequisite for the application of the proof system. The emphasis is on the proof of the AG, rather than on its derivation. In particular, the exercise exemplifies how the remaining proof obligations for a non-trivial AG, yielded by the proof system, take the shape of a number of clear, logical formulae per production, the proofs of which can be conducted entirely by formal manipulation. The example also shows how such proof obligations can be further split up into elementary parts. This enhances a separation of concerns and results in a number of small proofs to be conducted, most of which are fairly simple and proceed on a nothing else you can basis. Preface: the relation to earlier work The present paper embodies an application of the proof system for one-pass attribute grammars, as described in the first instance in volume 90/07 of this series of Computing Science Notes; see [Mar90]. Since the publication of the latter note, new insights have led to a slight modification of the theory, viz. the explicit inclusion of a reference to derivation trees in the specifications. As a result, the correctness condition for a one-pass AG w.r.t. Q and R cf. section 2.4 of [Mar90] now reads IJd:PTz, i:itz. (Q.d.i => R·d.j·(Fz·d.i» where the types ofQ and Rare PTz --+ itz --+ booC and PTz -> itz --+ stz -> booC, respectively. This correctness condition then generalises in a straightforward way to nonterminals other than start symbol Z, as described in [MargO]. Also the inference rule concerning a production pr of the form Ao(io, so) -> Wo AI(iI,SI) WI,Wn-1 An(in,sn) Wn So = eo , it == el , ... , in :::: en changes slightly, so as to become (cf. [MargO], p. 10) r, f' , d j : PTA, , ... , dn : PTA. , do: PTA, , do =, [Ao --> Ct, (dl , ... ,dn)] I> io : itAo , So : stAo ) ... in : itA .. Sn : stA .. , So =e eO , i1 =e el , ... in =e en qAo·do·io 1 1'J~:(qAi·d;.i; I\TAjdj .ij'sj) => qA.·d •• i. for all k: 1:S k:S n qAo·do·io 1 AJ=l(qAj·dr ij ATAj·dj.ij.$j) ~ TAo·do·io,sQ r , f' I> (pr correct) It is the premiss of this rule that will be used in this paper to serve as a remaining proof obligation for production pro The consistency proof for this inference rule rnns completely analogous to the proof of theorem 4.4 in [Mar90]. The change in the theory described above is the result of still continuing research into the development of proof rules for AGs; as such it will be covered in future work. In the same vein the example dealt with in this paper is to be processed as a part of a more comprehensive treatise later on. Eindhoven, August 1991 Jos MarceJis