A Specifier’s Introduction to Formal Methods (작업중)

runicode 2009. 3. 10. 16:40


A Specifier’s Introduction to Formal Methods


Jeannette M. Wing, Carnegie Mellon University


Applied to computer systems development, formal methods provide mathematically

based techniques that describe system properties.

As such, they present a framework for systematically specifying, developing, and verifying systems.


Formal methods used in developing computer systems are mathematically based techniques for describing system properties. Such formal methods

provide frameworks within which people can specify, develop, and verify systems in a systematic, rather than ad hoc, manner.

A method is formal if it has a sound mathematical basis. typically given by a formal specification language. This basis provides the means of precisely defining notions like consistency and completeness

and, more relevantly, specification, implementation, and correctness. It provides the means of proving that a specification is realizable, proving that a system has been implemented correctly, and proving properties

of a system without necessarily running it to determine its behavior.

A formal method also addresses a number of pragmatic considerations: who uses it, what it is used for, when it is used, and how it is used. Most commonly, system designers use formal methods to specify a

system’'s desired behavioral and structural properties.

However, anyone involved in any stage of system development can make use of formal methods. They can be used in the initial statement of a customer’'s requirements, through system design, implementation,

testing, debugging, maintenance, verification, and evaluation.

Formal methods are used to reveal ambiguity, incompleteness, and inconsistency in a system. When used early in the system development process, they can reveal design flaws that otherwise might be discovered only during costly testing and debugging phases. When used later, they can help determine the correctness of a system implementation and the equivalence of different implementations.

For a method to be formal, it must have a well-defined mathematical basis. It need not address any pragmatic considerations, but lacking such considerations would render it useless. Hence, a formal method should possess a set of guidelines or a “"style sheet”" that tells the user the circumstances under which the method can and should be applied as well as how it can be applied most effectively.

One tangible product of applying a formal method is a formal specification. A specification serves as a contract, a valuable piece of documentation, and a means of communication among a client, a specifier, and an implementer. Because of their mathematical basis, formal specifications are more precise and usually more concise than informal ones.

Since a formal method is a method and not just a computer program or language, it may or may not have tool support. If the syntax of a formal method’'s specification language is made explicit, providing standard syntax analysis tools for formal specifications would be appropriate. If the language’'s semantics are sufficiently restricted, varying degrees of semantic analysis can be performed with machine aids as well. Thus, formal specifications have the additional advantage over informal ones of being amenable to machine analysis and


For more on the benefits of formal specification, see Meyer. For more on the distinction between a method and a language, and what specifying a computer system means, see Lamport.

What is a specification language?


A formal specification language provides a formal method’s mathematical basis. I borrowed the terms and definitions that follow from Guttag et al. Burstall and Goguen have used the term "language" and more recently the term "institution" for the notion of a formal specification language.


Definition: A formal specification language is a triple, <Syn, Sem, Sat>, where Syn and Sem are sets and Sat ⊆ Syri x Sem is a relation between them. Sw is called the language’'s syntactic domain; Sem, its semantic domain; and Sur, its satisfies relation.

Definition: Given a specification language, <Syn, Sem, Sat>, if Sat(syn, sem) then syn is a specification of sem, and sem is a specificand of syn.

Definition: Given a specification language, <Syn, Sem, Sat>, the specificand set of a specification syn in Syn is the set of all specificands sem in Sem such that Sar(sw, sem).


Less formally, a formal specification language provides a notation (its syntactic domain), a universe of objects (its semantic domain), and a precise rule defining which objects satisfy each specification. A specification is a sentence written in terms of the elements of the syntactic domain. It denotes a specificand set, a subset of the semantic domain. A specificand is an object satisfying a specification. The satisfies relation provides the meaning, or interpretation, for the syntactic elements.

Backus-Naur form is an example of a simple formal specification language, with a set of grammars as its syntactic domain and a set of strings as its semantic domain. Every string is a specificand of each grammar that generates it. Every specificand set is a formal language.

