Is There Hypothesis for Attribute Grammars?

Software testing is a vital activity in the development life cycle of software systems. In fact, most programming languages and paradigms offer powerful testing frameworks to evaluate and improve the quality of software systems. In the context of software language engineering, Knuth introduced attribute grammars as a powerful programming paradigm for specifying the static semantics of languages. However, their expressiveness has extended their use to various other domains, such as to express complex multiple traversal tree-based algorithms, to specify advanced type inference algorithms, to elegantly implement pretty printing functions, to strictify lazy circular functions, etc.

Surprisingly, no attribute grammar-based system provides a testing framework. In this paper, we incorporate property-based testing, expressed via the Hypothesis system, in the pyZtrategic attribute grammar-based system [15]: a combined embedding of attribute grammars and strategic term rewriting defined in Python. As a result, we provide an advanced mechanism for attribute grammar writers to test their specifications by defining properties on attributes. Strategic term rewriting is a key component of our approach: attribute properties are tested on all attribute instances of an abstract syntax tree through strategic functions. Moreover, we use the generator mechanism provided by Hypothesis to automate the generation of test cases, i.e., abstract syntax trees. To validate the proposed technique, we consider an attribute grammar expressing advanced scope rules of a block structured language, and we show several properties defined over its attributes.

This section includes a brief introduction to attribute grammars, property-based testing, and strategic term rewriting. We will present these techniques in the Python language, in which we specify a powerful combined embedding of these three domain-specific techniques.

Before we present each of these powerful programming techniques, we start by presenting a simple but motivating example that we will use throughout the paper. Consider the well-known Repmin program. The goal of this program is to transform a binary leaf tree¹¹1A tree that stores its values in the leaves. of integers into a new tree with the exact same shape but in which all leaves have been replaced by the minimum leaf value of the original tree.

To model such a binary tree, we consider the following Python algebraic data type:

Leaf and Fork are data type constructors, which are functions used to construct instances of binary leaf trees of type Tree. For example, we can define a tree, $t_1$, in Python as follows:

Next, we define the recursive function tmin to compute a tree’s minimum value. Note that, while Python is not a typed language, it allows type annotations which we add to make functions more readable.

Where min computes the minimum of two given numbers. Similarly, we can express the recursive function replace, which places a given concrete value in all leaves of a tree:

Now, we combine functions replace and tmin to obtain a simple solution to Repmin:

Regarding this implementation, the underlying tree t is traversed twice: once to compute the minimum value and a second time to replace the value stored in the leaves by the computed minimum. In fact, there are two recursive functions with t as argument.

Combining property-based testing systems with attribute grammar systems is not straightforward. This challenge arises because properties are typically expressed in general-purpose programming languages, rather than in the domain-specific languages used by AG systems. One possible solution would be to extend the AG DSL to support PbT. However, this would require developing a new PbT framework specifically designed for AGs, which would also need to be integrated into the attribute evaluators’ functions. It should be noticed that in Section 2.2 we expressed properties on the Repmin program that can be seen as the attribute evaluator that an AG system would generate from the Repmin AG shown in Section 2.1. However, the Python code was manually written, rather than being produced by an AG system. Of course, programmers should write properties on the code/specification they write and not on generated code. In fact, the evaluators generated from AG systems, defining real language engineering problems, are complex and difficult to understand.

To integrate attribute grammars and property-based testing, we propose a novel methodology that incorporates the following techniques:

• $\mathrm{■}$

  First, we propose a novel embedding of attribute grammars and strategic term rewriting in the Python programming language, as provided by the pyZtrategic library [15]. pyZtrategic offers an shallow Embedded Domain-Specific Language (EDSL) that enables AGs and strategic term rewriting to be specified directly as regular Python programs. In this setting, the Embedded Attribute Grammar (EAG) is an executable Python program: given an AST it computes the values of its attribute instances.

• $\mathrm{■}$

  Second, properties are expressed directly on the attributes of the AG using the Hypothesis library. Since AGs are embedded in Python, properties have direct access to these attributes. As a result, writing properties for AG attributes closely resembles defining properties for regular Python programs.

