Common use of Foundations of Event-B's Logic Clause in Contracts

Foundations of Event-B's Logic. As ▇▇▇▇▇ is used to develop safety critical systems, bugs in Rodin's theorem prover constitute a serious problem. Unfortunately, several bugs have been discovered that make ▇▇▇▇▇'▇ theorem prover unsound. Obviously, any examination of soundness presupposes a clearly written specification of the logic's syntax, semantics, and proof calculus. There are several publications on the logic of Event-B, but they fail to serve as specification documents, because the logic defined therein is inconsistent [7] or only fragments of the logic implemented in Rodin are considered [8] [9] . Therefore we have devised a rigorous specification document for the logic of Event-B [10] . Mathematical extensions[1] play an important role in avoiding unsoundness, because they allow the user to define new operators, binders, types, and inference and rewrite rules in a soundness preserving fashion. The specification document [10] also devises the theoretical foundations of mathematical extensions. Note that mathematical extensions are well-understood for, e.g., HOL[11] , but the extension methods for HOL cannot be straightforwardly adopted for Event-B because of Event-B's well-definedness [12] mechanism and non-standard term rewriting.