In principle, a formal method is based on some well-defined formal specification language. In practice, however, this language may not have been explicitly given. The more explicit the specification language’'s definition, the more well-defined the formal method.

Formal methods differ because their specification languages have different syntactic and/or semantic domains. Even if they have identical syntactic and semantic domains, they may have different satisfies relations.


Syntactic domains. We usually define a specification language’'s syntactic domain in terms of a set of symbols (for example, constants, variables, and logical connectives) and a set of grammatical rules for combining these symbols into well-formed sentences. For example, using standard notation for universal quantification (V) and logical implication (*), let x be a logical variable and P and Q be predicate symbols. Then this sentence, Vx.P(x) Q(x), would be well-formed in predicate logic, but this one, Vx. + P(x) 3 Q(x), would not because + is a binary logical connective.

A syntactic domain need not be restricted to text; graphical elements such as boxes, circles, lines, arrows, and icons can be given a formal semantics just as precisely as textual ones. A well-formedness condition on such a visual specification might be that all arrows start and stop at boxes.


Semantic domains. Specification languages differ most in their choice of semantic domain. The following are some examples:


Abstract-data-type specification languages are used to specify algebras, theories, and programs. Though specifications written in these languages range over different semantic domains, they often look syntactically similar.

Concurrent and distributed systems specification languages are used to specify state sequences, event sequences, state and transition sequences, streams, synchronization trees, partial orders, and state machines.

Programming languages are used to specify functions from input to output, computations, predicate transformers, relations, and machine instructions.


Each programming language (with a welldefined formal semantics) is a specification language, but the reverse is not true, because specifications in general do not have to be executable on some machine whereas programs do. By using a more abstract specification language, we gain the advantage of not being restricted to expressing only computable functions. It is perfectly reasonable in a specification to express notions like “"Forallxin set A, there exists ay in setB such that property P holds

of.randy,”"whereA andBmightbeinfinite


Programs, however, are formal objects,

susceptible to formal manipulation (for

example, compilation and execution). Thus,

programmers cannot escape from formal

methods. The question is whether they work

with informal requirements and formal

programs, or whether they use additional

formalism to assist them during requirements


When a specification language’'s semantic

domain is over programs or systems of

programs, the term implements is used for

the satisfies relation, and the term implementation

is used for a specificand in Sem.

An implementation prog is correct with

respect to a given specification spec ifprog

satisfies spec. More formally,

Definition: Given a specification language,

<Syn, Sem, Sat>, an implementation prog in

Sem is correct with respect to a given

specification specin Syn if andonly ifSar(spec,


Satisfies relation. We often would like

to specify different aspects of a single

specificand, perhaps using different specification

languages. For example, you might

want to specify the functional behavior of

a collection of program modules as the

composition of the functional behaviors of

the individual modules. You might additionally

want to specify a structural relationship

between the modules such as what

set of modules each module directly invokes.

To accommodate these different views

of a specificand, we first associate with

each specification language a semantic

abstraction function, which partitions

specificands into equivalence classes.

Definition: Given a semantic domain, Srm, a

semantic abstraction function is a

homomorphism, A: Sem 4 z5“"”",th at maps

elements of the semantic domain into

equivalence classes.

For a given specification language, we

choose a semantic abstraction function to

induce an abstract satisfies relation between

specifications and equivalence classes of

specificands. This relation defines a view

on specificands.

Definition: Given a specification language,

<Sjn, Sem, Sat>, and a semantic abstraction

function, A, defined on Sem, an abstract

satisfies relation, ASat:Syn + 2‘'“"”", is the

induced relation such that

Vspec E Synpog E Sem

[Sat(spec,prog) = ASut(spec,A(prog))]

Different semantic abstraction functions

make it possible to describe multiple views

of the same equivalence class of systems,

or similarly, impose different kinds of constraints

on these systems. Having several

specification languages with different semantic

abstraction functions for a single

semantic domain can be useful. This encourages

and supports complementary

specifications of different aspects of a system