The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On Mon, Jan 25, 2021 at 4:39 PM Fritjof <fritjof AT uni-bremen.de> wrote:

Hi,

I have a question regarding what formal specification exactly means in the
proof assistant context.

First *formal verification* means an implementation satisfies its formal specification.
The satisfiability is shown using formal methods of mathematics, e.g., a constructed proof
in Coq.

So we have the following terms:

1) implementation
2) formal specification
3) constructed proofs

In the context of proof assistants, e.g., Coq, I would describe:

1) implementation - as the *program*, collection of function definitions and data types
2) formal specification - as the properties that argue about the program, e.g., theorems, lemmas or axioms
3) constructed proofs - statements of the LTac language

(or any other way to construct proof terms, by the way.)

I agree with your description above.

However, I have also read that the implementation part is referred to as a formal specification:
- https://www.cis.upenn.edu/~bcpierce/papers/pierce-etaps2018.pdf

or the combination of 1,2 and 3 is referred to as a formal specification, like in: a program in haskell
is extracted from this formal specification.

In a stepwise refinement approach (which the DeepSpec project is, to some extent), the implementation of refinement step N is the specification of step N+1. 

 

Maybe code extraction / automatic code generation is not the best example of a refinement step, causing some confusion in terminology.

Hope this helps,

- Xavier Leroy

Am I right, that the term *formal specification* often donetes the combination of 1,2 and 3, or just 1
or am I  missing something?

Kind Regards,
fritjof