Next: Conclusions and Future Up: VIS : A System Previous: Algorithms
One of the key goals of VIS is to serve as a platform for developing new verification algorithms. We have used as our model the object-oriented programming style of SIS. VIS is composed of 18 packages; each exports a set of routines for manipulating a particular data structure, or for performing a set of related functions (e.g., there are packages for model checking, variable ordering, and manipulating the network data structure). New packages can be added easily. This wealth of exported functions can be used by future programmers to quickly assemble new algorithms. All functions adhere to a common naming convention so that it is easy to find functions in the documentation.
Particular attention was paid to the design of the interfaces to packages that are still the subject of ongoing research (e.g., MDD variable ordering, image computation, and partitioning). This makes it easy for other researchers to plug in their algorithms for performing a particular task, and then evaluate their algorithm within the context of VIS.
Extensive user and programmer documentation exists for VIS. The creation of this documentation was aided by the tool ext , which extracts documentation embedded in the source code. For each function, the programmer provides a synopsis and a complete description, and ext automatically extracts this information, along with the function name and argument types, into an HTML file that can be viewed on the World Wide Web. Documentation for user commands is extracted in a similar fashion.
Thu Feb 8 16:55:08 PST 1996
|©2002-2018 U.C. Regents|