Yet another Imp variant, this time with types! Regular Imp has distinct syntax for boolean and arithmetic expressions, where only arithmetic expressions can contain variables.

     Inductive aexp := ... | Var : x -> aexp | ...
     Inductive bexp := ...

The goal of this case study is to

• collapse the two grammars into a single type exp
• allow variables to range over both booleans and naturals, and
• introduce types to keep things straight.

Soundness for Typed Imp (TImp) is a good example of a realistic conditional property, requiring custom generators for effective testing.

Identifiers, Types and Contexts

For the type of identifiers of TImp we will use a wrapper around plain natural numbers.

We will need one identifier-specific operation, fresh: given any finite set of identifiers, we can produce one that is distinct from all other identifiers in the set. To compute a fresh id given a list of ids we can just produce the number that is 1 larger than the maximum element:

We will also need a way of testing for equality, which we can derive with the standard dec_eq tactic.

Identifier Printing and Generation

One advantage of using natural numbers as identifiers is that we can take advantage of the Show instance of nat to print them.

To generate identifiers for TImp, we will not just generate arbitrary natural numbers. More often than not, we will need to generate a set of identifiers, or pick an identifier from such a set. If we represent a set as a list, we can do the former with a recursive function that generates n fresh nats starting from the empty list. For the latter, we have QuickChick's elems_ combinator.

Types

Here is the type of TImp types:

To use ty in testing, we will need Arbitrary, Show, and Dec instances. Instead of writing tedious manual instances for simple inductive types like ty, nat, etc., we can use QuickChick's automatic derivation mechanism.

Decidable equality instances are not yet derived fully automatically by QuickChick. However, the boilerplate we have to write is largely straightforward. As we saw in the previous chapters, Dec is a typeclass wrapper around ssreflect's decidable and we can use the dec_eq tactic to automate the process.

List-Based Maps

To encode typing environments (and, later on, states), we will need maps from identifiers to values. Why not just use the Logical Foundations version? Because it uses a function-based representation. For testing, we need to

• access the domain of the map,
• test the map for equality, and
• iterate through the map.

These are awkward for the functional representation.

Instead we're going to use a list-based representation. The operations we need are:

• empty : To create the empty map.
• get : To look up the binding of an element, if any.
• set : To update the binding of an element.
• dom : To get the list of keys in the map.

The implementation of a map is a simple association list. If a list contains multiple tuples with the same key, then the binding of the key in the map is the one that appears first in the list; that is, later bindings can be shadowed.

The empty map is the empty list.

To get the binding of an identifier x, we just need to walk through the list and find the first cons cell where the key is equal to x, if any.

To set the binding of an identifier, we just need to cons it at the front of the list.

Finally, the domain of a map is just the set of its keys.

We next introduce a simple inductive relation, bound_to m x a, that holds precisely when the binding of some identifier x is equal to a in m

We can now decide whether bound_to m x a holds for any m, x and a (the proof details are elided):

Contexts

Typing contexts in TImp are just maps from identifiers to types.

