Proof Hints for Event-B

TL;DR

This paper introduces 'proof hints' in Event-B models, leveraging interactive proof information to enhance model understanding and facilitate the transition from interactive to automatic proofs within the Rodin platform.

Contribution

It proposes a novel method of extracting proof hints from interactive proofs to improve model development and proof automation in Event-B.

Findings

Proof hints aid in understanding formal models.

Proof hints facilitate automatic proof generation.

Enhanced proof automation reduces proof effort.

Abstract

Interactive proofs are often considered as costs of formal modelling activity. In an incremental development environment such as the Rodin platform for Event-B, information from proof attempts is important input for adapting the model. This paper considers the idea of using interactive proofs to "improve" the model, in particular, to convert them into automatic ones. We propose to lift some essential proof information from the interactive proofs into the model as what we called proof hints. In particular, proof hints are not only for the purpose of proofs: it helps to understand the formal models better.