2011年9月20日星期二

Practical Advice on Writing Pre- Post-Conditions for Real Programs

http://www.cs.wright.edu/~pmateti/Courses/433/Notes/prepost-notes.html


Practical Advice on Writing Pre- Post-Conditions for Real Programs



Prabhaker Mateti



Large programs should have pre + post conditions for every major
routine.  Unfortunately, this is not the practice of the industry
(yet).  It is, nevertheless, required in our class room work.


We use the word "routine" as a generic term for procedures and
functions. As you know, a function is a routine that has no side effects, and
returns a value to the caller. Functions, by this definition, do not alter the
values of any global variables, files, or arguments. Whereas the sole purpose of
a procedure is to have a side-effect.



Pre-condition



The pre-condition should be written so that if we "evaluate" it,
the resulting value will be either the Boolean True or False.  It is a
statement by the programmer that a given routine should not be entered unless
its pre-condition is guaranteed.  If it is entered anyway, the routine may
behave erratically.  Obviously, the pre condition does not talk about
variables etc that are local to the routine.  It talks about all relevant
globals, and the input arguments. 


Ideally, the pre condition is a strictly Boolean expression possibly using
the for-all or there-exists quantifiers.  When this is difficult to
express, write it out as an English sentence, but with great care in its
construction so that no ambiguity or imprecision results.  We would like
the pre-condition to be as weak as possible; i.e., it describes the input
requirements of the routine in as general a way as possible.



Post-condition



The post condition of a routine describes the accomplishments of the
routine.  It should be written so that if we "evaluate" it, the
resulting value will be either the Boolean True or False. The results described
in the post condition need only be accomplished provided the routine was called
with its pre-condition being satisfied.  Obviously, the post condition
talks about all relevant globals, and the input arguments and relates them to
the output results.  In doing so, it is permitted to refer to the values
the globals and the input variables had at the time of entry into the
routine.  It generally does not talk about variables etc that are local to
the routine because the caller of the routine can only depend on the results
delivered  and the globals affected.


Ideally, the post condition is a strictly Boolean expression possibly using
the for-all or there-exists quantifiers.  When this is difficult to
express, write it out as an English sentence, but with great care in its
construction so that no ambiguity or imprecision results.  We would like
the post-condition to be as strong as possible; i.e., it describes the
properties of the output of the routine in as narrowly as possible.


Signatures


The signature of a routine says quite a bit in the sense of pre post
conditions. It declares the types of variables, and hence type requirements need
not appear in the pre post conditions. When you declare a formal parameter as a
value parameter, you are saying that its value at the end of the routine is by
itself of no significance, and the actual argument for it is unchanged. When you
declare it as a var (or
in-out) parameter, you are saying that the routine is expected to change its
value as seen by the caller.


Procedures and Functions that Alter Globals


Procedures often alter global variables whose names are not passed in as
actual arguments. The signature of a procedure as declarable in the typical
programming language does not make clear which globals are accessed and/or
modified. The specifications of such procedures should list all such variables,
and describe their values before and after a call to the procedure. If the
variable name is x, we can use face="Lucida Console" size="2">x0, or size="2">old-x, to stand for the value it had immediately upon entry into
the routine.


Frequently, we have a file that declares many globals. Not all of them are
manipulated by a routine. So, adopt the following convention. If a post
condition is silent regarding a global, we assume that it is actually asserting
that that global is-Unchanged by that routine. Some time a routine may not only
read but also actually update the value of global in between but finally leaves
its value as it was upon entry. In this case, silence is unacceptable, and we
should explicitly state that the global is unchanged.


Robustness Tests


Consider the following code:



int f (T x) {
int r;
if (! bexp(x))
return -1;
... more code ...
... r is defined so that r >= 0...
return r;
}



This is typical of many functions. Some checking of the given value of face="Lucida Console" size="2">x is made. The function is checking its
precondition in order to improve its robustness. If it does not pass this test,
i.e., bexp(x) is
false, the routine quits. This is often indicated to the caller by returning a
value that is outside the "legit" values, in this example a -1. In
other examples, you might see a panic()size="2"> routine being called.


Q: Is bexp(x) a precondition of face="Lucida Console" size="2">f() or not?


A: Strictly speaking it is not -- because the routine "works"
whether bexp(x) is true or not.  Strictly speaking, the preconditions were
"none", expressed logically as pre: TRUE.  But, realistically, it
is a precondition of f().  The programmer of f() included that test because
of uncertainity that f will be called only in those situations with bexp()
guaranteed.  This is typical of intermediate level routines in packages to
improve robustness.  Typical lower level routines omit such test because of
the execution  overhead of the test adds to the functionality of the
routine.  In such cases, the responsibility of verifying that the
precondition holds rests with the caller of the routine.


Some Useful Predicates


We list some predicates that we can think of as being predefined. These are
useful in post conditions.



V is-defined asserts that a legitimate value
from the domain type of v has been assigned to the variable face="Lucida Console">v after its declaration. face="Lucida Console" size="2">V is-undefined is
the same as not (V is-defined).


V is-unchanged asserts that the variable v has a
value at the point of return which is the same as it was at the point of entry.



P is-malloc-returned asserts that the pointer
value stored in the variable p is a value
returned by the routine malloc. You can create many other similar predicates by
using the names of other functions in place of malloc.

没有评论:

发表评论