Download MDELTA - Atelier B

Contents
1 Introduction
3
2 Terminology
5
2.1
Abbreviations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5
2.2
Definition of terms used . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5
3 Problem presentation
7
3.1
Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7
3.2
Well-definedness conditions . . . . . . . . . . . . . . . . . . . . . . . . . . .
8
3.3
Example of well-definedness lemma generation
. . . . . . . . . . . . . . . .
8
3.4
MLE location . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
9
3.5
The mdelta tool for checking well-definedness . . . . . . . . . . . . . . . . .
9
4 Using mdelta
11
4.1
When you should use it . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
4.2
Step I: Running mdelta . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
4.2.1
Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
4.2.2
Output . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
4.3
Step II: Verifying the application of mdelta . . . . . . . . . . . . . . . . . . 12
4.4
Step III: Creating the delta PROJECT B project . . . . . . . . . . . . . . . 13
4.5
4.4.1
Manual creation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
4.4.2
Automatic creation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
4.4.3
Script Output . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
Step IV: Proving the well-definedness lemmas . . . . . . . . . . . . . . . . . 13
1