Pre- and post-conditions (was Commenting code) 
Author Message
 Pre- and post-conditions (was Commenting code)

Quote:

>To me, the pre/post-conditions are the major thing; the implementation is
>just a commentary to the pre/post-conditions.  The pre/post-conditions are
>the real theory; the implementation is just a special case, given here as an
>example to this theory.

        I think the Eiffel and Sather languages take this a
step further.  Pre- and post-conditions are part of the
procedure declaration, methods can inherit these invariants,
and an exception will be raised if a condition is violated.  
        Oberon can emulate these features, and I wonder how
valuable they have turned out to be for other programmers.  
Though great in theory -- this is often how programs are
formally specified -- I wonder how useful built-in pre- and
post-conditions turn out to be in practice, since many formal
assertions cannot be practically checked at run-time.  (I'm
cross-posting this to Eiffel and Sather newsgroups.)


Wed, 18 Jun 1997 11:23:05 GMT  
 Pre- and post-conditions (was Commenting code)

:         Oberon can emulate these features, and I wonder how
: valuable they have turned out to be for other programmers.  
: Though great in theory -- this is often how programs are
: formally specified -- I wonder how useful built-in pre- and
: post-conditions turn out to be in practice, since many formal
: assertions cannot be practically checked at run-time.  (I'm
: cross-posting this to Eiffel and Sather newsgroups.)

Practically, the most useful element of programming by contract is
enforcement of preconditions. It is also unclear what kind of 'formal'
assertions cannot be checked at run time. What did you mean?

As for class invariants, they are very interesting in theory, but sometimes
presence of invariants can simply point to redundancy of data. Of course,
sometimes they can impose useful  limitations on class data.

--
Happy Holidays!
----------------------------------------------------------------------------
IMHO. Igor Chudov,      Resource Solutions Intl         office (918)588-2309
Systems Engineer,       for WilTel.                     home   (918)585-5862

                                          http://m-net.arbornet.org/~ichudov
                                     1819 South Jackson #32-P Tulsa OK 74107

                 f u cn rd ths, u cn gt a gd jb n cmptr prgrmmng.



Thu, 19 Jun 1997 05:09:58 GMT  
 Pre- and post-conditions (was Commenting code)

Quote:


> :         Oberon can emulate these features, and I wonder how
> : valuable they have turned out to be for other programmers.  
> : Though great in theory -- this is often how programs are
> : formally specified -- I wonder how useful built-in pre- and
> : post-conditions turn out to be in practice, since many formal
> : assertions cannot be practically checked at run-time.  (I'm
> : cross-posting this to Eiffel and Sather newsgroups.)

> Practically, the most useful element of programming by contract is
> enforcement of preconditions. It is also unclear what kind of 'formal'
> assertions cannot be checked at run time. What did you mean?

Most assertions can be checked, but it may not be practical to do so.  For
example:

An assertion that an object is the head of a valid doubly-linked list. To
check that, we need to walk the entire list.

An assertion that states that the contents of a buffer match the data on
disk. We don't want to read from disk every time to check that.

An assertion that a value is the smallest root of an equation. You can
certainly check that it is a root, but the smallest part is a little messy
to check depending on the equation.

An assertion that a buffer contains an accurate recording of what the user
has typed. To check that, you'd have to save a list of the user's
keystrokes somewhere else. (And, of course, that introduces a new data
structure with a related assertion...)

Basically, pretty much everything you might want to assert is probably
checkable, but the expense of checking it in terms of runtime or extra
storage required to track the events which got us to a particular state can
be prohibitive much of the time. (Of course, that's part of what compiler
or runtime switches are for.)

Quote:

> As for class invariants, they are very interesting in theory, but sometimes
> presence of invariants can simply point to redundancy of data. Of course,
> sometimes they can impose useful  limitations on class data.

Of course, the double-links above are a form of redundancy. But they are a
redundancy that can make a huge difference in operating time for some
algorithms.

Mark Hamburg
Adobe Systems, Inc.



Thu, 19 Jun 1997 07:37:49 GMT  
 Pre- and post-conditions (was Commenting code)

Quote:




