VSU_introIntroduction to Verified Software Units
Looking back: single-module programs
Next: modular verification of modular programs
- is implemented in one or more .c files;
- exports some set of functions (an API) described in a .h file
- (perhaps) has some private functions that are not exported
- imports from other modules, various sets of functions described in .h files
- (perhaps) manipulates data structures whose representations should be kept private from client modules
- (perhaps) has global variables of its own that (perhaps) other modules should not directly manipulate
- in part because a single "module" may be implemented in more than one .c file, to which the static keyword does not generalize;
- in part because we will use Verifiable C's "VSU" facility to enforce this kind of locality.
- Model_stack.v, the functional model, just in the sense that hash.v is the functional model for our hash table. But the functional model for stacks is so simple -- just Coq lists -- that we will merge that into Spec_stack.v.
- Spec_stack.v, the API specification of the stack module. This is the one that clients import; it contains (for example) funspecs and the names of abstract data types (ADTs). The important thing is that it contains nothing about the implementation of the function bodies, or the representations of ADTs, or any mention of internal functions that are not meant to be exported through the API.
- VSU_stack.v is the proof that the implementation of the stack module, stack.c, correctly implements the API spec in Spec_stack.v.
A Stack/Triang program to verify
stdlib.h
#include <stddef.h> extern void * malloc (size_t n); extern void free (void *p); extern void exit(int n);
stack2.h
struct stack; struct stack *newstack(void); void push (struct stack *p, int i); int pop (struct stack *p);
triang2.h
int triang (int n);
main2.c
#include "triang2.h" int main(void) { return triang(10); }
Let's verify!
And with that preamble, you can move on to the next chapter, Spec_stack.Warning
Next Chapter: Spec_stack
(* 2023-03-25 11:30 *)