ftp.umcs.maine.edu/2015-02-07.ftp.umcs.maine.edu.tar/ftp.umcs.maine.edu/pub/WISR/wisr6/proceedings/ascii/yakhnis.ascii

Text File | 1993-10-19 | 16KB | 307 lines

    Yakhnis - 1


Reusing Program Derivation Techniques and
Correctness Proofs via Generic Algorithms


Vladimir R. Yakhnis

Tel: [phone]
Email: [e-mail]

Joel A. Farrell

Tel: [phone]
Email: [e-mail]

Steven S. Shultz

Tel: [phone]
Email: [e-mail]

IBM Corporation
Dept. G37/16-3
1701 North Street
Endicott, NY 13760
Fax: [phone]


Abstract

We suggest that the notion of reuse be extended to Dijkstra-Gries
techniques of deriving programs from their specifications.  The formal
derivation and proof of programs as is practiced today is a very powerful
tool for the development of high quality software.  However, its application
by the software development community has been slowed by the amount of
mathematical expertise needed to apply these formal methods to complex
projects and by the lack of reuse within the framework of program
derivation.  To address these problems, we have developed an approach to
formal derivation that employs the new concept of generic algorithms.  A
generic algorithm is an algorithm which has 1) a formal specification; 2) a
proof that it satisfies this specification; and 3) generic identifiers
representing types and operations.  Using them, most software developers
need to know only how to pick and adapt generic algorithms, rather than
perform more technically challenging tasks such as finding loop
invariants and deriving loop programs.  The adaptation corresponds to
replacing the generic identifiers by concrete types and operations.  In
addition, this new methodology provides the developer with a form of reuse
of program derivation techniques, correctness proofs and formal
specifications.

Keywords: program derivation, proof of correctness, generic algorithm,
formal specification

Workshop Goals: discussing reuse of derivation techniques, correctness
proofs and formal specifications, discussing application of generic
algorithms within the framework of object orientation

Workshop Groups: reuse and formal methods, reuse and OO methods, tools
and environments

1    Introduction
The program development approach taught by the Dijkstra-Gries school is also
known as ╥calculational╙.  Indeed, as illustrated in [6], the best beginner's book
on the subject, programs could be calculated from the specifications in a
rigorous and elegant way.  In [15], a book intended for intermediate and
advanced students, many difficult programs are calculated from the
specifications.  Of course, anyone interested in the subject should also look
into classical [10].
Since the DO-loop is the most difficult programming element, this school
mostly concentrates on extracting ╥candidates╙ for the loop invariants from
the specifications.  Once a good candidate is found, the loop guard and the
loop body are ╥calculated╙ around it.  If the calculation is unsuccessful,
another candidate will be sought.  This methodology is very powerful.
However, it is not free of disadvantages:
1)    To efficiently utilize the methodology, one has to have certain
mathematical skill.  An ability to prove simple logical assertions may not
be enough;

2)    When reasoning about the program on the level of invariants a great deal
of programming intuition is lost.  For instance, while looking into the
elegant Kaldewaij's solution of maxsegsum problem, one could have a
╥gut╙ feeling that we are dealing with a recursively defined function.  But
it is never explicitly seen behind the manipulations with formulas;

3)    As presently taught, the methodology requires application of the same
detailed technique again and again, though for different programs.  In
deriving programs, one could often see that exact same thing was already
done before, but there is no way given to ╥reuse╙ it.  It is especially
obvious with ╥tail recursion╙ and ╥search by elimination╙ techniques
discussed in [15].
Recently an interesting work by J. Bohorquez and R. Cardoso (see [4])
addressed the second disadvantage by providing intuitive motivation for some
of the techniques for extracting the loop invariants and by making them more
general.  However this work did not address the first and third disadvantages.
Our new methodology ╥deriving programs using generic algorithms╙ extends
the Dijkstra-Gries methodology and is designed to overcome all three
disadvantages as follows.

1)  A number of pre-proved program templates supplied with invariants and
bound functions frees the practitioner from looking for the invariants.  We
call these templates ╥generic algorithms╙.  With the generic algorithms an
ability to prove simple logical assertions may be sufficient;

2)  Generic algorithms enhance the intuition.  For instance, the maxsegsum
problem is easily solved by an intuitively clear generic algorithm for
computing recursive functions.

3)  Generic algorithms allow reuse of program derivation techniques,
correctness proofs and formal specifications.  For instance, ╥tail recursion╙
and ╥search by elimination╙ techniques were converted into generic
algorithms.

