D32 Provers: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Wohuai
No edit summary
imported>Wohuai
No edit summary
Line 2: Line 2:
Concerning Rodin's provers the following contributions have been made:
Concerning Rodin's provers the following contributions have been made:
* Jann Röder (ETH Zurich) developed a relevance filter plug-in. The plug-in provides a proof tactic that first removes hypotheses from a given sequent according to several heuristics. The tactic then inputs the reduced sequent to one or several of Rodin's external provers (PP, newPP, ML). Jann Röder carried out experiments using Event-B models from different domains and observed that his tactic significantly increases the number of proof obligations proved automatically.
* Jann Röder (ETH Zurich) developed a relevance filter plug-in. The plug-in provides a proof tactic that first removes hypotheses from a given sequent according to several heuristics. The tactic then inputs the reduced sequent to one or several of Rodin's external provers (PP, newPP, ML). Jann Röder carried out experiments using Event-B models from different domains and observed that his tactic significantly increases the number of proof obligations proved automatically.
* Matthias Schmalz (ETH Zurich) worked out the theoretical foundations of Event-B's logic. "Event-B's logic" stands for the formalism in which, e.g., guards, invariants, axioms, and theorems are expressed, and proof obligations are expressed and proved. He provides a rigorous specification of syntax, semantics, proofs, theories, and mathematical extensions in ''one'' document. The document encompasses a small theory "Core", proves "Core"'s soundness, and shows how to define the remaining operators, types, and binders available in Rodin using mathematical extensions. The document thus provides a proof calculus for Event-B that is sound by construction, and a methodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions of predefined operators and binders, answering questions like "what is the meaning of <math>x \div y</math> if <math>x</math> or <math>y</math> is negative". For developers, it sheds some light on intricate questions concerning partial functions, e.g., why is it sound to rewrite <math>x \in \{y \mid \varphi(y)\}</math> to <math>\varphi(x)</math> but unsound (in general) to rewrite <math>\varphi(x)</math> to <math>x \in \{y \mid \varphi(y)\}</math>.
* Matthias Schmalz (ETH Zurich) worked out the theoretical foundations of Event-B's logic. "Event-B's logic" stands for the formalism in which, e.g., guards, invariants, axioms, and theorems are expressed, and proof obligations are expressed and proved. He provides a rigorous specification of syntax, semantics, proofs, theories, and [[D32 Mathematical Extensions|mathematical extensions]] in '''one''' document. The document encompasses a small theory "Core", proves "Core"'s soundness, and shows how to define the remaining operators, types, and binders available in Rodin using mathematical extensions. The document thus provides a proof calculus for Event-B that is sound by construction, and a methodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions of predefined operators and binders, answering questions like "what is the meaning of <math>x \div y</math> if <math>x</math> or <math>y</math> is negative". For developers, it sheds some light on intricate questions concerning partial functions, e.g., why is it sound to rewrite <math>x \in \{y \mid \varphi(y)\}</math> to <math>\varphi(x)</math> but unsound (in general) to rewrite <math>\varphi(x)</math> to <math>x \in \{y \mid \varphi(y)\}</math>.


