The use of formal methods provides confidence in the correctness of developments. Yet one may argue about the actual level of confidence obtained when the method itself -- or its implementation -- is not formally checked. We address this question for the B, a widely used formal method that allows for the derivation of correct programs from specifications. Through a deep embedding of the B logic in Coq, we check the B theory but also implement B tools. Both aspects are illustrated by the description of a proved prover for the B logic.
in a proof assistant consists in mechanizing a logic by encoding its syntax and semantic into a logic ( @cite_8 @cite_5 @cite_2 ). In a embedding, the encoding is partially based on a direct translation of the guest logic into constructs of the host logic. In a embedding the syntax and the semantic are formalised as datatypes. At a fundamental level, taking the view presented in Sec. , the deep embedding of a logic is simply a definition of the set of all sequents (the terms) and a predicate marking those that are (the inference rules of the guest logic being encoded as constructors of this predicate).
@cite_5 @cite_2 @cite_8
1584721038 1541992615 1864574667
Theorem provers were also called 'proof checkers' because that is what they were in the beginning. They have grown powerful, however, capable in many cases to automatically produce complicated proofs. In particular, higher order logic based theorem provers such as HOL and PVS became popular because the logic is well known and very expressive. They are generally considered to be potential platforms to embed a programming logic for the purpose of formal verification. In this paper we investigate a number of most commonly used methods of embedding programming logics in such theorem provers and expose problems we discover. We will also propose an alternative approach : hybrid embedding. Formal reasoning about computer programs can be based directly on the semantics of the programming language, or done in a special purpose logic like Hoare logic. The advantage of the first approach is that it guarantees that the formal reasoning applies to the language being used (it is well known, for example, that Hoare’s assignment axiom fails to hold for most programming languages). The advantage of the second approach is that the proofs can be more direct and natural.