18.1 How it works
Before going on into details and syntax, let us give a quick overview
of how that tactic works.
Its behavior is the following: you give a
program annotated with logical assertions and the tactic will generate
a bundle of subgoals, called proof obligations. Then, if you
prove all those proof obligations, you will establish the correctness and the
termination of the program.
The implementation currently supports traditional imperative programs
with references and arrays on arbitrary purely functional datatypes,
local variables, functions with call-by-value and call-by-variable
arguments, and recursive functions.
Although it behaves as an implementation of Floyd-Hoare logic, it is not.
The idea of the underlying mechanism is to translate the imperative
program into a partial proof of a proposition of the kind
" x. P(x)
Þ $(y,v). Q(x,y,v)
where P and Q stand for the pre- and post-conditions of the
program, x and y the variables used and modified by
the program and v its result.
Then this partial proof is given to the tactic Refine
(see 7.2.2, page X), which effect is to generate as many
subgoals as holes in the partial proof term.
The syntax to invoke the tactic is the following:
Correctness ident annotated_program.
Notice that this is not exactly a tactic, since it does not
apply to a goal. To be more rigorous, it is the combination of a
vernacular command (which creates the goal from the annotated program)
and a tactic (which partially solves it, leaving some proof
obligations to the user).
Whereas Correctness is not a tactic, the following syntax is
available:
Correctness ident annotated_program ; tactic.
In that case, the given tactic is applied on any proof
obligation generated by the first command.