2   Background
The notion of a generic algorithm as a tool intended to augment the
traditional program derivation techniques (see [6,10], etc.) was born in the
beginning of 1992 when the Endicott Programming Laboratory (EPL), IBM
Corporation, began investigating the use of formal methods to help improve
the quality of our commercial software products.  Since then we have taught
classes on formal methods and generic algorithms within the framework of IBM
Education System and successfully applied the approach for proving
correctness of one of the crucial parts of the CMS multitasking system.
The basis of the CMS multitasking system is the notion of a ╥thread╙.
Informally, a thread is a part of a program that a) has a logically independent
goal and b) runs concurrently with other parts of the same program or with
other programs.  One of the key components of the CMS thread management is
a module called ╥HighestPriorityRunnable╙.  Informally,
HighestPriorityRunnable finds the highest priority runnable thread from a
given set of threads.
We created a formal specification for HighestPriorityRunnable by isolating the
part of system state which interacts with HighestPriorityRunnable.  Having
done so, we looked at our library of generic algorithms for an algorithm with a
similar specification and chose one called
╥Choice_Based_Filtered_Bounded_Search╙.  This generic algorithm not only
applied easily to HighestPriorityRunnable, but produced a particularly elegant
and efficient solution to the problem.  For complete information on the formal
specification of HighestPriorityRunnable, and the refinement based on
╥Choice_Based_Filtered_Bounded_Search╙ see [21].
We summarized our results in three papers, [20,21,22].  Presently we are
working on the application of our approach within a new development project,
as well as on helping other developers throughout the EPL set up pilot projects
to utilize the generic algorithms.

3    Position
Our purpose is to ╥hide╙ most of the mathematical techniques involved in
program derivation in a number of pre-derived program templates that we call
generic algorithms.  A generic algorithm has the following features
Ñ    a formal specification;

Ñ    it is formally proven to satisfy this specification;

Ñ    it may have one or more generic identifiers representing data types or
operations;

Ñ    it may have embedded program specifications or pseudocode
instructions describing the next steps in the stepwise refinement process.
We have created a library of generic algorithms that implicitly contains many
techniques of program derivation converted into generic algorithms, as well as
generic algorithms not corresponding to a single such technique.  Some of our
generic algorithms were developed using the Dijkstra-Gries methodology and
the rest were derived using our extension of the Dijkstra-Gries methodology.  So
far we have about 30 algorithms in our library.  On the basis of our
development experience and by working through numerous examples in such
classical textbooks as [6,10,15], we became convinced that our library covers
most of the DO-loops a programmer could conceivably encounter in everyday
work.
In [22] we list the library of generic algorithms in Dijkstra-Gries notation.  The
work of converting them into other languages is underway.  We present below a
part of the table of contents from [22]:
1.0  Computation of Recursive Functions Using DO-loops
    1.1  Simple Recursive Function
    1.2  Finite Memory Recursive Function
    1.3  Tail Recursion

2.0  Searches
    2.1  Search by Elimination
    2.2  Searches with Quantifiers
        2.2.1  General Quantifiers
            2.2.1.1  Unbounded
            2.2.1.2  Bounded
        2.2.1  Boolean Quantifiers
            2.2.1.1  Unbounded
            2.2.1.2  Bounded

3.0  Logarithmically Efficient Algorithms
    3.1.  Binary Search
    3.2.  Binary Iteration
With the advent of the library of generic algorithms the program derivation
process could be ideally represented as follows.  We start from a formal
specification and view it as an algorithm consisting of a unique pseudocode
instruction.  The process of derivation consists of several stages, each resulting
in an algorithm having more detail than the previous ones.  We may stop
either when the algorithm becomes a compilable program or before that.  In
either case the resulting algorithm will satisfy the initial specification.  Each of
those stages consists of one or more iterations of the following steps:
1.    Choose a pseudocode instruction from the algorithm created in the
previous stage.  (Recall that every such instruction corresponds to a
formal specification that encodes a certain behavior during execution);

2.    Find a generic algorithm in the library that might be doing similar work;

3.    Adapt the generic algorithm by replacing its abstract types, operations
and variables by the related types, operations and variables from the
pseudocode instruction.  Adapt the specification of the generic algorithm
by the same replacement of types, operations and variables;

4.    Justify that the adapted specification from step 3 correctly implements
the specification of the pseudocode instruction.  [20] provides an
explanation of how to do it in a simple 3-step procedure.  If the
justification fails, go back to step 2;

5.    Replace the pseudocode instruction in the algorithm created in the
previous stage by the algorithm from the step 3.

4    Conclusion
Generic algorithms serve as reusable, transformable ╥building blocks╙ in the
formal derivation of programs.  They extend the paradigm of program reuse to
the reuse of program derivation techniques, program correctness proofs, formal
specifications and design steps.  Generic algorithms alleviate the problem of
mathematical skill levels by freeing the programmer from the search for loop
invariants and from providing respective interim proofs.  Thus they enable
programmers to derive mathematically correct programs from a formal
specifications with only occasional need to consult experts in program
derivation and program correctness proofs.  This methodology is applicable to
a vast segment of the program development process, from high level design to
coding.



