San Andres University

Faculty of Pure and Natural Sciences

Computer Science Degree

VDM Method

Cusiquispe Ancasí Juan Pablo 6161096 LP

MARTHA ROCIO MAURICIO LLIFUTA 5969412 LP

TEACHER: LIC. GERMAN HUANCA TICONA

SUBJECT FORMAL SPECIFICATIONS AND VERIFICATION

MANAGEMENT II - 2014
1.- Introduction
The development of the VDM method began in 1970 at the IBM laboratory in Vienna.
A group formed by Heinz Zemanek was working on the definition of a
design of the formal language and in the compiler project. Ideas to create a
operational semantics approach capable of defining the PL/I set,
including the characteristics of the parallel language were built. For this,
a target language called Vienna Definition Language (VDL) was used. The
the approach was very successful, but it was observed that the operational semantics could
to cause complications for formal reasoning. Then, a new emerged
approach, called denotative semantics in 1972. A PL/I compiler was
designed using that metalanguage, called Meta-IV, from which VDM emerged. A
From there, the VDM expanded, but it focused on two main areas. One of
them in Lyngby, Denmark, with Professor Dines Bjorner, one of the pioneers
from VDM and the other in Manchester, England, with Professor Cliff B. Jones.
Formal semantics is one of the areas of study in the science of
computing, concerned with attributing meaning to the constructions of the
programming languages.
Operational semantics is an approach to formal semantics, where the
meaning of a language construction that is specified by computation
when executed on a hypothetical machine. Operational semantics is more
worried about how the programs that simply run them
results of these calculations.
Denotational semantics assigns an approach to formal semantics. In this
Approach, meanings are often modeled by mathematical objects.
defined semantic functions of composition, which represent the effect of
functioning of a structure.
The term VDM is used as a generic term. Several dialects have emerged.
due to the diversification of the research conducted in the area. Different
dialects emerged mainly due to the different areas of application that
they could encompass VDM. This diversity of dialects, however, is difficult to
introduce the method in the industry.
In 1986, work was initiated to establish a version
standardized by VDM-SL. This first standard was initiated by BSI, which
it established a group whose participation was also open to members from other
organizations.
In 1991, the need for standardization was also recognized by ISO/
IEC JTC1 established a working group, SC22/WG19, for this task.
The ISO standard was launched in 1996.
Meta-IV is used to define large portions of the programming language.
PL / I. Other programming languages described, or partially described, use
the Meta-IV and VDM-SL and BASIC, FORTRAN, APL, Algol-60, PASCAL and ADA.
2.- Theoretical Framework

VDM stands for "Vienna Development Method", it is a collection of techniques for

the formal specification and the development of information systems. It consists of a
specification language called VDM-SL; standards for data and the
refining operations to establish links between the specifications that
require abstraction and detailed design specifications at the code level; and
a theoretical method of proof where rigorous arguments can be inferred
about the properties of specific systems and the accuracy of the
design decisions. The term 'VDM' is often used incorrectly to
refer only to the specification of the language.
The origins of VDM come from research in formal semantics of the
programming languages in the IBM laboratory in Vienna between 1960 and 1970,
including the VDL and Meta-IV notations. VDM is its modern descendant,
that is now used beyond the purpose of semantic language in development
of industrial systems and in academic research. A large number of
specification languages were derived from or inspired by VDM-SL, including
RSL, and VDM ++ VVSL, which supports Object-Oriented modeling and
competition systems.
2.1.- The VDM Language
The VDM is a formal method based on a model-based framework for the
denotative semantics to support the gradual improvement of models
abstracts to concrete implementations. The VDM method has a language of
formal specification, VDM-SL, which allows two forms of abstraction: the
representational abstraction and operational abstraction.
The representational abstraction is given by the modeling facilities of
data. These characteristics are based on the six mechanisms for the
structuring of the data mathematicians sets sequences,
correspondences, composite objects, Cartesian products, and unions.
In a low-level language it provides various numerical types, boolean,
among other things, they can be compounds formed by domains, called
domains, through the use of data structure mechanisms. The
domains form the classes of objects that have a mathematical structure
specific. Subtypes are supported by domain definitions using
the domain invariants.
Operational abstraction is supported by functional abstraction and by
relational abstraction. The first refers to the specification of functions and
the second regarding the specification of the operations. Both can
to be specified implicitly using pre and post-conditions, or explicitly
using applicative constructions to specify functions and
imperative constructions to specify operations. The basic difference is
that the operations have direct access to a collection of global objects, is
say, the status of the specification.
The state is a composite object made up of labeled components. A
VDM specification consists of a description of the state, using predicates
from the initialization and predicates of invariants, a set of configurations of
domain that also uses invariants, constants, operations, and functions.
For the standardization of VDM-SL, the semantics was used as a starting point.
of the STC / VDM-RL dialect, to reach its full definition. The definition
the complete pattern of VDM-SL can be divided into different components, such as
such as: (a) syntax defined at various levels of abstraction; (b) representations
of symbols; (c) static semantics; (d) dynamic semantics; and (e) the syntax of
mapping.
Syntax is the main component of VDM-SL and appears in two forms, one
like verification rules and another like type definitions. As an example of
Rule verification considers the syntax of an if-then-else expression. The
concrete syntax is given by:

