Rigorous software engineering: a method for preventing software defects - Technical

Stephen P. Bear

Formal specification languages enable software engineers to apply the rigorous concepts of discrete mathematics to the software development process.

The technology base of electronics and computer companies like Hewlett-packard is changing-software has become pervasive. In all market sectors the proportion of software in individual products continues to increase. Fig. 1 shows the dramatic increase of software in products of one family developed between 1979 and 1989. Product A produced in 1979 was entirely hardware, and contained no software at all. Product B contained 38 KNCSS (thousands of lines of noncomment source statements) of Pascal. In 1986, product C contained 200 KNCSS of structured assembly language, which is equivalent to about 100 KNCSS of a high-level language like Pascal or C. The current member of the family, product D released in 1989, contains some 350 KNCSS of C.

Growth like this is not accidental because there is a feedback loop that drives the increased functionality provided by increased software. Software enables us to design products with greater functionality. Initially, this functionality provides a competitive advantage, but it soon becomes essential to success in the market. To make an impact, each new product must have more features and more software.

Software Takes Too Long

This massive change in products, with software providing much of the functionality, is happening despite significant shortcomings in the current software development processes. The principal problem is that software development takes too long. The development process is difficult to control and defect removal can introduce seemingly arbitrary delays.

Delays increase development costs, but more important, they also reduce market share and affect overall lifetime profit. Studies of high-growth, short-lifecycle markets suggest, that a six-month delay in introducing a product can reduce profit by 33%.' One HP Division estimates that for each new product, finding and removing bugs can cost over I million dollars.(2)

Software development takes too long because it is wasteful. Errors and defects are introduced during development, but are not detected quickly. Further work is then built upon the erroneous development. When a defect is detected., there are many interlocking details, and these must be reworked or discarded. During development this happens repeatedly. Again and again, work carried out at one stage is thrown away and must be replaced.

Defects not detected until late in the software development process can affect large amounts of work. They are difficult, time-consuming, and expensive, to correct. Defects detected early in the development process require less work and typically they are easier and cheaper to correct.

Fig. 2 shows the cost of removing defects detected at various points in the software development process, as calculated by the software quality engineering group at one HP Division. Notice that costs of removal increase exponentially as the development proceeds.

It is instructive to look at these figures in a slightly different way, and to consider the cost of introducing an error at various points of the development process. If an error is detected by a code inspection or design review soon after it is introduced, it can be fixed quickly and cheaply. For example, if a specification error is detected at specification time, it will be cheap to repair. However, if it is not detected at this stage, then it is likely to lie dormant until the consequences of the error are observed, by which time it will be much more expensive to correct.

It turns out that the introduction and detection of the consequences of an error are nested because typically:

* Errors introduced during low-level design and coding are observed quickly during compilation and unit test

* Errors introduced during high-level design are observed during integration and system test

* Errors introduced during specification are not observed until system test and use.(3)

We can use this relationship to estimate the relative costs of introducing a defect at various points in the development process. It shows that a defect introduced early in the development process-and not detected immediately-will be much more expensive to fix than an error introduced during coding (see Fig. 3).

Clearly, defect prevention during specification and design is extremely important. Getting it right at this point is where it really matters. However, if we look at current practice, we see that the analytical and descriptive tools used during specification and design are very weak. There is little attempt to capture behavior at the specification stage. Early narrative documents describe features, but these are inevitably anibiguous, incomplete, and often contradictory. High-level descriptions of behavior are just as vague, and precise descriptions often resort to implementation details.

The result is a rush to code. Developers do not spend time understanding and describing behavior because it is hard to capture and communicate. Instead they use the implementation to document issues and resolve problems. Often, the implementation is the first precise description of what the software will do.

Many important decisions about overall behavior are made by programmers working at the lowest level of detail. This is not a good way to think about behavior, and decisions made in this way are often inconsistent or undesirable. Aspects of behavior emerge from interactions that have never been explicitly considered or analyzed. Behavioral defects embedded in the code are difficult to detect by inspection or review. However, they are the defects that begin the costly cycle of rework and waste.

Rigorous Software Engineering

Rigorous software engineering is an approach to software development that addresses quality and productivity by emphasizing the early stages in the development process. Rigorous software engineering concentrates on developing an early, precise understanding of the required behavior of the system under development. Expensive specification and design errors can be avoided, or detected and corrected before the implementation begins.

