For more information on NIST efforts in high integrity software, see http://hissa.ncsl.nist.gov/.
NIST-QIS is available free of charge, but before downloading and using, please read the Software User Agreement. Any use of NIST-QIS constitutes acceptance of the terms in the Software User Agreement.
Program correctness statements are used by programmers to assert conditions which are to be met at a given point in a program. Program correctness statements improve program quality by providing for the immediate notification and location of program behavior outside of constraints set by the programmer. Such notification can be enabled as programs are run in production after testing is complete. Furthermore, by developing correctness statements as a program is developed, the programmer reaches a deeper understanding of how the program is to function. Thus, many programming errors are eliminated before any testing begins.
In NIST-QIS, program correctness statements are extensions to the syntax of Java comments. The syntax is:
/*VERIFY <Expression> */
and:
//VERIFY <Expression>
where "Expression" must have a boolean type.
The NIST-QIS tool qis_tool.java is a preprocessor which takes Java applets with NIST-QIS correctness statements and produces normal Java syntax which can be compiled using the JDK from Sun. The NIST-QIS tool inserts additional Java code at the location where the correctness statements appear. The code inserted consists of calls to a method in the class qis.java. When the applet runs, the expression is evaluated and the default behavior is to log an exception to the standard error stream "err" if the expression evaluates false.
Optionally, a control panel can be configured by the NIST-QIS tool. By means of the control panel, which appears when the first false correctness statement is encountered, the applet can be directed to log nothing, log only true expressions, or log both true and false expressions. The control panel also permits a stack trace to be logged along with true expressions and/or false expressions. The control panel allows NIST-QIS to be used to trace execution paths. Note that if the control panel window is quit, there is no way to make it return without restarting the applet. The information logged after the control panel is quit is that which was set on the control panel before it was quit.
A csh script nist-qis. is provided to use NIST-QIS with the JDK. If one has an html file which references the applet "java_applet.class", the NIST-QIS source file would be "java_applet.qis". the output of qis_tool would be "java_applet.java", and the output of the Java compiler (javac) would be "java_applet.class". The NIST-QIS script has the following usage:
%nist-qis java_applet%nist-qis -p java_applet%nist-qis -n NIST-QIS has been tested with Sun's SortDemo from James Gosling and with Life from Josh Marketos. To see the results, try SortDemo and Life with NIST-QIS correctness statements added. Please note that the correctness statements added to these applets were for the purposes of testing NIST-QIS and illustrating its use. They are not intended to be an adequate set of correctness statements for either Life or SortDemo. The Life.qis, Life.java, BubbleSortAlgorithm.qis, BubbleSortAlgorithm.java, BidirectionalBubbleSortAlgorithm.qis, BidirectionalBubbleSortAlgorithm.java, QSortAlgorithm.qis, QSortAlgorithm.java files produced during the testing of NIST-QIS may also be seen.