1. A list of the names (and total percentage) of routines
in the library with multiple output parameters.
2. A list of the routines in the library.
3. A list of subroutines in the library which are directly
referenced in the domain model. A direct reference is a
subroutine which is explicitly listed in the domain
model.
4 A list of subroutines indirectly referenced in the
domain model. An indirect reference is a subroutine
whose call is not explicitly indicated in the domain
model but which is transitively invoked by one of the
subroutines explicitly indicated in the domain model.
5 A list of subroutines which can not be invoked under
any circumstances through the domain model.
6 Calls to library routines which supply a constant as a
parameter to the routine as opposed to a variable. This
could represent an incompleteness (or a possible redun-
dancy with other axioms) in that the axiom could be
more general.
7 Detect dead-end dataflows in the proof. Some library
routines could return values which are not ever used by
the caller. These represent dead-end dataflows. They
could be incompletenesses in the domain model. To
detect them we would need to know how calls are
sequenced in typical proofs generated from the axioms.
Can some knowledge of the proof strategy axioms help us
out here?
8 Detect and report pre-condition checks in the library.
A pre-condition check will manifest itself as a condi-
tional call to an exception handler which depends
solely upon input values. Since the domain axioms are
known to be weak wrt expressing complete pre-
conditions, we expect that most anything we find here
will be an incompleteness.
January 19, 1995
-- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Kurt Stirewalt (kurt@cc.gatech.edu | kswalt@mitre.org) % % Georgia Tech Software Engineering Research Center. Atlanta, Georgia. % % "Not tonight honey, it's darts night" % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%