>> :         Oberon can emulate these features, and I wonder how
>> : valuable they have turned out to be for other programmers.  
>> : Though great in theory -- this is often how programs are
>> : formally specified -- I wonder how useful built-in pre- and
>> : post-conditions turn out to be in practice, since many formal
>> : assertions cannot be practically checked at run-time.  (I'm
>> : cross-posting this to Eiffel and Sather newsgroups.)

>> Practically, the most useful element of programming by contract is
>> enforcement of preconditions. It is also unclear what kind of 'formal'
>> assertions cannot be checked at run time. What did you mean?

>Most assertions can be checked, but it may not be practical to do so.  For
>example:

>An assertion that an object is the head of a valid doubly-linked list. To
>check that, we need to walk the entire list.

[rest of the good 'hard' assertion examples deleted]

The idea in Oberon and C and C++ is that the caller had damn well better
get the preconditions right.  If the preconditions are not right, the
software is not guaranteed to work.

Oberon/F actually checks (at least) some of the assertions, because they
have a trap viewer which specifically says something like 'precondition
violation'.

My own philosophy moves between checking and not checking, so it would
not be fair to declare one way is better than another -- in essence, the
result is the same: procedure failure -- it's just how it gets reported
that is different.

[It's interesting how a thread on commenting has degenerated into a small
rwar on preconditions, postconditions & copyright law]

I am personally tired of reading third rate library manuals (the libraries
are mandated by managment) which are confusing to read, or absolutely no
help.  I would much rather see a set of preconditions (Oberon/F documents
preconditions, postconditions and trap values for violators) than a bunch
of poorly written prose from some stressed out programmer who believes the
library is simple & obvious.

['third rate' above means anything from AccSys (a very poorly designed dBase
library) to Borland's OWL or Microsoft's MFC.  OWL is particularly bad.  
There is no correlation between large companies and good documentation,
and small companies and bad documentation.  Either type of documentation
can be produced from either type of company]

Taylor Hutt
Bagpipe music: cacophony or fabulous study in chaos?



Fri, 20 Jun 1997 00:04:51 GMT  
 Pre- and post-conditions (was Commenting code)

Quote:


>        I think the Eiffel and Sather languages take this a
>step further.  Pre- and post-conditions are part of the
>procedure declaration, methods can inherit these invariants,
>and an exception will be raised if a condition is violated.  
>        Oberon can emulate these features, and I wonder how
>valuable they have turned out to be for other programmers.  
>Though great in theory -- this is often how programs are
>formally specified -- I wonder how useful built-in pre- and
>post-conditions turn out to be in practice, since many formal
>assertions cannot be practically checked at run-time.  (I'm
>cross-posting this to Eiffel and Sather newsgroups.)

Until using Sather I rarely used assertions and the like.  I now use
pre and post conditions in quite a bit of my code as well as
assertions and invariants.  Being able to debug with them on, then
turn them off on a class by class basis means that I can have
expensive checks and eliminate them when I want to.  This has
undoubtedly saved me lots of debugging time.

Class invariants are less useful though.  Since they are called at
each routine invocation, they are often called at times when the
object does not obey its invariants - because the called routine is
there specifically to fix it.  

--


"You never learn anything, you just get used to it."



Mon, 23 Jun 1997 03:46:49 GMT  
 Pre- and post-conditions (was Commenting code)

Quote:


>>To me, the pre/post-conditions are the major thing; the implementation is
>>just a commentary to the pre/post-conditions.  The pre/post-conditions are
>>the real theory; the implementation is just a special case, given here as an
>>example to this theory.

>        I think the Eiffel and Sather languages take this a
>step further.  Pre- and post-conditions are part of the
>procedure declaration, methods can inherit these invariants,
>and an exception will be raised if a condition is violated.  
>        Oberon can emulate these features, and I wonder how
>valuable they have turned out to be for other programmers.  
>Though great in theory -- this is often how programs are
>formally specified -- I wonder how useful built-in pre- and
>post-conditions turn out to be in practice, since many formal
>assertions cannot be practically checked at run-time.  (I'm
>cross-posting this to Eiffel and Sather newsgroups.)

The word I get from the field, that is, from people working on
commercial Eiffel software is that
  1) Where they used assertions extensively in a well disciplined fashion
   there was major payback in quality.
  2) They wish they'd used them more!

Hope this helps,
-- Jim

