2
$\begingroup$

enter image description here

Where is the formal spec located? Like this? enter image description here

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?

$\endgroup$
  • 1
    $\begingroup$ If you'd generate programs from formal specs, what would you need tests for? (Dummy control, I know...) $\endgroup$ – Raphael Aug 17 '16 at 19:42
  • $\begingroup$ It is customary that the programmers and the QA team work independently from the informal spec. If two teams independently arrive at the same conclusions from the spec it is at least a hint that they have understood the information in the document correctly. Test make sense even if you have formal spec. What doesn't make sense IMHO is producing the tests from the infomal spec. $\endgroup$ – Joe Dohn Aug 18 '16 at 8:04
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks a lot for your elaborate answer. I understand that there are lots of possibilites. Having multiple specifications sounds horrible from a practical point of view. I still don't get what the advantage of a formal spec is at all - why not just have a program. If our problem is formulated in a programming language powerful enough the program is the proof and in addition we have a single point of truth. $\endgroup$ – Joe Dohn Aug 18 '16 at 7:57
  • 1
    $\begingroup$ @JoeDohn there are at least three reasons 1) the people coming up with the requirements might not be programmers, 2) a specification language can be higher-level than a programming language, 3) it's a lot easier to verify that a program complies to a formal spec than verifying that it complies with informal requirements $\endgroup$ – adrianN Aug 18 '16 at 13:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.