=== Motivations ===
=== Motivations ===
Line 19: Line 19:
Unfortunately, several bugs have been discovered that make Rodin's theorem prover unsound.
Unfortunately, several bugs have been discovered that make Rodin's theorem prover unsound.
Obviously, any examination of soundness presupposes a clearly written specification of the logic's syntax, semantics, and proof calculus.
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 described logic itself is inconsistent or only fragments of the logic implemented in Rodin are considered.  
There are several publications on the logic of Event-B, but they fail to serve as specification documents, because the described logic itself is inconsistent [http://www.event-b.org/abook.html] or only fragments of the logic implemented in Rodin are considered [http://e-collection.ethbib.ethz.ch/eserv/eth:30601/eth-30601-02.pdf] [http://deploy-eprints.ecs.soton.ac.uk/11/4/kernel_lang.pdf].
Therefore a new specification document has been written.
Therefore a new specification document has been written [ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf].


Mathematical extensions allow the user to define new operators, binders, types, and inference and rewrite rules in a soundness preserving fashion.
[[D32 Mathematical Extensions|Mathematical extensions]] allow the user to define new operators, binders, types, and inference and rewrite rules in a soundness preserving fashion.
Hence, they play an important role in avoiding unsoundness.
Hence, they play an important role in avoiding unsoundness.
Therefore, the report also devises the theoretical foundations of mathematical extensions.
Therefore, the report [ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf] also devises the theoretical foundations of mathematical extensions.
Note that mathematical extensions are well-understood for, e.g., HOL, but the extension methods for HOL cannot be straightforwardly adopted for Event-B because of Event-B's well-definedness mechanism and non-standard term rewriting.
Note that mathematical extensions are well-understood for, e.g., HOL, but the extension methods for HOL cannot be straightforwardly adopted for Event-B because of Event-B's [[Well-definedness in Event-B|well-definedness]] mechanism and non-standard term rewriting.


=== Choices / Decisions ===
=== Choices / Decisions ===
Line 31: Line 31:


=== Available Documentation ===
=== Available Documentation ===
This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:
 
* Requirements.
* The internals of the relevance filter plug-in and the process of fine tuning are documented in: [http://TODO Röder Jann, Relevance Filters for Event-B, Master Thesis, ETH Zurich, 2010].
* Pre-studies (states of the art, proposals, discussions).
* [ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf The Logic of Event-B]: a rigorous specification of the logic (for Rodin developers) and a reference document containing the definitions of built-in symbols (for Rodin users).
* Technical details (specifications).
* Teaching materials (tutorials).
* User's guides.  
A distinction shall be made on the one hand between these different categories, and on the other hand between documentation written for developers and documentation written for end-users.


=== Planning ===
=== Planning ===

Revision as of 10:06, 12 November 2010

Overview

Concerning Rodin's provers the following contributions have been made:

  • Jann Röder (ETH Zurich) developed a relevance filter plug-in. The plug-in provides a proof tactic that first removes hypotheses from a given sequent according to several heuristics. The tactic then inputs the reduced sequent to one or several of Rodin's external provers (PP, newPP, ML). Jann Röder carried out experiments using Event-B models from different domains and observed that his tactic significantly increases the number of proof obligations proved automatically.
  • Matthias Schmalz (ETH Zurich) worked out the theoretical foundations of Event-B's logic. "Event-B's logic" stands for the formalism in which, e.g., guards, invariants, axioms, and theorems are expressed, and proof obligations are expressed and proved. He provides a rigorous specification of syntax, semantics, proofs, theories, and mathematical extensions in one document. The document encompasses a small theory "Core", proves "Core"'s soundness, and shows how to define the remaining operators, types, and binders available in Rodin using mathematical extensions. The document thus provides a proof calculus for Event-B that is sound by construction, and a methodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions of predefined operators and binders, answering questions like "what is the meaning of x \div y if x or y is negative". For developers, it sheds some light on intricate questions concerning partial functions, e.g., why is it sound to rewrite x \in \{y \mid \varphi(y)\} to \varphi(x) but unsound (in general) to rewrite \varphi(x) to x \in \{y \mid \varphi(y)\}.

Motivations

Relevance Filtering

Rodin's external provers (PP, newPP, ML) tend to timeout if the given sequent contains many irrelevant hypotheses. For PP and newPP the user can still manually select the hypotheses he considers relevant, but that is a tedious and error-prone process, in particular for large models. Several heuristics for selecting relevant hypotheses have been proposed in the literatur. The relevance filter plug-in implements these heuristics and provides a default configuration that has been shown to be almost optimal on a given collection of models from different domains. The relevance filter plug-in has also significantly increased the number of automatically proved proof obligations on models of industrial partners, which have not been used for fine tuning the heuristics.

Foundations of Event-B's Logic

As Rodin 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 Rodin's 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 described logic itself is inconsistent [1] or only fragments of the logic implemented in Rodin are considered [2] [3]. Therefore a new specification document has been written [4].

Mathematical extensions allow the user to define new operators, binders, types, and inference and rewrite rules in a soundness preserving fashion. Hence, they play an important role in avoiding unsoundness. Therefore, the report [5] also devises the theoretical foundations of mathematical extensions. Note that mathematical extensions are well-understood for, e.g., HOL, but the extension methods for HOL cannot be straightforwardly adopted for Event-B because of Event-B's well-definedness mechanism and non-standard term rewriting.

Choices / Decisions

This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.

Available Documentation

Planning

This paragraph shall give a timeline and current status (as of 28 Jan 2011).