The rigorous software engineering philosophy could be summarized as one of defect prevention. Think carefully about what you want to do and get it right the first time.

The approach is to develop an abstract, but precise description of the behavior of the software system. This description can be reviewed to ensure that the system does what is required. If there are problems, they can be fixed quickly and cheaply-long before an implementation is created.

Underlying the rigorous approach are formal specification languages. These are mathematically based languages that provide support for abstract and precise descriptions of software systems.

Rigor in the Software Lifecycle

Rigor can be used effectively at all stages of the software lifecycle. Naturally, if the early stages of the development are more error-prone or more costly if flawed, then those stages are likely to benefit most.

If we take a simple model of software development-specification then design then implementation then testing-we can show the application and benefits of rigorous software engineering for each stage. In real software development, these phases will appear, but they may be interleaved, repeated, or omitted.

Specification. Rigorous techniques are particularly useful at the specification stage. A rigorous system of specification is both abstract and precise. Abstraction focuses attention on the essential aspects of behavior. An abstract description is not cluttered or confused with irrelevant details. It makes the behavior of the system easier to understand and to think about. Precision encourages careful thought because issues must be resolved and cannot be hidden in an ambiguous narrative.

Together, abstraction and precision make it possible to communicate the proposed behavior. Reviews and inspections can be more effective. Other people can understand what is suggested because they can analyze consequences and identify problems or omissions.

The specification of the system will construct a model that shows all the required properties of the system. This model can be used to resolve difficult issues of behavior. If the model cannot resolve these issues, then it is flawed and needs improvement. In practice, this makes it difficult to ignore tricky areas of the specification.

A rigorous specification, then, provides benefits to both the authors of the specification documents and the reviewers of those documents. Clarity of thought and concept helps prevent defects from being introduced. Clarity of expression empowers reviewers and helps ensure that defects are quickly identified and removed.

Design. A feature of the rigorous software engineering approach is the ability to separate concerns. In the specification phase, emphasis is placed on what a system is to do. In the design phase emphasis is placed on how the system is to be built because decisions about behavior have already been made. It is not necessary to resolve requirements issues while doing design.

Precise specifications provide detailed guidance for designers. Teams of designers know what is to be done. This makes it easier for the development to be well-managed because tasks can be defined precisely (design the feature whose specification is as follows) and allocated to developers. Misunderstandings causing integration problems or system errors can be dramatically reduced.

It is straightforward to combine the rigorous approach with techniques such as structured design.4,5 This gives many benefits, especially the ability to trace which parts of the design implement which parts of the specification. This traceability is an important attribute of any development process, allowing subsequent enhancements to code to be done in a controlled way and improving the quality of the finished software product. The article on page 51 shows the combination of structured design techniques and rigorous specifications.

Good specifications are, especially important when software is developed by subcontractors. Rigorous specifications can be made tight enough to allow subcontractors to implement precisely the desired functionality, and for there to be much less disagreement over the required behavior of the system.

Implementation. As with design, decisions about requirements have already been made. In addition, at this stage, design decisions have also been made. Effort is concentrated on producing an efficient implementation of the desired behavior.

The code modules can be traced to the design descriptions and the design descriptions can be traced to the specifications. The vocabulary of the specification is used in the commentary for the code-for example, to state properties that particular functions depend on to work correctly.

Testing and inspections. Throughout the development, the deliverables of the various stages can be tested or inspected. Before executable code is available, the specifications and design documents can be formally inspected using standard industry practices.6 The descriptions provide precise, independent criteria for correctness. In a formal inspection the reviewers know what the design or code is supposed to do and can check whether it meets these requirements.

The correctness of test cases can also be reviewed against the specifications. The behavior of the system should be predictable from the specification and tests can be chosen to verify this. Industry-standard testing techniques7,8 can be used to supplement the tests from the specifications to catch additional code-oriented errors.

Formal Specification Languages

Rigorous software engineering requires precise but abstract descriptions of behavior. It is possible to write these descriptions in a natural language such as English, German, or Japanese, but it, is very difficult to do so without introducing anibiguity and other problems. The key to rigorous software engineering is the use of formal specification languages to describe behavior.

Formal specification languages look like programming languages in that they both have special syntax and use special symbols, but they do very different jobs. A formal specification language is designed to describe what a product is to do while a programming language is designed to describe how it is to be done.