• $\mathrm{■}$

  Third, property-based testing systems include mechanisms for the automatic generation of (many) random inputs to validate properties. Hypothesis is no exception. Thus, we will rely on such Hypothesis generators to produce ASTs and then check that properties on attributes instances hold for all the ASTs decorated by the Python EAG.

• $\mathrm{■}$

  Finally, we rely on strategic programming to apply these properties to all instances of attributes in a given decorated abstract syntax tree⁵⁵5A decorated AST is a tree in which the values of all attribute instances have been computed..

Names serve to identify program entities such as variables, functions, types, and modules, enabling these entities to be referenced throughout a program. Name resolution determines the association between each reference and its corresponding declaration(s) based on the language’s scope rules. Specification of such scope rules is often complicated because it cuts across the local inductive structure of programs (as described by an abstract syntax tree). For example, the name introduced by a let node in an AST representing a functional program may be referenced by a node arbitrarily distant from its declaration. Attribute grammars offer a powerful way to define complex scope rules in a structured and declarative setting. In fact, name analysis played a foundational role in Donald Knuth’s pioneering work on AGs [9].

To express the scope rules of programming languages, we will consider the (sub)language of let expressions as incorporated in most functional languages, such as Haskell. Although being a concise example, the Let language holds the central characteristics of programming languages, such as (nested) block-based structures and mandatory but unique name declarations. In addition, the semantics of Let does not force a declare-before-use discipline, meaning that a variable can be declared after its first use. The following is an example of a program in the Let language, which corresponds to the correct Haskell code.

This expression evaluates to 28. Usually, Let expressions allow nesting which complicates the scope rules: nested let expressions inherit the context (i.e., declared names) of their outermost ones, where nested declarations hide outer ones. Next, we show an example where the nested declaration of the name a hides its outer declaration.

The Let language does not force a declare-before-use discipline: This is the case in the first use of c: it refers to its (later) definitions in the outermost block. Note that nested Let defines a second name a. Consequently, the use of name a (in the in part of the nested let) refers to the inner definition and not to the outer definition. However, in a let block, a name may be declared once, at most. So, the second definition of the identifier a in the outermost block is invalid. Furthermore, the Let language requires that only defined names may be used. As a result, the applied occurrence of w is invalid, since w has no binding occurrence at all. Unused names, such as b, are not errors, although, they represent dead code.

We aim to develop a program that analyzes Let programs and generates a list of identifiers that violate the language’s scope rules. To simplify identifying incorrectly used names in a Let program, we require that the list of invalid identifiers follows the sequential structure of the input program. Thus, the semantic meaning of processing this sentence is [b,w,a].

A conventional implementation of the required analysis naturally leads to a program that traverses each block twice: once for accumulating the declarations of names and constructing an environment and a second time to process the uses of names (using the computed environment) in order to check for the use of undeclared identifiers. The uniqueness of identifiers is checked in the first traversal: for each newly encountered identifier

As annotated in the Let program ex (using Haskell comments), the outermost let block is context-free. It begins by accumulating the declared names in an empty list of declarations (dcli in the comment labelled 1). This accumulated list forms the environment of the outer let (dclo in comment 2). For a nested Let, the initial context – its starting list of declarations – is the total environment of the enclosing Let (see dcli in comment 3). To distinguish declarations with the same name at different nesting levels, we pair each name with its corresponding level.

In such a straightforward algorithm, semantic errors caused by duplicate definitions are detected during the first traversal, whereas errors due to missing declarations are identified in the second traversal. Consequently, errors found in the first traversal must be explicitly passed to the second.⁸⁸8This is typically achieved by using intrusive code into the implementation of scope rules – either by storing values directly in the AST (as a side effect in imperative programming) or by using gluing data structures to pass such values between traversal functions (as required in a purely functional setting) [17] Additionally, scheduling the traversal functions is complex: the first traversal of inner blocks can only begin during the second traversal of the outer block. As a result, the traversal functions become intertwined. In the elegant style of AG programming, the grammar writer neither needs to schedule complex traversal functions nor rely on additional mechanisms to pass information between traversals. The AG system automatically infers these traversals and produces the necessary mechanisms to convey information between traversal functions.

Next, we show the visual representation of the AG that specifies the scope rules of the Let language.⁹⁹9Due to space limitations we omit here its definition as a Python EAG.

