A logic for one-pass, one-attributed grammars
Ajjm Jos Marcelis · TU/e Research Portal · 1990
A proof system for one-pass grammars is presented as an extension of a very general logic, with elements from typed A-calculus and natural deduction. In the formulae of the logic, the emphasis is on contexts, which, at all times during a proof or derivation step, explicitly express the environment in which a step must take place. The proof method arrived at is compositional: to prove the correctness of a grammar (w.r.t. a specification), a proof per production rule suffices, where the contexts in which such a proof must be carried out ensure that local information is used only. The proof method is also reminiscent of the Hoare-style of proving programs.