In this chapter we link the stack/triang program with stdlib2 (our internal implementation of malloc/free/exit) instead of with stdlib (which axiomatizes malloc/free/exit as external functions). Both programs use the exact same main.c program:

#include <stddef.h>
#include "stdlib.h"
#include "stack2.h"
#include "triang2.h"

int main(void) {
  return triang(10);
}

and the only difference would be in the Makefile, the Unix ld or cc command would link the programs together with stdlib2.o instead of stdlib.o. The Coq code in this chapter is practically the same as in VSU_main, since the client program (main.c) should be oblivious of private data representations (etc.) of the stdlib module. The only difference is that in some places it says stdlib2 instead of stdlib. In addition, we illustrate a new concept, restrictExports, a more general mechanism than privatizeExports.

The VSU for main

This VSU has the standard preamble:

An alternate way to adjust the Exports of a VSU

Recall that in VSU_main we needed to restrict the Exports list of stacktriangVSU1, to obtain stacktriangVSU. We did this using privatizeExports. But sometimes one also wants to restrict the Exports list in a different way: weaken some of the funspecs using funspec_sub, to provide more abstraction (give the client less information). In this stack+triang+main program, we have no need to do that, but we illustrate the process.

Given a VSU v, restrictExports v Exports' is the type of a new VSU whose Exports list has been replaced by Exports'. The lemma prove_restrictExports says,

• if Exports' does not have any repeated identifiers, and
• if for every (id,fspec') in Exports', there is an (id,fspec) in Exports such that funspec_sub (fspec,fspec'),
• then there is a new VSU whose exports is Exports'.

We will now use this to build stacktriangVSU.

At this point, we must prove funspec_sub for every (id,fspec') in the TriangASI. There is just one, namely triang_spec. So just one bulleted subgoal. And because (in this use of restrictExports) we did not change the funspec between Exports and Exports', we can use funspec_sub_refl to prove it.

For more significant uses of funspec_sub to adapt and abstract VSUs, see: "Verified Software Units", by Lennart Beringer, ESOP'21.

End of digression about restrictExports

The funspec for main is just as it was in VSU_main.

Identical to the proof of body_main in VSU_main.