Overview
Two recent trends point to a practical and effective way of
detecting and avoiding errors in software: (1) the widespread use of
programming languages with strong type systems; (2) software tools that are able
to statically or dynamically identify errors in programs. Both efforts narrow
the gap between the rich knowledge in a programmer's head and the impoverished
textual description of programs. If programmers provide redundant descriptions
of aspects of a program's intended behavior, compilers and other tools can check
that the program conforms to these specified aspects. The approach of checking a
program against a partial specification faces a number of open and challenging
research problems:
 | What should a programmer be able to specify and how?
How can these descriptions be made accessible and' meaningful?
|
| What are efficient and effective techniques for
checking these specifications against program texts? |
| With partial checkable specifications can we improve
the maintenance and evolution of software? |
|
What's New?
|
