Technical Reports by Ian Hayes

Most computing languages are highly structured but conventional (flat) grammars do not make that structure explicit. To address this issue, we examine adding block structure to grammars. We allow a production in a grammar to have local productions associated with it. The local productions are accessible only via that production. Local productions for one construct may be nested within local productions for higher level constructs to form a tree-structured hierarchy.

If block structuring is used with an attribute grammar one can also avoid explicit copying of inherited attributes through intermediate nodes in the parse tree that do not modify or make use of the attribute. For example, in the definition of an expression in a programming language grammar one may have an environment attribute that is identical for all nodes in the expression subtree. The explicit passing down of the environment attribute through the intermediate nodes can be avoided by allowing direct reference to the environment attribute of the top-level expression nonterminal.

Keywords: Block structure; attribute grammars; L-attribute grammars; upward remote attributes.

The refinement calculus provides a framework for the stepwise development of imperative programs from specifications. This paper presents a semantics for a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specifications constructs (general predicates and assumptions) and universal quantification. A semantics is defined for this wide-spectrum language based on executions, which are partial functions from states to states, where a state is represented as a set of bindings. This execution semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and a refinement law for introducing recursive procedures is presented.

Keywords: Logic programming, refinement.