The syntax and symbols of formal specification languages are based on discrete mathematics. This can be intimidating to begin with, but in fact the math is quite simple--far easier than the continuous mathematics routinely used by hardware engineers. The math is used to provide an abstract mathematical model of the system. This is not a new idea since it is the standard approach in engineering to use a model to understand the behavior and properties of a system.

One such language is the Hewlett-packard Specification Language, HP-SL(9). HP-SL has been developed at HP Laboratories in Bristol, England, and has already been used on real software development projects at several divisions in HP The language is supported by a toolset (the HP Specification Toolset), based on the emacs editor with an optional interface to the HP Softbench(10) product. The toolset allows the production of specification documents containing a mixture of natural language and HP-SL. Using the toolset, specifications can be chocked for syntactic correctness and for type correctness. The toolset is not a Hewlett-packard product, but has been made available to academic and research institutions.

HP-SL is a specification language that uses data types, functions and logic to describe properties of software systems. These properties can be expressed at both a high level of abstraction and a high level of precision. This combination of abstraction and precision allows important behavior to be captured without becoming lost in a mass of detail.

An Overview of HP-SL

The HP Specification Language, or HP-SL, is a notation for describing the behavior of software systems and components in an abstract yet precise manner. The language allows attention to be focused on what a system does, while deferring decisions on how a system is implemented.

The following sections introduce some of the main parts of HP-SL. This should provide a useful guide to interpreting the HP-SL specifications presented in this issue.

Values

In HP-SL, values can be given names. These names can then be used to represent values. The following declaration gives the name num to the value 3.

val num: Int [delta/=]- 3

The declaration also says that num is of type Int (integer). Int is one of the predefined HP-SL types. A declaration need not define exactly which value is chosen for a name. For example,

val num[.sub.1] : Int

says that num, is the name for some value of type Int, but does not say which particular value is chosen. Later sections will show that logic can be used to constrain values that are given names.

Value declarations can appear at the top level of a specification (as above) in which case their scope is the entire specification. They can also be used to define local values using a let expression. The let construct is similar to that found in many functional programming languages. For example, the value of the expression:

  let
       val one: Nat1 [delta/=] 1
       val ten: Nat1 [delta/=] 10
      in
       one + ten
      endlet

is the natural number 11. The names one and ten are defined in an inner scope and are not visible outside the let expression.

Types

Types in HP-SL are much like types in a programming language in that they are collections of similarly structured values that permit the same set of operations. Thus, numbers and Booleans (truth values TRUE and FALSE) are distinct types, since arithmetic operators +, -, *, etc.) work on numbers but not on truth values, and the logical operators (A, V, ==>, etc.) work on truth values but not on numbers.

HP-SL provides a number of predefined types and ways of constructing brand new types from existing types. HP-SL also allows names to be given to types. Predefined Types. Table I lists the predefined types in HP-SL. These types are available for use in all specifications.

The numerical types (Real, Int, Nat0, and Nat0 have all the expected arithmetical operators defined on them +, -, * , /, <, >, mod, etc.). The Boolean type has the five standard Boolean operators defined on it ( A logical AND, V logical OR, => logical implication, - logical negation, and - logical equivalence).

Naming Types. In HP-SL, types can be given additional names. The following declaration gives the name MyNum to the existing type Nat0.

syntype MyNum [delta/=] Nat0

This declaration does not introduce a new type, but merely gives another name to an existing type. Values of type MyNum are indistinguishable from values of type Nat0. (The keyword syntype derives from synonym type).

Constructing Types. HP-SL has some predefined type constructors that provide ways of creating more, complicated types from other types. The most common of these are sets, sequences, and maps.

Sets. These types are used to model collections of data for which order and repetition are unimportant. Set types in HP-SL are constructed using the type constructor Set. For example,

syntype Natset [delta/=] Set Nat0

associates the name Natset with sets of natural numbers. Values of the set types are written as follows:

val empty_set: Natset [delta/=]{}

val even_set: Natset [delta/=]{2,4,6}

where empty_set is a name for the empty set, and even_set is a name for the set containing three elements 2, 4, and 6.

For large sets, it is not practical to list all the values. Therefore, HP-SL provides a syntax similar to the conventional mathematical set comprehension.

val one_to_a_thousand [delta]/=]{x~x:Nat0 . x [equal to or less than] ~ x [equal to or more than] 1000}

The set one to-a-thousand contains all the natural numbers between 1 and 1000.

HP-SL provides all the conventional set operators (U set union, n set intersection, E-= set membership, \ set difference, and C subset).

