them attractive to researchers, that more usable tools and techniques for
“lightweight” formal methods will emerge, and will enable more practitioners
to reap their benefits at a reasonable cost. The use of formal specifications can
result in fewer requirements errors. This benefit may exist, as Bertrand Meyer