As definitions of type relationship, the syntax of the if-then-else expression

given by:

Note that syntax is the starting point for defining everything else.
relevant aspects of the VDM-SL standard.
As for the representation of symbols, there are currently two ways,
a math and another ASCII. A mathematical representation has symbols
"elegantes", distinguiendo entre las palabras clave, palabras reservadas, y se
it looks a lot like mathematical notation. The ASCII representation to make the
automatic processing of VDM-SL specifications. Let's take, for example,
a simple mapping of natural numbers to boolean values. In representation
NmB
Mathematics or mapping would be given by the collection ext rw: → while

in the ASCII mapping it would be in the form collectionwr ext: map natabool.

Static semantics defines the specifications that may be

syntactically correct, but that does not necessarily follow the rules of the type
and the scope of language.
Dynamic semantics is based on set theory and notation.
mathematics. Here, operators are used to construct a domain universe
which contains all the valid values that can be expressed in VDM-SL.
The mapping syntax is the component responsible for the transformation between the
VDM-SL specifications and the representations of the defined specifications
a priori.
2.2.- Structure of the VDM
VDM supports two types of structures: (1) representational abstraction, in the
that the data can be described without the structural detail used in the application
final y (2) abstraction of operation, in which the manipulations over the
Abstract objects introduced are described in the representation abstraction.
What can first-order predicate logic and statements be used for?
analogous to programming languages. A specification in VDM is structured
in several blocks, each block is identified by a keyword:

types
definition of types

values
definition of values

functions
<definition of functions>

operations
definition of operations
state of state definition
 end
2.3.- Representational Abstraction
In representational abstraction, a software model can be built to
starting from two basic types of specification language and constructed types
through other compositions, previously defined. There are five definitions
mathematics: set, sequence, mapping, record and tuple. The identifiers in
VDM are made up of alphanumeric characters (case-sensitive)
lowercase) and Greek letters, and without size restrictions. The comments
In VDM, they have the prefix with the character '-'.

2.3.- Simple Types

In VDM, simple types can be subdivided into two categories: types.
primitives defined in the language and 'constants' defined by the user. The types
primitives are the basic elements that belong to the VDM language itself that
it relates to mathematical definitions and not their representation in a
programming language, such as: the type of integer number Z no
It is limited by the number of bits supported by the implementation language.
Table 1 presents the primitive types in VDM, among them the type 'token' that
it represents a collection of accounting values associated with other types.

Table 1: Types Basics

About these, arithmetic operators are defined as " + ", " - ", " * ", " / " and the
relational operators '<', '>', '≤', '≥', '=' and '≠'. The operators listed in the Table
They can also be applied to them:
 Table 2: Operations with basic types
A constant is a user-defined identifier, whose value is itself.
"name", that is, its internal representation is a string with the same value
that its 'name', for example: Orange is a constant whose value is orange.
2.4.- Compound Types
They are types that are built from other previously defined types using
for these type constructors. These constructors can be: unions,
sets, sequences, mappings, records, Cartesian products and types of
functions.
Unions combine two or more types into a single type through the operator "|"
example: User = Teacher | Student, that is, a user type variable
it can be an instant given "teacher" or "student" or also "Message = Success |
ERROR-input" message at a given moment may have the value Success
or input-error, but never both values at the same time.
Sets in VDM must be finite, or countably infinite sets.
they can be specified. These are treated as finite sets
sufficiently "large", so that in this way the can be simplified the
possible mathematical proofs. The syntax is defined as follows:
"Ind: P-set", where "Ind" is the identifier associated with a variable, "P" is the type
(must be defined beforehand) and the word "-set" indicates that this variable will have
a set of values. It is also possible to define new types in a way
analogous, for example: People = Employee-set, that is, the type
"Employee" is a set of people. Another way to specify sets is
using mathematical notation, for example: Pairs ¿ {n b e l o n g s t o N |n myo d 2 =0 }

Digits ¿ {0,1,2,3,4,5,6,7,8,9} . An empty set is described by {} Son

