The axiom file describes the behavior of the ADT that is being tested. More specifically, the axiom file specifies what tests will be conducted on the ADT. Obviously, the better the ADT is described, the more confident the user can be in the quality of the code. For specific details on how to rigorously define an ADT's behavior using axia, take Comp 204, if you haven't (or aren't in the process of) taken it already.
The axia are defined using the signatures and alii described in their own respecive files. Spacing and linefeeds are ignored, so the user can space things out for easy readability. Here is an example of the description of one axiom:
nodedel_new
equalIsh (nodeDel (newPetrinet (), NodeId nid1),
newPetrinet ())
The description of an axiom begins with its name. Each axiom must have a unique name, so that in the almost-unheard-of event of a bug, Danish can report which axia failed. Next comes the expression of the axiom, which must return a boolean at the lowest level. The expression may consist of any known method (described in the signatures file), constants (including any alii), or free variable.
Free variables act as instances of a data type, and variables must be declared as belonging to a specific type at least once in the file. This is done by prefixing an occurence of the free variable with its type. When Danish is run, the free variables are replaced by specific values from the vector file. A free variable is guaranteed to keep the same value within an axiom during each test of that axiom, but will not retain the same value for different axia or tests. The variable must belong to the same data type throughout the file - it cannot be declared as an int for one axiom and a char for another.
When Danish is run, each axiom will be tested using every possible combination of test vector assignments to the free variables. The left-hand side of the axiom (lvalue) is then compared to the right-hand side (rvalue) using a method that returns a boolean. Such a method may have to be written into the Java class file if Java does not provide a suitable one. (For example, the "==" operator can tell if two integers are equal, but probably not two instances of the ADT being tested.) If the result of the comparison between the lvalue and rvalue is 'false', the axiom has failed, and the user must return to the bit mines to code some more. In this case, if the verbose option is enabled and a printing method is supplied, the values of the lvalue and rvalue are displayed. If the result is 'true', the ADT gets a hearty pat on the back before being put through more tests.
The axia that appear in this manual are for format demonstration purposes only. Examples are not meant to be complete. It is up to the user to determine the full set of axia necessary to describe the behavior of a given class.
It is extremely important to be careful when forming your axia, because Danish cannot tell the difference between an error in an axiom and an error in your Java class code -- it can only report whether the two are consistent.
Previous Topic
Next Topic