[Prev][Next][Index]

"protective" specs


Gary is too generous in citing my thesis as a reference.  Section
5.1.4 of my thesis introduces the notion of a "protective"
specification that is somewhat related to this thread of discussion on
"LSL boolean ... undefined terms."  An interface specification is
protective if it is independent of the exempt terms of its used trait.
The intention is that you'd strengthen the pre-condition to protect
yourself from dealing with those exempt terms that you might encounter
in the post-condition.  For example, you'd add a pre-condition (like
s ~= empty) to the POP-STACK interface so you don't have to deal with
the LSL term pop(empty) in the post-condition.