Re: Pre-condition vs. Post-condition

[brad@terminus.umd.edu (Brad Balfour)]

In article <jls.669368339@rutabaga>
jls@rutabaga.Rational.COM (Jim Showalter) writes:
>>procedure pop(s: stack)
>>begin
>>   if(not empty(s)) then
>>      -- pop the stack
>>   else
>>      raise underflow
>>end pop;
>>procedure pop(s: stack)
>>begin
>>   stack.top := stack.top - 1;
>>   exception
>>      when Constraint_Error => raise underflow
>>end pop;
>Note that in the second case the procedure is faster, since it doesn't
>have to do the check first. Not only is it faster, it is safer, since
>without using tasks you cannot guarantee that between the time you
>checked and the time you popped it hadn't been popped elsewhere. For
>both of these reasons, I'd say the second version is far better than
>the first version, and that the original poster's thesis that exceptions
>should be used rarely if ever has been contradicted by the very examples
>provided to support his/her case!

   It should be kept in mind, however, that the first example will always
produce correct results (except in the presence of tasks where it should
be replaced with a concurrent component), but that the second example breaks
in the presence of a "pragma supress". However, on most compilers, it is
not necessary to change the code to get this effect. Instead, all one has
to do is add a switch to the compiler run to turn off the constraint checks.
Then, push will trash memory randomly and pop will return garbage rather
than raise underlfow.

   Also, the second example is not safe in the presence of multiple tasks.
It is possible for a second thread of control to be changing the contents of
the stack at the same time as the first so that between the read of
stack.top and the computation of the -1 and then the assignment there
are plenty of opportunities of the push to change (and write to) stack.top.
It is a mistake to assume that the line "stack.top := stack.top - 1;" is a
single atomic assignment.




Brad Balfour
EVB Software Engineering, Inc.
brad@terminus.umd.edu