## Specifying Functions: Two Styles

- May 12, 2023

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.