cod. 1008872

Academic year 2019/20
3° year of course - First semester
Academic discipline
Informatica (INF/01)
Discipline informatiche
Type of training activity
48 hours
of face-to-face activities
6 credits
course unit

Learning objectives

By the end of the course the students are expected to:
(1) Understand that building large or complex software systems is essentially different from programming small applications.
(2) Understand the fundamentals concerning the construction of functional specifications of software systems.
(3) Should be fluent in using the Z formal notation as a formal specification language.
(4) Understand the basics of about formally proving specification properties.

Knowledge and understanding
Using formal specification languages for the construction of large or complex software systems is one of the key tools to produce reliable software.

Applying knowledge and understanding
Solve many real-world problems concerning the formal specification of software systems.

Making judgements
Decide what part of a software are critical or complex enough as to be formally specified; decide what properties a given specification should enjoy.

Think and understand that formal specifications are a key communication vehicle among a development team. Be able to write clear, understandable and clearly correct formal specifications.

Lifelong learning skills
Students will learn a key tool of Computer Science, i.e. using logic and mathematics to describe software, which will let them approach their professional work in a essentially different way compared to those who have not been exposed to this knowledge.


Programming skills

Course unit content

1-Formal specification in the Z formal notation

2-The {log} (setlog) satisfiability solver and constraint programming language

3-Specification animation and automated proof

Full programme

- Introduction to formal methods
- Formal specification with the Z notation
- The {log} (setlog) satisfiability solver and constraint programming language
- Translating Z specifications into {log} programs
- Animation of Z specifications by means of {log}
- Automated proof of state invariants


Antoni Diller. Z: An Introduction to Formal Methods. John Wiley Press, 1990.

B. Potter, D. Till, and J. Sinclair. An introduction to formal specification and Z. Prentice Hall PTR Upper Saddle River, NJ, USA, 1996.

Jim Woodcock and Jim Davies. Using Z: specification, refinement, and proof. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1996.

Teaching methods

Standard classes; problem solving on paper; problem solving on computers

Assessment methods and criteria

Individual project in which each student must propose a problem and work out its Z specification including some state invariants, translate it into {log}, run some simulations and discharge some proof obligations concerning state invariants.

Other information

- - -