• Sean Kelly <sean f4.ca> Apr 13 2005
• Sean Kelly <sean f4.ca> Apr 14 2005

Sean Kelly <sean f4.ca> writes:

# /*
#  This example shows that the class invariant and postcondition are
#  not evaluated if scope exits via an exception.  if the exception
#  is recoverable it is possible that the function postcondition has
#  not been met and that the application is in an invalid state.  The
#  class invariant will be tested the next time a public method is
# called, but this may still be a while.
#  */
#
# import std.c.stdio; 
# 
# class DBCTest
# {
#     this()
#     {
#       cnt = 0;    
#     }
#     
#     void f1()
#     in
#     {
#         printf( "in\n" );
#     }
#     out
#     {
#         printf( "out\n" );
#     }
#     body
#     {
#         printf( "body\n", cnt );
#         if( cnt++ > 0 )
#             throw new Exception( "DBCTest Exception" );
#     }   
#     
#     invariant
#     {
#         printf( "invariant\n" );    
#     }
#     
#     int cnt;
# }
# 
# void main()
# {
#     DBCTest d = new DBCTest();
#     
#     while( true )
#     {
#         try
#         {              
#             d.f1();
#             printf( "*** loop ***\n" );
#         }
#         catch( Exception e )
#         {
#             printf( "DBC test caught: %.*s \n", e.toString() );
#             break;
#         }
#     }
#     printf( "done\n" );    
# }

Sean Kelly <sean f4.ca> writes:

FWIW, this first example was more to promote discussion than an actual bug
report.  AFAIK this is working as intended.


Sean