In these attribute equations, we can see that attributes dcli (inherited) and dclo (synthesized) are used to define an accumulator: it starts at the root as the empty list, and at Assign and Nested productions, the Name is added to that list. The inherited attribute env is used to pass downwards the accumulated list as the environment. It should be noticed that at NestedLet productions, such environment (env) is copied to the initial list of declarations of the nested let (attribute dcli). In the nested Let the environment env is the accumulated list of declarations of the same Let (attribute dclo). Having expressed this non-trivial scope rules in the elegant AG formalism, we now write several properties to test our specification.

1. 1.

   Property stating that every declared name needs to be in the environment:

   ⬇

   def checkOneDeclared(t: Lets, z: Zipper[Lets]) -> list[bool]:

   match t:

   case Assign(x, _, _) | NestedLet(x, _, _): return [mBIn(x, env(z))]

   case _ : return []

   def testDeclaredNames(i):

   assert all(st.full_tdTU(lambda x: st.adhocTUZ(st.failTU, checkOneDeclared, x), obj(i)))

   Where mBIn is a simple lookup function that returns true if the name (its first argument) is in the environment env (its second argument). The property is applied to all Assign and NestedLet nodes/productions using a full top-down strategy. The property holds if it is true in all nodes.

2. 2.

   Property stating that every declared name must not be in the accumulated environment thus far. This would correspond to a duplicated declaration.

   ⬇

   def checkOneDeclaredDcli(t: Lets, z: Zipper[Lets]) -> list[bool]:

   match t:

   case Assign(x, _, _) | NestedLet(x, _, _): return [mNBIn((x, lev(z)), dcli(z))]

   case _ : return []

   def testDeclaredNamesDcli(i):

   assert all(st.full_tdTU(lambda x: st.adhocTUZ(st.failTU, checkOneDeclaredDcli, x), obj(i)))

   Where mNBIn checks whether a given name already exists at the same nested level (given by attribute lev) in the accumulated list of declarations dcli.

3. 3.

   Property stating that the initial list of declarations of a nested Let is a subset of the total environment of its outer one:

   ⬇

   def checkNested(t: Lets, z: Zipper[Lets]) -> list[bool]:

   match t:

   case NestedLet(_, _, _): return [isSubset(dcli(z.z_dollar(2)), env(z.z_dollar(2)))]

   case _ : return []

   def testNested(i):

   assert all(st.full_tdTU(lambda x: st.adhocTUZ(st.failTU, checkNested, x), obj(i)))

   In all NestedLet nodes, the initial list of declarations (attribute dcli) of a nested Let (the second child of production/constructor NestedLet) is a subset of the total list of declarations (attribute dclo) of that same child.

4. 4.

   Property that states that every declared name is not dead:

   ⬇

   def checkOneDead(t: Lets, z: Zipper[Lets]) -> list[bool]:

   return [dead(z)]

   def testDeadCode(i):

   assert allFalse(st.full_tdTU(lambda x: st.adhocTUZ(st.failTU, checkOneDead, x), obj(i)))

   Where dead is an attribute that checks whether a name declaration is unused.

5. 5.

   A property that checks whether an optimization preserves the semantics of Let programs. In [15] we have expressed the optimization of arithmetic expressions (simplifying multiplication by zero/one, etc) as the innermost strategic function opt. The evaluation of a Let program is synthesized by attribute eval. Thus we write a property that checks if the original AST is equal to the value of the transformed AST.

   ⬇

   def testEvalInOpt(ast):

   assert eval(obj(ast)) == eval(opt(obj(ast)))

   This property shows the expressiveness of our approach: It is defined on attributes (eval) of the original AST and the AST produced by a strategic-based function (opt).

This paper presents a technique for expressing property-based testing within the attribute grammar formalism. We combined a Python embedding of attribute grammars with the property-based testing framework Hypothesis. In this embedding, AGs are written directly as Python functions, allowing Hypothesis properties to be expressed directly on attributes. Strategic term rewriting is a key component of our approach: attribute properties are tested on all attribute instances of an abstract syntax tree through strategic functions. To demonstrate the expressiveness of our technique, we presented several properties to test the scope rules of a modern block-structured Let language, as commonly found in many (functional) languages.