Download as a PDF

4 A Proof Framework for VDM — Mural
20
4.1
Constants and Expressions
. . . . . . . . . . . . . . . . . . . . .
21
4.2
Rules of Inference . . . . . . . . . . . . . . . . . . . . . . . . . . .
22
4.3
Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
22
4.4
Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
22
4.5
A Sample Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . .
23
5 VDMTools
24
5.1
Main Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
24
5.2
VDM++
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
25
5.2.1
A Basic Class Outline . . . . . . . . . . . . . . . . . . . .
25
5.2.2
The Language
25
. . . . . . . . . . . . . . . . . . . . . . . .
6 A VDMTools Example
6.1
27
Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
27
6.1.1
Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
27
6.1.2
Instance Variables . . . . . . . . . . . . . . . . . . . . . .
28
6.1.3
Constructors . . . . . . . . . . . . . . . . . . . . . . . . .
28
6.1.4
Operations . . . . . . . . . . . . . . . . . . . . . . . . . .
29
6.2
Screenshots . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
6.3
VDM to Java . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
6.4
Java to VDM . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
36
6.5
Other features
36
. . . . . . . . . . . . . . . . . . . . . . . . . . . .
7 Conclusion
36
3