Download Atelier B 4

ClearSy
5.6 Displaying Proof Obligations
This tool enables:
• displaying the proof obligations of a component clause by clause,
• displaying obvious proof obligations, i.e. those that were eliminated by the proof
obligations generator,
• displaying and printing proof obligations using mathematical fonts via a word processing program (LATEXor Word).
The proof obligations include comments that specify:
• the origin of the assumptions (for example: Component invariant),
• the theoretical justification of the proof obligation.
In this case the comment refers to a sub-section in thex Proof obligations - Reference
manual.
Graphical user interface
The GUI is supposed to be launched, a project is opened. To open the GUI of the interactive prover,
it is necessary to click on the given component, and trigger the “Component -> Proof -> Interactive
Proof ...” menu.
The following window will be then dispayed:
ClearSy
70
Atelier B 4 - User manual