Download as a PDF

Contents
1 Introduction
5
2 First Overview
6
2.1
Origins of the Vienna Development Method . . . . . . . . . . . .
6
2.2
Rigorous Specification and Proof . . . . . . . . . . . . . . . . . .
6
2.2.1
Rigorous Specification . . . . . . . . . . . . . . . . . . . .
7
2.2.2
Rigorous Proof . . . . . . . . . . . . . . . . . . . . . . . .
8
Formalization and Tools Support . . . . . . . . . . . . . . . . . .
9
2.3
3 The Language
3.1
3.2
3.3
3.4
9
Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
10
3.1.1
Explicit Functions . . . . . . . . . . . . . . . . . . . . . .
10
3.1.2
Implicit Functions . . . . . . . . . . . . . . . . . . . . . .
11
Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
13
3.2.1
Example: Simple Calculator . . . . . . . . . . . . . . . . .
13
3.2.2
The State . . . . . . . . . . . . . . . . . . . . . . . . . . .
15
Set Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
15
3.3.1
The ”-set” Constructor . . . . . . . . . . . . . . . . . . .
16
3.3.2
Partitions . . . . . . . . . . . . . . . . . . . . . . . . . . .
16
Composite Objects . . . . . . . . . . . . . . . . . . . . . . . . . .
17
3.4.1
Defining Composite Objects . . . . . . . . . . . . . . . . .
17
3.4.2
Creating Instances . . . . . . . . . . . . . . . . . . . . . .
18
3.4.3
Decomposing Objects . . . . . . . . . . . . . . . . . . . .
19
2