--

*------------------------------------------------------------------------------*
Jim McKim  (203)-548-2458     In exactly 3.2 seconds it will be a few



Tue, 24 Jun 1997 02:44:37 GMT  
 Pre- and post-conditions (was Commenting code)
I have a little confusion in when to use exception handling.  I have seen
many examples of different uses for exception handling in Eiffel (rescues).

My question is:  When is exception handling appropriate?  And when is it not?

The use of exceptions that I currently aggree with
involves those "out of our control" exceptions
that occur at the operating system level or close to it.  The EiffelNet
libraries use exception handling to clean up sockets if something goes wrong:

        my_server_make is
                do
                        make_the_server
                        execute_the_server
                        cleanup_the_server
                rescue
                        cleanup_the_server
                end

This is great, useful and works well!

At the other extreme I have seen examples of exception handling used in
data entry validation:

        my_data_entry: STRING is
                do
                        io.readline
                        Result := io.laststring
                ensure
                        Result.count <= Max_entry_length
                rescue
                        io.putstring ("Invalid entry.")
                        retry
                end

This exception relies on the postcondition being checked and failing if
the string entered is to long.  What happens if I compile this system
with postcondition checking turned off?  Yes, it wouldn't work!

Another example, a little better than above (IMHO), could be:

        my_data_entry: INTEGER is
                do
                        io.readint
                        Result := io.lastint
                rescue
                        io.putstring ("Entry must be an integer")
                        retry
                end

This routine doesn't rely on a postcondition to cause the exception, but
relies on the failure of readint if the user enters a string that doesn't
make up an integer.

At what extreme should exceptions be used: for only OS like exceptions,
exceptions on assertions or what?

I tend to write my Eiffel code with just the feature specifications
(assertions etc.) and the code comes later (sometimes much later :-).
But I don't believe I am using the exception mechanism to its fullest
potential.

I welcome any discussion on this topic.

Glenn Maughan

--
Glenn Maughan ---------------------------------------------------------------
Object Technology Group, PhD Student | Ph:    +613 90-32660
Department of Software Development   | Fax:   +613 90-32745



Wed, 25 Jun 1997 06:59:58 GMT  
 Pre- and post-conditions (was Commenting code)
Please remove comp.lang.oberon from the exception handling
discussion.  I began the thread on pre- and post-conditions
and crossposted it to the Eiffel and Sather newsgroups, but
the exception handling features of those languages are not
relevant to Oberon.

Thank you,
Mike



Wed, 02 Jul 1997 10:49:22 GMT  
 Pre- and post-conditions (was Commenting code)

! Suppose library A raise ea1, ea2.  Library B raise eb1, uses library A,
! and passes through ea1 to the clients of library B.  If library A is
! revved to now raise ea3 as well, the type signatures of the routines in
! library B are now in error.  If A and B come from different vendors,
! this is a potential nightmare for developers, and a reason not to
! require that exceptions be declared.

I can now see that this is a problem, but I still feel it must be well
documented what exceptions may be raised. There are other ways than doing
it for each routine. Let's suppose we declare that library A may raise
ea1, ea2, and library B may raise eb1. (These declarations would be per
library and not per routine.) In addition we specify that library B depends
on library A and thus may raise any exception that A may raise. Now if library
A gets a new exception ea3, library B doesn't have to be changed.

This would give the responsibility of exceptions that A may raise only
to A and eventual users of A and B. I.e. one library would not be
responsible for the exceptions another library may raise but it would
be responsible for its own exceptions.

In some way this is a compromise, but it seems better than having no
exception declarations at all.

--
---                               --    
--   --   Ari Huttunen           ----   Twas brillig, and the slithy toves
    ----                  --      --      Did gyre and gimble in the wabe;
     --                  ----           All mimsy were the borogoves,
                          --              And the mome raths outgrabe.
                                                          <JABBERWOCKY>



Sat, 05 Jul 1997 21:42:09 GMT  
 Pre- and post-conditions (was Commenting code)

Quote:
(Ari Juhani Huttunen) writes:

> (Jonathan Shapiro) writes:

> ! Suppose library A raise ea1, ea2.  Library B raise eb1, uses library
> A,
> ! and passes through ea1 to the clients of library B.  If library A is
> ! revved to now raise ea3 as well, the type signatures of the routines
> in
> ! library B are now in error...