operations on sets are allowed with the traditionally used symbols
used in mathematics to express: union, intersection, difference, this
content, belongs, equality, among others. In addition to an operation denoted
by the word 'card', where 'card S' returns the cardinality of the set S.
Sequences are allowed under the operations as shown in Table 3.
 Table 3: Operations with sequences
Mappings are like mathematical functions (and not functions in languages
programming). These functions associate one set of domain to another set
from image. For example:
X = {1,2,3,4,5 }

Y ={1,8,27,64,125}

M =X m Y
→ – mapping of domain X for image Y, being the
mapping instances:
M1={1↦1,2↦8,3↦27,4↦64,5↦125}

M2= {n m a p s t o m |n is in X and m is in Y · m=n ^ 3 }

These mappings can be applied to the operations described in the

table 4.

Table 4: Operations with functions

Records in VDM are analogous to records in a programming language, and
they are described in the following syntax:
where T is the identifier of the record type being defined and T1, T2,
T3, ... Tn represent the types of each component of T. These components are
called fields and are identifiable by the variables v1, v2,..., vn. The symbol '::'
it is part of the syntax and separates these fields from the record type identifier
created.
Example:

The function 'mk-' is used to instantiate values of a certain type, it

they can assign as parameters, initial values or variables that contain
values that would be assigned to each field according to their order of
statement. For example: "nl = mk-Book(tit, "John", from 2000)" where a
we instantiate a new book with the title value equal to the value "tit", the value of
author field equals 'John' and the year equals '2000'. To access these values of
the variable 'nl', you just have to put the name of the variable followed by '.' and the
field name, for example, to know the title of the book he just wrote
Title
A Cartesian product in VDM and an ordered collection of symbols
grouped by a single name, according to the following syntax: "T = Tn "
T1xT2x ...", where "T" is the name of the Cartesian product type and "T1xT2x ...
In 'his components. As an example, if Book = String X String X N and
Collection = String X String X N, then Book = Collection.
In VDM, 'the types of functions' define the type of domain and the co-domain of
a function, using the following syntax: F=N ↦ N , to denote a function
receives an integer and returns another integer. Examples of instances
(functions) associated with this type are:

(λn:N·n+2) ∈ F receives n , and returnsn+2

( λn:N∙n2 )∈F receives n , and returnsn

2

( λn:N·n mod 2)∈F receives n and returns n m o d 2

A pattern is a structure that consists of collections of identifiers,

symbols and values.
An entry is associated with a pattern if there is a set of values for
defects associated with the pattern, according to the examples in Table 5.

Table 5: Examples of patterns

2.5.- States
In VDM, a 'state' consists of a specification of a certain problem.
including the representation of domain objects and the operations that are
you can do it with the same. The syntax is simple: at the beginning of the state you
place the following sequence 'the state <state name> of' at the end of
block the word "end". In Figure 1, a simplified example is given, since it does not
includes operations. In this example, three domain objects are declared
related to a state called 'department', being these: (1) the courses that
the department has (type: set of courses), (2) the students who are
related to this department (type: group of students) and (3) professors
associated with the department (type: set of teachers).

Figure 1: Example of state

2.6.- Invariants
They are the properties that each entity (object) must preserve, analogous to the
restrictions in the database. They are expressed through notations
mathematics that describe the restrictions on the values for the different
domain objects, these restrictions must be obeyed at the end of each
operation. They can refer to a certain object, in this case
The various objects contained in the same state are called 'type invariants.'
classifying them as "state invariant". An example of a type invariant.

Student △

course completed∧ cursomatriculado = {}

where a keyword that must precede any invariant declaration,

mk - is a function used to create instances of a record, 'Δ' is the
symbol used for creating separate instances of the record of the
expression that describes the invariant and "enrolled course completed course = {}
expression that means the following restriction: the intersection of the courses
done by a student with the courses they enrolled in must be empty. It is
to say, at the end of each operation this invariant must be maintained, ensuring
that a student takes the same course twice. The state invariants
can be built similarly.
2.7.- Operational abstraction
Representational abstraction describes objects in the software domain.
modeling, the behavior of this model is captured through the
operational abstraction. This behavior is described by functions and
operations declared in the 'states' of the system, according to the concept
of the state previously presented. The main difference between the operations and
functions, the last ones do not access global variables, while
operations, in addition to accessing global variables, can also
change their values.
2.7.1.- The Let command
In addition to the functions and operations, expressions can be used.
"complex" to describe the behavior of the system. When you are
expressions are used on several occasions during the specification, it becomes
it's interesting to associate an identifier. In a way, it's possible to draw an analogy.
among the expressions and 'macros' available in programming languages,
for example, 'C'. To associate the identifiers of the expressions that
we use the letque command according to the following syntax: let<definition>in
<expression>.
We see an example:
 let estudiante : Estudiante = mk-Estudiante (“Rodrigo”, “1234”,{}. IngInfor) in
