-Lightweight specifications support software maintainability by providing a way to verify that any changes to a code base preserve certain program properties. We give two examples of lightweight specifications for numerical code: units-of-measure types which specify the physical units of numerical quantities in a program; and stencil specifications which describe the pattern of data access used in array computations. Not only can we automatically verify that a program correctly implements these requirements but specifications provide documentation for future developers. Specifications can also be inferred and generated automatically in some cases, further reducing programmer effort. We finish by identifying future potential specification techniques to ease the maintenance and comprehension of scientific code.
Being able to comprehend and easily extend a code base is central to software sustainability; inflexible and inscrutable code is difficult to maintain, adapt, and debug in the future. Frequently the intention of the original programmer is not clear from the code alone. There may be an underlying mathematical model from which the code is derived (e.g., numerical computations in science), but the relationship between the implementation and the model is rarely documented clearly. Programmers often attempt to communicate their original intention by commenting their code, providing informal specifications and descriptions of the program. This approach is often less than perfect: comments must be kept up-to-date with the code they describe and an appropriate level of abstraction must be used to provide effective information (rather than, say, describing each operation line by line).
This informal and manual commenting approach contrasts
with full program specification in which a formal and precise
mathematical description is provided for a program [
We believe lightweight specification and verification provides an intermediate solution. Lightweight specifications describe the behaviour of some aspects of a program, rather than the whole. This reduces the burden on the programmer whilst still aiding comprehension of the program by others. The specification language can be designed to target a higher level of abstraction than the code itself thereby producing useful specifications which are both human- and machine-readable. We advocate for including such lightweight specifications as inline comments in the code so that the usual tool-chain (compilers, IDEs, version control) is unaffected. The usual verification benefits are provided: a program can be checked for conformance to its lightweight specifications, and this also ensures specifications are up-to-date with the code.
We give an example of two such lightweight specification
and verification techniques provided by our tool, CamFort,
for Fortran code base verification. Figure 1 shows an extract
of a Navier-Stokes fluid simulation (based on [
Note that lightweight specifications can be given selectively to
parts of the code as required, rather than being all or nothing.
CamFort has four modes of interaction with specifications:
!= stencil readOnce, backward(depth=1, dim=1) *
,! reflexive(dim=2) :: f
!= stencil readOnce, backward(depth=1, dim=2) *
,! reflexive(dim=1) :: g
do i = 1, imax
do j = 1, jmax
if (iand(flag(i,j), cf))
rhs(i,j) = ((f(i,j) - f(i-1,j)) / delx +
,! (g(i,j) - g(i,j-1)) / dely)
,! / del_t
end do; end do
2) inference: CamFort can infer specifications automatically,
giving useful information and reducing programmer effort.
For units-of-measure, a programmer need not specify the
units for each variable. For example, the unit specification
for rhs on line 10 need not be given. In infer mode,
CamFort infers and reports the units of all variables (whether
they have been given an explicit specification of not). For
stencil specifications, CamFort can infer specifications of
the shape of a large class of regular array access patterns.
3) synthesis: based on the above inference, CamFort can
further reduce programmer effort by inserting automatically
inferred specifications into the code where relevant. For
example, the specifications on lines 16, 17 can be inferred
and synthesised by CamFort entirely automatically without
any programmer effort.
4) suggestion: (just for units), CamFort can suggest a subset
of program variables that if given a specification manually
by the programmer provides enough information to
CamFort to infer the units-of-measure for all other variables.
The inference, synthesis, and suggestion features of CamFort
further support the lightweight nature of the specifications. In
a previous study, we sought to measure how much CamFort
reduces programmer effort via the inference and synthesis of
unit specifications [
For the full Navier-Stokes code, of which Figure 1 above
gave an excerpt, the latest version of CamFort suggests that
only 79 of the 262 variable declarations actually require a
usergiven specification to infer and synthesise units-of-measure for
the rest of the variables: a 70% saving in effort compared with
manually specifying the units of every variable [
Note that specifications can be declared once, given a name, and reused many times, further reducing effort.
There are a variety of directions to explore for future
specifications. We give three examples that we are exploring.
1) Software contracts such as pre- and post-conditions,
assertions, and loop invariants can be added to check expected
ranges of values and program behaviour. Techniques for
inferring contracts are available [
Lightweight specifications aid software maintainability and
reuse by providing high-level information to other developers
about the intention of the code. Automatically verifying their
correctness ensures that the code remains up-to-date with the
specification and can provide confidence in changes made
by new developers. Our open-source tool CamFort1 provides
implementations of stencil and units-of-measure specifications
(see [
This work was supported by the Engineering and Physical Sciences Research Council (EP/M026124/1).