3 [element of] {1...5} = TRUE

(1,2) [union cup] {2,3,4} = {1,2,3,4}

(1,2) [intersectioncap] n {2,3,4} = {2}

{1,2} \ {2,3,4} = {1}

{1,2} [subsetor is = to] {1,2,3} = TRUE

Sequences. These types are used to model collections of data for which order and repetition are important. Sequence types in HP-SL are constructed using the type constructor Seq. For example,

syntype Natseq [delta/=] Seq Nat0

associates the name Natseq with sequences of natural numbers. Values of this sequence type are written as follows:

val empty_seq: Natseq [delta/=] << >>

val even_seq: Natseq [delta/=] << 2, 4 >>

where empty_seq is defined to be the empty sequence, and even_seq is defined to be the sequence of two elements, the first of which is 2 and the second of which is 4.

There are a few standard names for sequence operators. The names for the HP-SL sequence operators are listed in Table II.

Maps. These types are used to associate values of some type with values of another type. In programming languages, maps are implemented by structures such as hash tables, association lists, and trees. In HP-SL map types are constructed directly using the type congtructor m/-->. For example, the definition:

syntype Char_to_num [delta/=] Charm/-->Nat0

gives the name Char_to_num to the type mapping values of type Char to values of type Nat0. Values of this map type are written as follows:

val empty: Char_to_num [delta]/= []

val amap: Char_to_num [delta]/= ['a' ~--> 1, 'p' ~--> 1]

where empty is the empty map and amap is the map that associates 'a' with 2, 'm' with 1, and p' with 1. The function lookup is provided to return the associated value in a map. For example,

lookup amap 'a' = 2.

Another function, dom, is provided to calculate the elements in a map's domain. For example, dom amap = {'a','m', 'p'}.

Introducing New Types. We have already seen ways of giving names to types using the syntype keyword. Doing this does not introduce a new type, it merely gives a name to an existing type. To introduce a new type, HP-SL provides the keyword type. This can be used in a variety of ways to construct new types, most of which are advanced topics in HP-SL. The most common use of type is to make record and union types. Record types contain values of several other types, and union types permit choices between alternatives.

For example, consider a record type used to represent boats. To represent a boat in this simple example, we only need to know the displacement of the boat and the number of engines it has. The type Boat will be adequate for this (assume we already have a type Weight to record the displacement).

  type Boat
       [~  boat ~>
        (engines: Nat1,
         displacement: Weight)
       ~]

This definition states that values of type Boat have two fields: engines and displacement. The type of the engines field is Nat1, while the type of the displacement field is Weight. We can construct values of Boat using the name before the > symbol-boat.

val single: Boat [delta]/= boat(1, 5000)

val double: Boat [delta]/= boat(2, 7000)

The value single is intended to represent a single-engine boat with displacement 5000, and double a twin-engine boat with displacement 7000. Just as in a programming language, the fields of a record value can be accessed. In HP-SL, the fields are accessed by functions generated from the field names used in the type definition.

engines(double) = 2

displacement(single) = 5000

Consider now a type Ship, values of which are either boats (as before) or yachts. Yachts have sails, not engines, and an important statistic is the sail area. We define this using the following union type:

  type Ship [delta]/=
                [~  boat ~>
                  (enagines: Nat1,
                  diaplacement: Weight)
                  ~]
         ~
        [~ yacht ~>
         (sail_area: Area,
         displacement: weight)
        ~]

The symbol "I" is used to indicate alternatives in union types.

We can redefine the previous boats as ships:

val single: Ship [delta]/= boat(1, 5000)

val double: Ship [delta]/= boat(2, 7000)

val yacht[.sub.1]: Ship[delta]/= yacht(400, 2000)

The field accessing mechanism works as before:

displacement(double) = 7000

displacement(yacht[.sub.1]) = 2000

Functions

Functions are used to model computations and calculations. Functions in HP-SL are "pure" in the sense that they cannot have side effects.

Functions are defined in one of two ways-explicitly or implicitly. An explicit function definition gives a formula to calculate a result from the inputs. An implicit function definition gives a test or definition of which result is correct for the given inputs. To make this clearer, consider a function max that returns the maximum of two integers.

Defined explicitly, a function looks like:

1: fn max : Int x Int - Int

2: is max(x, y)

3: [delta]/=

4: if x < y

5: then y

6: else x

7: endif

