Where in the toolchain does formal specification come in?

Question

Where is the formal spec located? Like this?

Are tests made from formal or informal spec? I saw a project where they where generated from a the formal spec and that never made sense to me.

Is the verification step manual or can it be automated?

If it is manual, we now have 3 things to maintain and keep in sync. The problem of a possible mismatch between informal spec and code has just been moved between the informal and the formal spec. What did we gain?

If the verification step can be automated completely then why write any code at all? Just let it be generated from the spec automatically. If we fold those two steps into one the situation is the same as before; we have a high level description of our problem which a compiler turns into a low level representation that can be executed by a machine. What did we gain?

Answer 1

Tests can be written based on either a formal spec or an informal spec.

Verification always requires a formal specification. Formal verification might be manual or automated, or some combination of the two; it depends what techniques you use. Typically, it's hard to do completely automatic verification -- it's more usual that verification systems automate part of the verification task, but require some assistance from the programmer (e.g., to specify invariants or prove lemmas that are hard for the automated system to prove). See https://en.wikipedia.org/wiki/Formal_verification for an overview; there are also textbooks that give an overview of formal verification. I suggest reading some standard references on formal verification: they will probably answer a lot of questions you might have.

There's nothing that says you have to have an informal spec, a formal spec, and a program. You could have just a formal spec and a program.

It is often helpful to have specifications at multiple levels of abstraction/granularity, with theorems relating them. Higher-level specs may be easier to understand and specify properties about the whole system or properties we ultimately care about, but may be difficult to prove directly; lower-level specs may be more detailed and harder to work with or understand, but may have a more direct mapping to the program and might facilitate proof/verification.

Higher-level specs might be formal, or in some cases they might be less formal.