that, perhaps inadvertently, raises an interesting point. (Someone may want to post this on
Newbie question: Verification of my formal spec + test against specific cases
Hi everybody,
here´s a newbie question: So I was wondering if I specify a system with TLA+ or PlusCal and then run the model checker to verify it, does it make any sense to test against specific input/cases?
Given that I have a spec of a system in TLA+ or PlusCal, can I test against specific inputs/test cases at all?
Thank you!
One thing that can limit the usefulness of TLA+/TLC and other verification tools
is the difficulty of creating test inputs. For example, I advocate (and practice)
specifying nontrivial pieces of code such as a Java method. If the method is
complex or subtle enough, it might warrant a TLA+ or PlusCal specification.
However, that often is not worth the effort because testing the spec is difficult
for the following reason: A piece of a program operates on data structures that
have been produced by other parts of the program. Writing examples of the TLA+
representation of those data structures is often a lot of work. It might still
be worthwhile to write a TLA+/PlusCal spec to make sure that I understand what
the method should do before I write the code, but the amount of testing I can do
is often only enough to catch "coding errors" in the spec, not basic design errors.
If the piece of code is important enough to really test its design, one
approach is to write a program to produce the TLA+ representation of
the data structures manipulated by that piece of code. This is done by
inserting the necessary code in the program being written at the place where
the piece of code is executed. One place I did that is in checking a TLA+ spec
of the PlusCal to TLA+ translator. I produced a version of the translator
that, after parsing the PlusCal algorithm, generated a TLA+ module consisting
of the TLA+ spec of the translator with an initial condition that gave
the PlusCal algorithm as its input. The translator then took the result
generated by running TLC on the spec (output by the spec using the Print operator)
and used it as the translation in the module it produced. I could then run
TLC on the algorithm produced by that translation and by the ordinary translation
and compare their outputs. I was thus able to test the actual translation against
the TLA+ spec of the translation on actual PlusCal algorithms. At some point I stopped
updating the TLA+ spec to keep up with features added to PlusCal. However, for
algorithms that don't use those added features, it still works. To compare its
output with that produced by the translator, one has to run the translator with
the appropriate -version option.
Leslie