Formal Specification and Design Techniques

Formal methods concepts Formal specification

Download 0.69 Mb.

Page	4/6
Date	04.03.2021
Size	0.69 Mb.
	#55992

1 2 3 4 5 6

fmse-introduction

Formal Specification is useful…

Formal methods concepts

Formal specification

Translation of a non-mathematical description (diagrams, tables, English text) into a formal specification language
Concise description of high-level behavior and properties of a system
Well-defined language semantics support formal deduction about specification

Formal Specification is useful…

For those who implement programs to satisfy needs of customers,
For those who test the results,
and those who write instruction manuals for the system.
Because it is independent of the program code, a formal specification of a system can be completed early in its development.

But the name and the comment are not as helpful as they might seem. Some numbers don't have integer square roots. What happens if you call iroot with a set to 3? Negative numbers don't have square roots at all. What if you call iroot with a set to -4? Does it return anything, or does it loop forever - or crash?

These questions reveal the problem with the name and the comment: They aren't complete.

The code doesn't resemble the specification at all. This is the key difference between Z and an executable programming language: The predicate in a Z definition describes what the function does without explaining how to do it; the body of a C function describes how to compute the function without explaining what the result will be.

The two descriptions are complementary; neither can take the place of the other. We need both.

Formal Specification in Z

Code in C

Download 0.69 Mb.

Share with your friends:

1 2 3 4 5 6