References
[1]    K. R. Apt, ╥Ten Years of Hoare's Logic, a Survey╙, ACM Trans. on Prog.
Lang. and Sys., 3, 431-483 (1981).
[2]    R. Apt, E. R. Olderog,  Verification of Sequential and Concurrent Programs,
Springer-Verlag, 1991.
[3]    R. C. Backhouse, ╥Program Construction and Verification╙, Prentice-Hall,
1986.
[4]    J. Bohorquez, R. Cardoso, ╥Problem Solving Strategies for the Derivation of
Programs╙, to appear in Logical Methods, a collection of papers honoring
A. Nerode's 60th birthday.
[5]    T. Clement, ╥The Role of Data Reification in Program Refinement: Origin,
Synthesis and Appraisal╙, The Computer Journal, vol. 35, num. 5, October
1992.
[6]    E. Cohen, Programming in the 90s: An Introduction to the Calculation of
Programs, Springer-Verlag, 1990.
[7]    E. W. Dijkstra, A Discipline of Programming, Prentice Hall, 1976.
[8]    E. W. Dijkstra, W. H. J. Feijen, A Method of Programming, Addison Wesley,
1988.
[9]    E. W. Dijkstra, C. S. Scholten, Predicate Calculus and Program Semantics,
Springer-Verlag, 1990.
[10]    D. Gries, The Science of Programming, Springer-Verlag, 1981.
[11]    C. A. R. Hoare, ╥An Axiomatic Basis for Computer Programming╙, CACM
12, 1969.
[12]    C. A. R. Hoare, ╥An Axiomatic Approach to Computer Programming╙, in
Essays in Computer Science, C. A. .R. Hoare and C. B. Jones (eds), Prentice-
Hall, 1989.
[13]    D. C. Ince, An Introduction to Discrete Mathematics and Formal System
Specification, Oxford University Press, 1988.
[14]    C. B. Jones, Systematic Software Development using VDM, Prentice-Hall
International 1990.
[15]    A. Kaldewaij, Programming: The Derivation of Algorithms, Prentice Hall,
1990.
[16]    J. Loeckx, K. Sieber, The Foundations of Program Verification, John Wiley
& Sons, 1987.
[17]    C. Morgan, Programming from specifications, Oxford University Press,
1991.
[18]    J. C. P. Woodcock,  ╥The Rudiments of Algorithm Refinement╙, The
Computer Journal, vol. 35, num. 5, October 1992.
[19]    J Woodcock, M Loomes, Software Engineering Mathematics, Pitman, 1988.
[20]    V. Yakhnis, J Farrell, S Shultz, ╥Deriving Programs with Generic
Algorithms: An Overview╙, to appear in IBM Systems Journal.
[21]    V. Yakhnis, J Farrell, S Shultz, ╥Deriving Programs with Generic
Algorithms: The Approach and a Case Study╙, to appear.
[22]    V. Yakhnis, J Farrell, ╥The Library of Generic Algorithms in Dijkstra-Gries
Notation╙, to appear.
5    Biography
Vladimir R. Yakhnis is an advisory programmer in the IBM Endicott
Programming Laboratory.  He received a Diploma in mathematics from Moscow
State University, Moscow, Russia in 1975.  He worked as a computer
programmer in Moscow, Russia and Houston, Texas.  Dr. Yakhnis received a
Ph.D. in mathematics and an M.S. in computer science from Cornell
University, Ithaca, New York in 1990.  He worked as a Postdoctoral Fellow at
Mathematical Sciences Institute, Cornell University until 1991.  His research
was in program correctness for concurrent and sequential programs, winning
strategies for two person games, finite automata and recursion theory.  Dr.
Yakhnis joined IBM in 1991 in Endicott.
Joel A. Farrell is a senior programmer at the IBM Endicott Programming
Laboratory in Endicott, New York.  He joined IBM in Endicott in 1981 in VM
Development where he has worked on such areas as I/O and program
management.  Most recently he has been involved in parallel and distributed
computing and in formal methods for software development.  Mr. Farrell
received his BS degree in computer science from Kansas State University in
1980 and his MS degree in 1985 from Syracuse University, also in computer
science.  In 1992 he received an IBM Outstanding Innovation Award for his
work on parallel processing in CMS, and an IBM First Level Invention
Achievement Award.  He is a member of the Association for Computing
Machinery.
Steven S. Shultz is an advisory programmer at the IBM Endicott Programming
Laboratory in Endicott, New York.  He joined IBM in Endicott in 1981 in VM
Development where he has worked on such areas as I/O and virtual storage
management. Most recently he has been involved in parallel and distributed
computing and in formal methods for software development.  Mr. Shultz
received his BS degree in Computer and Information Science from Ohio State
University in 1981.  In 1992 he received an Outstanding Innovation Award for
his work on parallel processing in CMS, and an IBM First Level Invention
Achievement Award.