Line 1 gives the signature* of the function. In this example the signature says that max takes two values of type Int and returns one value of type int. Line 2 gives names for the formal parameters of max, x and y. Line 3 introduces the body of the function definition, and says that what follows will be an algorithm to calculate the result given the inputs. Lines 4 to 7 are the explicit algorithm.

Defined implicitly, a function looks like:

  1: fn max : Int x Int  + Int
       2: is max(x, y)
       3: return larger
       4: post
       5:     (larger = x v larger = y)
       6:     ~
       7:     larger [equal to or greater than]x
       8:     ~
       9:     larger [equal to or greater than] y

Lines 1 and 2 of this definition are identical to the explicit definition. Line 3 introduces the name larger for the result. Line 4 introduces the body of the implicit definition (known as a postcondition, hence the keyword post).

A signature defines the argument types and the result type of a function.

Lines 5 to 9 are a test which is true precisely when the value larger is the correct result for the function. The implicit style can allow quite complicated functions to be defined in a simple way, without having to give an algorithm. For example, a square root function could be specified implicitly as follows:

  fn sqrt: Real -->  Real
        is sqrt(r)
        return s
        post
            r = s *  s

The square root example as given is, of course, incorrect. The square root of a negative real number is not itself a real number. A specifier has two choices here extend the definition to complex numbers or restrict the definition to nonnegative reals. A particular strength of HP-SL is its ability to restrict the scope of function definitions in a natural way. This is done by adding a precondition to the function definition. This precondition is a Boolean test that determines valid inputs to the function. In the square root example, the definition given is only valid for inputs greater than or equal to zero. Hence the corrected definition is:

  fn sqrt: Real   Real
        is sqrt(r)
        pre r [equal to or greater than] 0
        return s
        post
            r = s * s

Relations

For modeling operations on the system state, it is useful to identify the particular kinds of functions that return a Boolean result. Such functions are called relations and have a special syntax in HP-SL. For example:

  rein vowel : Char
        is vowel(c)
        [delta]/=
            c [is an element of] {'a', 'e', 'i', 'o', 'u')

defines a relation called vowel which is true just for those characters that are vowels. So the expression vowel('a') is TRUE, whereas the expression vowel('k') is FALSE. The mail system described in the article on page 32 shows how relations are used to model system operations.

Using Logic

The use of logic is pervasive in HP-SL. Logic can be used to constrain values, types, and functions to specify intended properties precisely without needing to give algorithms. The implicit form of the function definition is one way in which logic can be used.

Logic can be used to constrain value definitions by using the sat keyword. The sat is shorthand for satisfies.

val x: Int sat x > 10

val y: int sat y [is an element of] {,9,31}

This defines x to be some integer greater than 10, and y to be one of the values 1, 9, or 31.

Logic can also be used to constrain types. Consider a set of characters. To model part of a system, it may be true that these sets can never be empty. HP-SL gives a simple way of stating such constraints using the inv keyword inv is short for data type invariant).

syntype N_e_char set Set Char inv s . s =/= [{}

The s between the inv and the . is a name that represents a typical member of the type N_e_char_set. This name is used in the logical expression after the to state that all such members would be nonempty. So the set {'a', '6'} would be of type N_e_char_set but the set {} would not. The notion of invariant allows powerful statements about expected properties of systems. This aids the production and analysis of specifications.

In addition to the simple logic expressions used so far (propositional logic), HP-SL also provides predicate logic. Predicate logic extends propositional logic by introducing quantifiers that allow statements about all values of some type or about some values. The symbol V, read as "for all" or "for any," is used to make statements about all members of some type. The expression

(for every] x: Nat0 x [equal to or greater than]0)

says that: for all x of type Nat0, x [equal to or greater than] 0. Another quantifier is the symbol 3, read as "there exists," which allows statements about some values. For example., the expression

  ( [exists] x: Char   x = 'a')
  says that: there exists an x of type Char such that x = 'a'

Who Has Used Rigorous Techniques?

Rigorous methods are creating increasing interest in the software development community. The articles on pages 46 and 51 describe experiences using HP-SL on real projects at two HP divisions. HP Laboratories Bristol is also providing consulting services to HP divisions in Colorado, California, and Scotland.