valid-student (student).
2.7.2.- Definition of functions
Functions in VDM can be of four types: (1) implicit functions, (2) the
explicit functions, (3) high-level, and (4) polymorphic functions. The functions
implicit ones are characterized by declarative properties, and they differ from the
explicit functions mainly through syntax. The syntax of functions
implicit is:

where 'func' is the name of the function being declared, p1, p2, ...
pn" are the input parameters, "t1, t2, ..., tn" are the types associated with each
"p" is the return parameter whose type is "t", "B" is an expression.
Boolean that indicates the "pres" -conditions that must be met before the
function be executed and 'B' are the 'post' conditions that must be met
after the execution of the function, where 'B' specifies the majority of the
semantics of the function.
The specification style of explicit functions has two components: one
function declaration and its definition, following the syntax:
Statement
func: t1xt2x.....xtn -> t

where 'func' is the name of the function, 't1xt2….xtn' are the types
associated with each parameter and "t" the return type of the function, and

Definition

func(p1, p2,……., pn) △Ε

pre B
where "func" is the function name, "p1, p2, ....., pn" are parameters of
entry, the symbol △ it is a separator, Ε it is an expression of type 't' and 'B'
it is a pre-condition.
In VDM, high-level functions can be defined from lower-level functions.
of lower abstraction. For example:
 power: N x N → N

power ( ) ( x ) 4 n △ x

A function is polymorphic or generic if it has a structure capable of handling

appropriately different types of parameters. For example:
subsequence [ @ X ] :@ X∗x@X∗→ B

subsequence( small)
There exist i, j in large indices∨ j>i⋀lensmall= j−i+1 ∙
There exists
(find small m:
) →i……
∙j.
For all k in inds small∙small ( k )=large(m ( k ) )

This function checks if the sequence 'small' and the subsequence 'large' returns a
boolean value. However, the two types of elements 'small' and 'large' are not
defined in the function itself, that is, this function is valid for any type of
set. This functionality is syntactically guaranteed by the "@" symbol.
2.7.3.- Definition of Operation
Operations can also be of two types: (1) implicit operations and (2)
the explicit operations. The implicit operations have similar functions to
the implicit functions, but they have two additional clauses: external clause
"ext", which contains a list of all global variables that can be accessed by
the operation and the error block of 'err'. Thus forming the following
syntax:
where 'Oper' is the name of the operation, the 'p's', 't's' and the blocks 'B' and 'B ''
they have the same meaning as the functions, 'ext' is the keyword that
indicates the start of the external clause, where <node> is mode (rd-read and wr-
writing) with which the variables "g1, g2, ..., gk" are used, "err" is the
keyword that indicates the start of the error block, where "e1, e2, ..., en"
The identifiers of each error 'B1, B2, ..., Bn' are expressions.
boolean variables that indicate the occurrence of errors and "B'1, B'2, ... B'n" are actions
associated with each error.
2.7.4.- Definition of declarations
In VDM, it is possible to use existing statements in languages of
programming like C or Pascal. Table 6 presents some statements
valid followed by its syntactic definition.
These statements have a similar semantics to the commands used in the
programming languages. Generally, these statements are used
to better detail the specification, when it is at a level of
abstraction very close to the programming level.

Table 6: Examples of Statements

3.- Conclusions:
We can conclude that the VDM method aids in the abstraction of tests.
simulation where data refinement includes the specification of machines
of state since the VDM supports two types of structures: the abstraction
representational, in which data can be described without structural detail
used in the final application and the abstraction of operation, in which the
manipulations on the introduced abstract objects are described in the
abstraction of representation so that predicate logic can be used
first order and analogous statements of programming languages.
4.- Bibliography

Seven Myths of Formal [Link] Hall. IEEE Software, September

1990.

Seven More Myths of Formal [Link] P. Bowen, Michael G.

Hinchey. IEEE Software, July 1995.

Ten Commandments of Formal [Link] P. Bowen, Michael G.

Hinchey.

Ten Commandments of Formal Methods... Ten Years [Link] P.

Bowen, Michael G. Hinchey. IEEE Computer, January 2006.

Verified Software: theories, tools, experiments. Vision of a Grand Challenge

[Link] Hoare and Jay Misra, July 2005.

Verified Software: A Grand [Link] Jones, Peter O'Hearn, Jim

Woodcock. IEEE Computer, April 2006.

First Steps in the Verified Software Grand [Link] Jones, Peter

O'Hearn, Jim Woodcock. IEEE Computer, April 2006.

A Specifier's Introduction to Formal MethodsJeanette M. Wing. IEEE

Computer, 1990.