> I can now see that this is a problem, but I still feel it must be well
> documented what exceptions may be raised.

Absolutely. My point was only that such documentation cannot, in
principle, always be accurate.  There is a window of time prior to the
new release of module B during which the old documentation is current,
and does not yet reflect the new exceptions that are thrown by module A.

As to granularity, it proves in practice to be fairly important to know
which exceptions can be thrown at the granularity of procedures, so
module-scope declarations are not entirely satisfactory.

Jonathan



Sun, 06 Jul 1997 00:43:44 GMT  
 Pre- and post-conditions (was Commenting code)

Quote:
(Harry G. George) writes:



> >Eiffel and C++ both have relatively elaborate exception systems.

> >Oberon has essentially a one-level system: halt the current task and
return
> >to the main loop.

> >What none of them has (at least the last time I looked at Eiffel, it
didn't
> >have this) is something like Common Lisp's unwind-protect.

Not so.  Try this:

   foo is
   do
      dangerous_call;
      protection_call;
   rescue
      protection_call;
   end;

The "rescue" clause is called automatically if any kind of exception is
generated during the routine.  Hence whether there is an exception or not,
the routine "protection_call" will be executed.

However unwind-protect mechanisms are generally a bad idea: one should be
taking different action for a failure than a success.  Failure actions
should try to tidy up the object, leaving it in some sort of consistent
state.  The usual use for unwind-protect is to restore some kind of global
state which should have been local in the first place.

A rescue clause will can terminate in one of two ways.  The one above falls
through, generating an exception in the caller.  The alternative is to
"retry", which jumps to the start of the routine and runs it again.  It is
up to the programmer to avoid an endless loop under these circumstances.

Paul.
--
----------------------------------------+-----------------------------------
---
Paul Johnson                            | You are lost in a maze of twisty




Thu, 10 Jul 1997 18:39:50 GMT  
 Pre- and post-conditions (was Commenting code)

Quote:



>> >Class invariants are less useful though.  Since they are called at
>> >each routine invocation, they are often called at times when the
>> >object does not obey its invariants - because the called routine is
>> >there specifically to fix it.  

>> Then you are not using class invariants correctly. Class invariants are
>> things that shouldn't ever be untrue after calling a publicly assessable
>> function. They are a conveniant way of putting the same postcondition
>> after every function in the class.

>Actually you are both missing the point.  Class invariants are things
>that are true *outside* feature execution time.  So if you have a
>class with routines "foo" and "bar", where "foo" calls "bar", then
>"bar" should only check the invariants if called from another object.
>When "foo" calls "bar", "bar" should *not* check its invariants
>because "foo" might have temporarily violated them.

>Note the subtle difference between calls from another class and
>another object.  If "foo" calls "other.bar" where "other" is an object
>of the same type, then "bar" should still check its invariants.  Each
>object is responsible for its own consistency, and should not be its
>brother's keeper.

>This leads to a difference in semantics between a call to "bar" and a
>call to "Current.bar".  The former will not cause an invariant check,
>while the latter does.

If you want to get picky, you can't ever make totally sure that the
invariants are satisfied.
Imagine eiffel classes:

class A feature forward: B end;
class B feature backward: A end;

If A has class invariant
forward.backward = Current

Then you can't ever be certain that the invariant is maintained since a
feature of class B could invalidate A's invariant without ever calling any
more members of A.

--

Chris Bitmead



Sat, 12 Jul 1997 01:30:43 GMT  
 
 [ 16 post ]  Go to page: [1] [2]

 Relevant Pages 

1. Pre-condition vs. Post-condition

2. Pre-condition vs. Post-condition

3. Pre-condition vs Post-condition

4. "BIG E vs little e", was pre-condition vs post-condition

5. pre-condition vs post-condition

6. question about pre- & post-conditions

7. percursor and pre- and post-condition inheritance

8. Pre- and post-conditions under multiple inheritance

9. Where to implement Pre and Post Conditions?

10. "Destructors" and dynamic pre/post-conditions

11. Pre/Post Conditions

12. Old chestnut: invariants, pre/post conditions

 

 
Powered by phpBB® Forum Software