F* IMT Spec: Specification extraction.

The goal is to be able to extract from F*'s types the QCheck properties needed to check the specification.

We need to answer several questions.

Spec extraction

How do we get the pre and post-conditions from an F* signature? The easiest approach would be just to make sure that every function is written as

let foo_pre x = P x
let foo_post y = Q y
val foo : x:T -> Pure T' (requires (foo_pre x)) (ensures foo_post)

Then, extracting the pre and post-conditions is trivial. However, I think this approach might be too tedious, this should be easily automated. Can one generate foo_pre and foo_post directly from foo using Meta-F*? Discussed in #21.

QCheck integration

Having extracted the insertion function pre and post-conditions, we provide handwritten QCheck tests for them. This process should be also automated. Theses tests use manually defined generators, on a following section we discuss the possibility of extracting them.

• Provide QCheck tests for extracted spec.
• Automate the QCheck test generation.

Spec style

What interpretation should we give to refinements on a function's arguments w.r.t its pre-condition. Should we avoid using them?

For now, as explained in #21, we collect all refinements on the arguments' types as part of the pre-condition.

Generators

How will we go about the QCheck generator extraction? How do we make sure that strong pre-conditions don’t render our tests trivial? Should we take this approach?