Keywords

1 Introduction

In this paper, we present the set theory of the B method [1] using polymorphic types and rewriting. Expressed this way, this theory has the benefit of being quite automatable for several reasons. In particular, the use of polymorphism allows us to make the theory more synthetic by removing some typing predicates, which therefore improves proof search. As for rewriting, it is introduced along the lines of deduction modulo theory [5], where axioms are turned into rewrite rules over both propositions and terms. Deduction modulo theory has proved to be also very useful to improve proof search when integrated to usual automated proof techniques. In this paper, we also aim to advertise that more and more automated tools are able to deal with polymorphic types and rewriting, and we provide some experimental results involving the latest versions of these tools.

2 A Set Theory with Polymorphism and Rewriting for B

In the following, we consider the pure set theory part of the B method, i.e. the material introduced in Chap. 2 of the B-Book [1]. This part of the B theory is suitable as it can be easily turned into a theory that is compatible with deduction modulo theory, i.e. where a large part of axioms can be turned into rewrite rules. We therefore transform whenever possible the axioms and definitions into rewrite rules. The resulting theory is summarized in Figs. 1 and 2, where we omit the set \(\mathsf {BIG}\) and the sets defined in extension.

Fig. 1.
figure 1

Rewriting rules of the B set theory (part 1)

Full size image

As can be seen, the proposed theory is typed, using first order logic extended to polymorphic types à la ML, through a type system in the spirit of [2]. This extension to polymorphic types offers more flexibility, and allows us to deal with theories that rely on elaborate type systems, like the B set theory. The complete type system used here can be found in [3]. The type constructors, i.e. \(\mathsf {tup}\) for tuples and \(\mathsf {set}\) for sets, and type schemes of the considered set constructs are provided in Fig. 3 of Appendix A, where Type is the type of types and \(o\) the type of formulas. Type arguments are subscript annotations of the construct, and to improve readability, we remove the type annotations in tuples when they are redundant with the membership construct.

Fig. 2.
figure 2

Rewriting rules of the B set theory (part 2)

Full size image

3 Experimental Results

To test the previous theory, we consider 319 lemmasFootnote 1 coming from Chap. 2 of the B-Book [1]. As tools, we consider automated theorem provers able to deal with polymorphic types and rewriting natively. Our set of tools includes: Zenon Modulo (version 0.4.2), a tableau-based prover that is an extension of Zenon to deduction modulo theory; ArchSAT (development versionFootnote 2), a prover that combines a SAT solver with tableau calculus and rewriting; and Zipperposition (version 1.5), a prover based on superposition and rewriting. To show the impact of rewriting over the results, we also include the Alt-Ergo SMT solver (version 1.01), which deals with polymorphic types but not rewriting.

The experiment was run on an Intel Xeon E5-1650 v3 3.50 GHz computer, with a timeout of 90 s and a memory limit of 1 GiB. The results are summarized in Table 1. These results show the high performances, in terms of proved problems, obtained by the provers extended to rewriting, Zipperposition and ArchSAT in particular, compared to the SMT approach of Alt-Ergo. Looking at the cumulative times, Alt-Ergo is not really faster than Zipperposition and ArchSAT, which take more time to find few more difficult problems (with a timeout of 3 s, they respectively find 303 and 260 proofs in 17.61 s and 16.61 s, while Alt-Ergo finds the same number of proofs). The low results of Zenon Modulo are probably due to the fact that it uses a heuristic to transform the axioms into rewrite rules.

Table 1. Experimental results over the B set theory benchmark
Full size table

4 Conclusion

In light of the previous experimental results and as perspectives, we aim to apply our approach, consisting of a B set theory using polymorphic types and rewriting together with appropriate tools (Zenon Modulo, ArchSAT, and Zipperposition), to proof obligations coming from the formalization of real-world applications. In particular, we plan to use the benchmark provided by the industrial partners of the BWare project [4], which gathers about 13,000 proof obligations.