Organizations outside of HP have used formal specifications in various ways. For instance, one organization used formal specifications to develop a reusable framework for a family of software products for instruments." They concluded that the application of formally based techniques in this fashion proved to be cost-effective, and the reusability of the specifications has translated into reusable components. Another organization used formal techniques as part of their reengineering efforts on a major software product.12 They used the formal notation Z, which is very similar to HP-SL, to manage the introduction of new features into the product. The specification document became a record of the commitment promised by the designer to the customer. Many software houses in Europe have successfully used formal and rigorous techniques for a wide range of applications ranging from safety-critical applications like air-traffic control to telecommunications controllers.

Introducing Rigorous Techniques into a Project

For many people, rigorous techniques represent a radically different way of approaching software development. Adopting this approach can be far from straightforward. In recognition of this problem, the software engineering department at HP Labs in Bristol has a project team called the applied methods group, or AMG, whose mission is to act in collaboration with other parts of HP to introduce formally based methods.

To date, a phased approach has been taken which starts with a small, low-risk project and develops to a more substantial collaborative project. It is important that the projects have the following features:

* Enthusiasm from the project engineers to try something new

* Full effective commitment from all the managers involved, from project manager to lab manager

* Commitment to project-centered training just before the collaborative project

* Realistic expectations of what benefits and costs are involved.

In addition, the product being developed needs to have a high chance of successful delivery to market. The collaborations aim to be at the center of the product development, not merely providing an ancillary technology. As with introducing any new technology, there are requirements on the rigorous techniques. These requirements include training, effective technical support, adequate documentation, and high-quality supporting tools that, can be integrated into the normal development environment of the project. A large part of the team's work has been to ensure that this level of support is available.

Conclusion

Rigorous software engineering is an approach that is both practical and theoretically sound. Its introduction into the software engineering community is progressing. It offers scope for substantial improvements in software, quality and productivity. In addition, the approach is likely to be developed further to support a wider range of applications.

References

1. D. Reinertsen, "Whodunit? The Search for the New-product Villers," Electronic Business, July 1983, pp. 63-66.

2. W T Ward, "Calculating the Real Cost of Software Defects," Hewlett-packard Journal, Vol. 43, no. 4, October 1991, pp. 55-58.

3. B. Cohen, W T. Harwood, and M. I. Jackson, The Specification of Complex Systems, Addison-LWesley, 1986.

4. M. Page-Jones, The Practical Guide to Structured Design, Second Edition, Yourdon Press, 1988.

5. M. Jackson, System Development, Prentice-Hall, 1983.

6. M. E. Fagan, Advances in Software Inspections, IEEE Transacons on Software Engineering, Vol. SE-12, no., 7, July 1986, pp.. 744-751.

7. G. J. Myers, The Art of Software Testing, John Wiley & Sons, 1979.

8. M. Ould and C. L Unwin, Testing in Software Development, BCS Monographs in Informatics, Cambridge University Press, 1986.

9. S.P. Bear, "An Overview of HP-SL," VDM 91 Formal Software Development Methods, lSpringer-Verlay, 1991, 00. 571-587.

10. M. R. Cagan, "The HP SoftBench Environment: An Architecture for a New Generation of Software Tools," Hewlett-packat- Jopurnal, Vol. 41, no. 3, June, 1990, pp. 36-47.

11. D. Garlan and N. Delisle, "Formal Specifications as Reusable Frameworks," VDM 90.- VDM and Z - Formal Methods in Software Development, Springer-verlag, 1990.

12. C.J. Nix and B.P Collins, "The Use of Software Engineering, Including the Z Notation, in the Development of CICS," Journal of Quality Assurance, Vol. 14, no. 3, September 1988, pp. 103-110.

Bibliography

1. S.L. Gerhart, Applications of Formal Methods: Developing Virtuoso Software," IEEE, Software, September 1990, Vol. 7, no. 5, pp. 6-10.

2. A. Hall,"seven Myths of Formal Methods," IEEE Software, September 1990, Vol. 7, no. 5, pp. 11-20.

3. I. Hayes, Specification Case Studies, Prentice Hall Intemational, 1990.

4. C.B. Jones, Systematic Software Development Using VDM, Prentice Hall International, 1986.

5. C.B. Jones and R.C. Shaw,. Case Studies in Systematic Software Development, Prentice Hall International, 1990.

6. B. Meyer, "On Formalism in Specification," January 1985, Vol. 2, no. 1, pp. 6-26.

7. J.M. Wing, "A Specifier's Introduction to Formal Methods," IEEE Computer, Vol. 23, no. 9, September 1990, pp. 8-24.

COPYRIGHT 1991 Hewlett Packard Company
COPYRIGHT 2004 Gale Group