Given a context Gamma and a type T, we can try to generate a random identifier whose binding in Gamma is T. We use List.filter to extract all of the elements in Gamma whose type is equal to T and then, for each (a,T') that remains, return the name a. We use the oneOf_ combinator to pick an generator from this list at random. Since the filtered list might be empty we return an option, we use ret None as the default element for oneOf_.

We also need to generate typing contexts. Given some natural number n to serve as the size of the context:

• Create its domain (n fresh identifiers)
• Create n arbitrary types
• Zip them together

Expressions

We are now ready to introduce the syntax of expressions in TImp. The original Imp had two distinct types of expressions, arithmetic and boolean expressions; variables were only allowed to range over natural numbers. In TImp, we extend variables to range over boolean values as well, and we collapse expressions into a single type exp.

Typed Expressions

While the typing relation is almost entirely standard, there is a choice to make about the Ty_Eq rule. The Ty_Eq constructor above requires that the arguments to an equality check are both arithmetic expressions (just like it was in Imp), which simplifies some of the discussion in the remainder of the chapter. We could have allowed for equality checks between booleans as well - that will become an exercise at the end of this chapter.

Typing in TImp is decidable: given an expression e, a context Gamma and a type T, we can decide whether has_type Gamma e T holds.

Generating Typed Expressions

Instead of generating expressions and filtering them using has_type, we can be smarter and generate well-typed expressions for a given context directly. It is common for conditional generators to return options, allowing the possibility of failure if a wrong choice is made internally. For example, if we wanted to generate an expression of type TNat and chose to try to do so by generating a variable, then we might not be able to finish (if the context is empty or only binds booleans). To chain together two generators with types of the form G (option ...), we need to execute the first generator, match on its result, and, when it is a Some, apply the second generator.

This pattern is common enough that QuickChick introduces explicit monadic notations.

    GOpt = fun A : Type => G (option A)
         : Type -> Type

    Monad_GOpt
         : Monad GOpt

This brings us to our first interesting generator -- one for typed expressions. We assume that Gamma and T are inputs to the generation process. We also use a size parameter to control the depth of generated expressions (i.e., we'll define a sized generator). Let's start with a much smaller relation: has_type_1 (which consists of just the first constructor of has_type), to demonstrate how to build up complex generators for typed expressions from smaller parts.

To generate e such that has_type Gamma e T holds, we need to pick one of its constructors (there is only one choice, here) and then try to satisfy its preconditions by generating more things. To satisfy Ty_Var (given Gamma and T), we need to generate x such that bound_to Gamma x T. But we already have such a generator! We just need to wrap it in an EVar.

(Note that this is the ret of the GOpt monad.)

Now let's consider an extended typing relation, extending the previous one with all of the constructors of has_type that do not recursively require has_type as a side-condition. These will be the base cases for our final generator.

We can already generate values satisfying Ty_Var using gen_typed_evar. For the rest of the rules, we will need to pattern match on the input T, since Ty_Num can only be used if T = TNat, while Ty_True and Ty_False can only be used if T = TBool.

We now need to go from a list of (optional) generators to a single generator. We could do that using the oneOf combinator (which chooses uniformly), or the freq combinator (by adding weights). Instead, we introduce a new one, called backtrack:
       backtrack : list (nat × GOpt ?A) → GOpt ?A Just like freq, backtrack selects one of the generators according to the input weights. Unlike freq, if the chosen generator fails (i.e. produces None), backtrack will discard it, choose another, and keep going until one succeeds or all possibilities are exhausted. Our base-case generator could then be like this:

To see how we handle recursive rules, let's consider a third sub-relation, has_type_3, with just variables and addition:

Typing derivations involving EPlus nodes are binary trees, so we need to add a size parameter to enforce termination. The base case (Ty_Var3) is handled using gen_typed_evar just like before. The non-base case can choose between trying to generate Ty_Var3 and trying to generate Ty_Plus3. For the latter, the input type T must be TNat, otherwise it is not applicable. Once again, this leads to a match on T:

Putting all this together, we get the full generator for well-typed expressions.

When writing such complex generators, it's good to have some tests to verify that we are generating what we expect. For example, here we would expect gen_exp_typed_sized to always return expressions that are well typed. We can use forAll to encode such a property.

Values and States

In the original Imp language from Logical Foundations, variables ranged over natural numbers, so states were just maps from identifiers to nat. Since we now want to extend this to also include booleans, we need a type of values that includes both.

We can also quickly define a typing relation for values, a Dec instance for it, and a generator for values of a given type.

States in TImp are just maps from identifiers to values

We introduce an inductive relation that specifies when a state is well typed in a context (that is, when all of its variables are mapped to values of appropriate types). We encode this in an element-by-element style inductive relation: empty states are only well typed with respect to an empty context, while non-empty states need to map their head identifier to a value of the appropriate type (and their tail must similarly be well typed).

Evaluation

The evaluation function takes a state and an expression and returns an optional value, which can be None if the expression encounters a dynamic type error like trying to perform addition on a boolean.

We will see in a later chapter (QuickChickTool) how we can use QuickChick to introduce such mutations and have them automatically checked.

Type soundness states that, if we have an expression e of a given type T as well as a well-typed state st, then evaluating e in st will never fail.

To test this property, we construct an appropriate checker:

     ===>
       QuickChecking expression_soundness_exec
       [(1,TNat), (2,TNat), (3,TBool), (4,TNat)]
       [(1,VNat 0), (2,VNat 0), (3,VBool true), (4,VNat 0)]
       TBool
       Some EAnd (EAnd (EEq (EVar 4) (EVar 1)) (EEq (ENum 0) (EVar 4))) EFalse
       *** Failed after 8 tests and 0 shrinks. (0 discards)

Where is the bug?? Looks like we need some shrinking!

Shrinking for Expressions

Let's see what happens if we use the default shrinker for expressions carelessly.

     ===>
       QuickChecking expression_soundness_exec_firsttry
       [(1,TBool), (2,TNat), (3,TBool), (4,TBool)]
       [(1,VBool false), (2,VNat 0), (3,VBool true), (4,VBool false)]
       TBool
       Some EAnd (ENum 0) ETrue
       *** Failed after 28 tests and 7 shrinks. (0 discards)

The expression shrank to something ill-typed! Since it causes the checker to fail, QuickChick views this as a succesfull shrink, even though this could not actually be produced by our generator and doesn't satisfy our preconditions! One solution would be to check the preconditions in the Checker, filtering out shrinks. But that would be inefficient.

We not only need to shrink expressions, we need to shrink them so that their type is preserved! To accomplish this, we need to intuitively follow the opposite of the procedure we did for generators: look at a typing derivation and see what parts of it we can shrink to while maintaining their types so that the type of the entire thing is preserved. As in the case of gen_exp_typed, we are going to build up the full shrinker in steps. Let's begin with shrinking constants.

• If e = ENum x for some x, all we can do is try to shrink x.
• If e = ETrue or e = EFalse, we could shrink it to the other. But remember, we don't want to do both, as this would lead to an infinite loop in shrinking! We choose to shrink EFalse to ETrue.

The next case, EVar, must take the type T to be preserved into account. To shrink an EVar we could try shrinking the inner identifier, but shrinking an identifier by shrinking its natural number representation makes little sense. Better, we can try to shrink the EVar to a constant of the appropriate type.

Finally, we need to be able to shrink the recursive cases. Consider EPlus e₁ e₂:

• We could try (recursively) shrinking e₁ or e₂ preserving their TNat type.
• We could try to shrink directly to e₁ or e₂ since their type is the same as EPlus e₁ e₂.

On the other hand, consider EEq e₁ e₂:

• Again, we could recursively shrink e₁ or e₂.
• But we can't shrink to e₁ or e₂ since they are of a different type.
• For faster shrinking, we can also try to shrink such expressions to boolean constants directly.

Putting it all together yields the following smart shrinker:

As we saw for generators, we can also perform sanity checks on our shrinkers. Here, when the shrinker is applied to an expression of a given type, all of its results should have the same type.

Back to Soundness

To lift the shrinker to optional expressions, QuickChick provides the following function.

Armed with shrinking, we can pinpoint the bug in the EAnd branch of the evaluator.

     ===>
        QuickChecking expression_soundness_exec'
        [(1,TNat), (2,TNat), (3,TNat), (4,TBool)]
        [(1,VNat 0), (2,VNat 0), (3,VNat 0), (4,VBool false)]
        TBool
        Some EAnd ETrue ETrue
        *** Failed after 8 tests and 1 shrinks. (0 discards)

Well-Typed Programs

Now we're ready to introduce TImp commands; they are just like the ones in Imp.

(Of course, the derived Show instance is not going to use these notations!)

We can now define what it means for a command to be well typed for a given context. The interesting cases are TAsgn and TIf/TWhile. The first one, ensures that the type of the variable we are assigning to is the same as that of the expression. The latter, requires that the conditional is indeed a boolean expression.

Now, here is a brute-force decision procedure for the typing relation (which amounts to a simple typechecker).

To complete the tour of testing for TImp, here is a (buggy??) evaluation function for commands given a state. To ensure termination, we've included a "fuel" parameter: if it gets to zero we return OutOfGas, signifying that we're not sure if evaluation would have succeeded, failed, or diverged if we'd gone on evaluating.

Type soundness: well-typed commands never fail.

Exercise: 4 stars, standard (well_typed_state_never_stuck)

Write a checker for the above property, find any bugs, and fix them.

Exercise: 4 stars, standard (ty_eq_polymorphic)

In the has_type relation we allowed equality checks between only arithmetic expressions. Introduce an additional typing rule that allows for equality checks between booleans.
    | Ty_Eq : ∀ Gamma e₁ e₂,
        Gamma |⊢ e₁ \IN TBool → Gamma |⊢ e₂ \IN TBool →
        Gamma |⊢ EEq e₁ e₂ \IN TBool Make sure you also update the evaluation relation to compare boolean values. Update the generators and shrinkers accordingly to find counterexamples to the buggy properties above. HINT: When updating the shrinker, you will need to come up with the type of the equated expressions. The Dec instance of has_type will come in handy.

Automation (Revisited)

QuickChick is under very active development. Our vision is that it should automate most of the tedious parts of testing, while retaining full customizability. We close this case study with a brief demo of some things it can do now. Recall the has_type_value property and its corresponding generator:
  Inductive has_type_value : value → ty → Prop :=
    | TyVNat : ∀ n, has_type_value (VNat n) TNat
    | TyVBool : ∀ b, has_type_value (VBool b) TBool.

  Definition gen_typed_value (T : ty) : G value :=
    match T with
    | TNat ⇒ n <- arbitrary;; ret (VNat n)
    | TBool ⇒ b <- arbitrary;; ret (VBool b)
    end. QuickChick includes a derivation mechanism that can automatically produce such generators -- i.e., generators for data structures satisfying inductively defined properties!

===> GenSizedSuchThathas_type_value is defined.

Let's take a closer look at what is being generated (after doing some renaming and reformatting).

     ===>
       GenSizedSuchThathas_type_value = fun T : ty =>
       {| arbitrarySizeST :=
          let fix aux_arb (size0 : nat) (T : ty) {struct size0}
                : G (option value) :=
            match size0 with
            | 0 => backtrack [(1, match T with
                                  | TBool => ret None
                                  | TNat => n <- arbitrary;;
                                            ret (Some (VNat n))
                                  end)
                             ;(1, match T with
                                  | TBool => b <- arbitrary;;
                                             ret (Some (VBool b)))
                                  | TNat => ret None
                                  end)]
            | S _ => backtrack [(1, match T with
                                    | TBool => ret None
                                    | TNat => n <- arbitrary;;
                                              ret (Some (VNat n))
                                    end)
                               ;(1, match T with
                                    | TBool => b <- arbitrary;;
                                               ret (Some (VBool b)))
                                    | TNat => ret None
                                    end)]
            end in
            fun size0 : nat => aux_arb size0 T |}

       : forall T : ty,
           GenSizedSuchThat value
               (fun v => has_type_value v T)

This is a rather more verbose version of the gen_typed_value generator, but the end result is actually exactly the same distribution!

(More) Typeclasses for Generation

QuickChick provides typeclasses for automating the generation for data satisfying predicates.

A variant that takes a size,...

...an unsized variant,...

...convenient notation,...

...and a coercion between the two:

Using "SuchThat" Typeclasses

QuickChick can now (ab)use the typeclass resolution mechanism to perform a bit of black magic:

  ==>
    QuickChecking conditional_prop_example
    +++ Passed 10000 tests (0 discards)

Notice the "0 discards": that means that quickchick is using generators that produce x and y such that x = y!

Acknowledgements

The first version of this material was developed in collaboration with Nicolas Koh.