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) -> e and 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) or g v1 v2 begins, until the moment where the function body e is executed, in a context where the name x1 is 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 value v2 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 and x2 to the actual arguments v1 and v2. 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 application g v1 returns a perfectly valid function of one argument.

How does one describe the behavior of the functions f and 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:

  • After the definition let f = fun (x1, x2) -> e, the name f is bound to some value v such that, for all values v1 and v2, the application of v to the pair (v1, v2) results in …

  • After the definition let g = fun x1 -> x2 -> e, the name g is bound to some value v such that, for all values v1 and v2, the application of v to the values v1 and v2 result in …

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 of g 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:

  • For all values v1 and v2, if the names x1 and x2 are bound to the values v1 and v2, then the execution of the expression e results in …

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

  • After the definition let f = fun (x1, x2) -> e, the name f is bound to the function fun (x1, x2) -> e.

  • After the definition let g = fun x1 -> x2 -> e, the name g is bound to the function fun x1 -> fun x2 -> e.

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:

  • The distinction between these styles arises only because the function invocation process is not atomic. In a language where n-ary functions are primitive, the function invocation process atomically binds x1 to v1 and x2 to v2. The program logic can take care of reasoning about this step, so neither the callee nor the caller need to reason about it.

  • Caller-side reasoning is less abstract and requires a mixture of Hoare-style reasoning (that is, reasoning in terms of logical assertions) and symbolic execution (that is, reasoning by simulating steps of execution). The tradition and culture of Hoare-style reasoning is so prevalent that this style may seem quite alien to most researchers and practitioners.