Gagallium : Specifying Functions: Two Styles (original) (raw)

In this post, I discuss two approaches to writing formal specifications for (possibly curried) functions of multiple arguments. I refer to these two styles as callee-side reasoning and_caller-side reasoning_. While the former style is very much standard, the latter style is perhaps relatively little known.

Specifying Functions: Two Styles

In OCaml, the definitions let f = fun (x1, x2) -> eand let g = fun x1 -> fun x2 -> e both define functions. The function f is uncurried: it expects one argument, which must be a pair. The function g is_curried_: it expects one argument and returns a function of one argument.

In both cases, the function invocation process is non-atomic. From the moment where the function application f (v1, v2) org v1 v2 begins, until the moment where the function bodye is executed, in a context where the name x1is bound to the value v1 and the name x2 is bound to the value v2, a number of computation steps take place. In the case of the function application f (v1, v2), the pair (v1, v2) is first transmitted to the function; then, this pair is decomposed; and only then is the function body executed. In the case of the function application g v1 v2, the value v1 is first transmitted to the function; then, some kind of nameless function, or closure, is returned; then, the valuev2 is transmitted to this nameless function; and only then is the function body executed.

In either case, the purpose of the function invocation process is to eventually bind the formal parameters x1 andx2 to the actual arguments v1 andv2. However, the details of the process vary. Furthermore, in the case of a curried function, this process can be_interrupted_ in the middle and resumed at a later time, because_partial applications_ are permitted: the function applicationg v1 returns a perfectly valid function of one argument.

How does one describe the behavior of the functions fand g in precise informal prose or in a formal program logic, such as Hoare logic or Separation Logic?

Two distinct approaches emerge, depending on who reasons about the function invocation process: the callee, or the caller?

In the first style, callee-side reasoning, one publishes a specification of the function; whereas in the second style,caller-side reasoning, one publishes a specification of the function’s body.

Callee-Side Reasoning

It may seem more natural to let the callee reason about the function invocation process. Indeed, this process is then analyzed just once, at the function definition site, as opposed to once at each call site. Furthermore, this approach results in more abstract specifications, along the following lines:

In these specifications, the value v remains abstract. It is a runtime representation of a function (presumably a code pointer or some kind of closure), but the caller does not have to know.

This is the most common style.

An upside of this style is its high level of abstraction: functions are viewed as abstract objects.

A downside of this style is that it does not support partial applications in a very natural way. The above specification ofg describes only what happens when g is applied to two values v1 and v2. If one wishes to allow the partial application g v1, then one must write a more complex specification. This is possible, but slightly cumbersome.

Caller-Side Reasoning

The other, less common, approach is to publish a specification of the function’s body, along the following lines:

Then, the functions f and g can be described in a concrete manner, along the following lines:

These are not traditional specifications in the tradition of Floyd and Hoare. Instead of describing the abstract behavior of an application of the functions f or g, they are concrete descriptions of the runtime values that represent the functions f and g.

It is then up to the caller, at each call site, to reason about the function invocation process.

A downside of this style is its lower level of abstraction: functions are viewed as concrete values whose runtime representation is exposed. (For example, whether a function is recursive or not recursive becomes visible.)

An upside of this style is that it naturally offers support for partial applications, without any extra effort. The above specifications expose sufficient information for the caller to reason about a partial application.

Bottom Line

As far as I know, the existence of these two styles is discussed nowhere in the literature. I can see two reasons why this is so: