Subject: "protective" specs
From: firstname.lastname@example.org (Jeannette Wing)
Date: 25 Jul 1995 21:28:38 GMT
Organization: Carnegie-Mellon University, School of Computer Science
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.